View: session overviewtalk overviewside by side with other conferences
09:00 | Students' Proof Assistant (SPA) SPEAKER: Anders Schlichtkrull ABSTRACT. The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle but also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach structured proving is with a concrete prover where the connection between semantics, proof system, and prover is clear. In fact, the proofs in Lamport's TLAPS proof assistant have a very similar structure to those in the declarative prover SPA. To illustrate this we compare a proof of Pelletier's problem 43 in TLAPS, Isabelle/Isar and SPA. |
09:30 | Natural Deduction Assistant (NaDeA) SPEAKER: Jørgen Villadsen ABSTRACT. We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. In particular we compare our approach to natural deduction in the Isabelle proof assistant. NaDeA is available online: https://nadea.compute.dtu.dk/ |
10:00 | Rating of Geometric Automated Theorem Provers SPEAKER: Pedro Quaresma ABSTRACT. The field of geometric automated theorem provers has a long and rich history, form the early synthetic provers in the 50th of last century to nowadays provers. Establishing a rating among them will be useful for the improvement of the current methods/implementations. With wider scope, more efficient, with readable proofs and with trustworthy proofs. We need a common test bench: a common language to describe the geometric problems; a large set of problems and a set of measures to achieve such goal. |
14:00 | SPEAKER: Maximilian Doré ABSTRACT. Proving lemmas in synthetic geometry is an often time-consuming endeavour - many intermediate lemmas need to be proven before interesting results can be obtained. Automated theorem provers (ATP) made much progress in the recent years and can prove many of these intermediate lemmas automatically. The interactive theorem prover Elfe accepts mathematical texts written in fair English and verifies the text with the help of ATP. Geometrical texts can thereby easily be formalized in Elfe, leaving only the cornerstones of a proof to be derived by the user. This allows for teaching axiomatic geometry to students without prior experience in formal mathematics. |
14:30 | Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable ABSTRACT. We present a new succinct proof of the uncountability of the real numbers – optimized for clarity – based on the proof by Benjamin Porter in the Isabelle Analysis theory. |
ThEdu Business Meeting
16:00 | ThEdu'18 business meeting SPEAKER: Pedro Quaresma ABSTRACT. ThEdu'18 business meeting ThEdu'18 post proceedings at EPTCS ThEdu'19 - where, when and other organizational issues. |
Workshops dinner at Magdalen College. Drinks reception from 7.15pm, to be seated by 7:45 (pre-booking via FLoC registration system required; guests welcome).