Published in Acta Didactica Napocensia, volume 3 number 2, 1 June 2010
Maxim Hendriks, Technische Universiteit Eindhoven, The
Netherlands
Cezary Kaliszyk, Technische Universität München, Germany
Femke van Raamsdonk, Vrije Universiteit Amsterdam, The Netherlands
Freek Wiedijk, Radboud Universiteit Nijmegen, The Netherlands
Abstract. This article describes the system ProofWeb developed for
teaching logic to undergraduate computer science students. The system is based
on the higher order proof assistant Coq, and is made available to the students
through an interactive web interface. Part of this system is a large database
of logic problems. This database will also hold the solutions of the students.
The students do not need to install anything to be able to use the system (not
even a browser plug-in), and the teachers are able to centrally track progress
of the students. The system makes the full power of Coq available to the
students, but simultaneously presents the logic problems in a way that is
customary in undergraduate logic courses. Both styles of presenting natural
deduction proofs (Gentzen-style `tree view' and Fitch-style `box view') are
supported. Part of the system is a parser that indicates whether the students
used the automation of Coq to solve their problems or that they solved it
themselves using only the inference rules of the logic. For these inference
rules dedicated tactics for Coq have been developed. The system has already
been used in type theory courses and logic undergraduate courses. The ProofWeb
system can be tried at http://proofweb.cs.ru.nl/.
Key words: Logic Education,
Proof Assistants, Coq, Web Interface, Natural Deduction
Pages 35-48. Download PDF