ProofJudge: Automated Proof Judging Tool for Learning Mathematical Logic

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

378 Downloads (Pure)

Abstract

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 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 publicationExploring Teaching for Active Learning in Engineering Education (ETALEE 2015) : Book of Abstracts
PublisherIUPN - Ingeniør Uddannelsernes Pædagogiske Netværk
Publication date2015
Pages141-148
Publication statusPublished - 2015
EventExploring Teaching for Active Learning in Engineering Education (ETALEE 2015) - DTU Skylab, Kgs. Lyngby, Denmark
Duration: 11 Nov 201512 Nov 2015
http://www.etalee.dk/index.html

Conference

ConferenceExploring Teaching for Active Learning in Engineering Education (ETALEE 2015)
LocationDTU Skylab
Country/TerritoryDenmark
CityKgs. Lyngby
Period11/11/201512/11/2015
Internet address

Keywords

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

Fingerprint

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

Cite this