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.
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 language | English |
---|---|
Title of host publication | Exploring Teaching for Active Learning in Engineering Education (ETALEE 2015) : Book of Abstracts |
Publisher | IUPN - Ingeniør Uddannelsernes Pædagogiske Netværk |
Publication date | 2015 |
Pages | 141-148 |
Publication status | Published - 2015 |
Event | Exploring Teaching for Active Learning in Engineering Education (ETALEE 2015) - DTU Skylab, Kgs. Lyngby, Denmark Duration: 11 Nov 2015 → 12 Nov 2015 http://www.etalee.dk/index.html |
Conference
Conference | Exploring Teaching for Active Learning in Engineering Education (ETALEE 2015) |
---|---|
Location | DTU Skylab |
Country/Territory | Denmark |
City | Kgs. Lyngby |
Period | 11/11/2015 → 12/11/2015 |
Internet address |
Keywords
- E-Learning
- Automated Tool
- Mathematical Logic
- Computer Science