Teaching Logic Using a State-of-the-Art Proof Assistant - Volume 3 - Issue 2 - 2010

Oct 15, 2026

Uploaded by Rizky

ProofWeb is presented as a system for teaching logic to undergraduate computer science students through an interactive web interface. Built on the higher-order proof assistant Coq, it combines a large database of logic problems with support for storing student solutions and centrally tracking progress. Students can work without installations, including no browser plug-ins, while natural deduction proofs are shown in Gentzen-style tree view and Fitch-style box view.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages14

Reading Time35 min

AccessFree to download

Introduction

Teaching logic in undergraduate curricula

Benefits of exercise practice and computer assistance

Examination use case

ProofWeb development and key innovations

Volume 3, Number 2, 2010 TEACHING LOGIC USING A STATE-OF-THE-ART PROOF ASSISTANT Maxim Hendriks, Cezary Kaliszyk, Femke van Raamsdonk, Freek Wiedijk 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 ofthe 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/](http://proofweb.cs.ru.nl/) . Key words: Logic Education, Proof Assistants, Coq, Web Interface, Natural Deduction 1 Introduction At most European universities, part of the undergraduate computer science curriculum is an introductory course that teaches the rules of propositional and predicate logic. At the Radboud Universiteit (RU) in Nijmegen this course is taught in the first year and is called `Beweren en Bewijzen' (Dutch for `Stating and Proving') . At the Vrije Universiteit (VU) in Amsterdam this course is taught in the second year and is called `Inleiding Logica' (`Introduction to Logic') . Almost all computer science curricula have similar undergraduate courses. For learning this kind of elementary mathematical logic it is crucial to work many exercises. Those exercises can of course be done in the traditional way, using pen and paper. The student is completely on his own, and in practice it often happens that proofs that are almost-but-not-completely-right are produced. Alternatively, they can be made using some computer program, which guides the student through the development of a completely correct proof. A disadvantage of the computerized way of practising mathematical logic is that a student often will be able to finish proofs by random experimentation with the commands of the system (accidentally hitting a solution), without really having understood how the proof works. Of course, a combination of the two styles of practicing formal proofs seems to be the best option. In any case, computer assistance for learning to construct derivationsin mathematical logic seems desirable. Currently the most popular program that is used for this kind of `computer-assisted logic teaching' is a logical framework called Jape [3], developed by Surin and Bornat at the University of Oxford. Besides exercises there is also the issue of examination. It would be good if the student has the opportunity to do at any moment a (part of the) logic exam by logging in to the system and be presented with a set of exercises from a database that have to be solved within a certain time. This may require human supervision to prevent cheating. We did not yet work on this, but just mention it as a possible interesting application of computer-assisted logic teaching. This article describes our development, named ProofWeb. This system provides functionality much This paper is an expanded version of the presentation given to the second Computer Algebra and Dynamic Geometry Systems in Mathematics Education (CADGME) conference at the Unive

FAQs

What is ProofWeb and what problem does it address?

ProofWeb is a web-based system for teaching logic to undergraduate students. It focuses on helping students practice proof construction while reducing issues like finishing proofs by random command experimentation.

How does ProofWeb deliver logic exercises and proof checking?

Students access a central server via a web interface, and the proof assistant runs on the server. The system supports Coq-based inference and indicates whether automation was used or proofs were built using inference rules.

What presentation styles are supported for natural deduction proofs?

ProofWeb supports Gentzen-style tree view and Fitch-style box view, presenting deduction proofs in formats customary for undergraduate logic courses.

Oct 15, 2026

Uploaded by Rizky