Teaching logic using a state-ofthe-art proof assistant

This article describes the system ProofWeb that is currently being developed in Nijmegen and Amsterdam for teaching logic to undergraduate computer science students. This 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 will be a large database of logic problems. This database will also hold the solutions of the students. This means that the students do not need to install anything to be able to use the system (not even a browser plug-in), and that the teachers will be able to centrally track progress of the students. The system makes the full power of Coq available to the students, but simultane-ously 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 a type theory course, and is currently being further developed in the first year logic course of computer science in Nijmegen