DOMtutor: Automated Autograding for Logic in Computer Science

Abstract

Teaching computer science at universities is often structured rather classically and theory oriented. The former refers to "transmission"-style lectures accompanied by exercises which are submitted and graded manually, providing delayed feedback (if any). The latter refers to exercises often posed at a conceptual level, requiring solution ideas to be sketched out on paper, but not put to the test in practice. By its nature, this is particularly true for subjects relating to theoretical computer science, such as courses on propositional or first-order logic or automata theory. Frameworks that automatically execute and evaluate code (also called autograders) are sometimes used to augment teaching. They provide (near) instant feedback and hands-on experience, prompting reflective analysis. However, their use usually is reserved for programming / practically oriented courses. We propose to (i) use autograders also (and especially) for theoretical courses and (ii) use the established DOMjudge system, which is used, among others, for the International Collegiate Programming Contest.