ProofJudge: Automated Proof Judging Tool for Learning Mathematical Logic

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

142 Downloads (Pure)


Today we have software in many artefacts, from medical devices to cars and airplanes, and the software must not only be efficient and intelligent but also reliable and secure. Tests can show the presence of bugs but cannot guarantee their absence. A machine-checked proof using mathematical logic provides strong evidence for software correctness but it is requires advanced knowledge and skills. We have developed a tool which helps the student to practice their skills and also allows a better conceptual understanding of state-of-the-art proof assistants. Previously the proofs has been carried out using pen and paper because no adequate tool was available. The learning problem is how to make abstract concepts of logic as concrete as possible.

ProofJudge is a computer system and teaching approach for teaching mathematical logic and automated reasoning which augments the e-learning tool NaDeA (Natural Deduction Assistant). We believe that automatic feedback on student assignments would allow the students to enhance their skill in natural deduction proofs which are fundamental in formal verification and artificial intelligence applications. The teachers will benefit too and can put more emphasis on the semantics. Natural deduction is taught at most if not all universities but few tools exist. Initially we plan to have former students on the course to evaluate ProofJudge and later it will be employed in the course.
Original languageEnglish
Title of host publicationProceedings of the ETALEE 2015 Conference: Exploring Teaching for Active Learning in Engineering Education
EditorsJørgen B. Røn
PublisherIUPN - Ingeniør Uddannelsernes Pædagogiske Netværk
Publication date2016
ISBN (Print)978-87-998898-0-8
Publication statusPublished - 2016
EventExploring Teaching for Active Learning in Engineering Education (ETALEE 2015) - DTU Skylab, Kgs. Lyngby, Denmark
Duration: 11 Nov 201512 Nov 2015


ConferenceExploring Teaching for Active Learning in Engineering Education (ETALEE 2015)
LocationDTU Skylab
CityKgs. Lyngby
Internet address


  • E-Learning
  • Automated Tool
  • Mathematical Logic
  • Computer Science


Dive into the research topics of 'ProofJudge: Automated Proof Judging Tool for Learning Mathematical Logic'. Together they form a unique fingerprint.

Cite this