|
Published: 1st April 2019 DOI: 10.4204/EPTCS.290 ISSN: 2075-2180 |
| Preface Pedro Quaresma and Walther Neuper | |
| Students' Proof Assistant (SPA) Anders Schlichtkrull, Jørgen Villadsen and Andreas Halkjær From | 1 |
| Natural Deduction Assistant (NaDeA) Jørgen Villadsen, Andreas Halkjær From and Anders Schlichtkrull | 14 |
| Towards Ranking Geometric Automated Theorem Provers Nuno Baeta and Pedro Quaresma | 30 |
| Towards Intuitive Reasoning in Axiomatic Geometry Maximilian Doré and Krysia Broda | 38 |
| Theorem and Algorithm Checking for Courses on Logic and Formal Methods Wolfgang Schreiner | 56 |
| Technologies for "Complete, Transparent & Interactive Models of Math" in Education Walther Neuper | 76 |
The reader is welcome to the post-proceedings of THedu'18.
(Computer) Theorem Proving (TP) is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. Topics of interest include: methods of automated deduction applied to checking students' input; methods of automated deduction applied to prove post-conditions for particular problem solutions; combinations of deduction and computation enabling systems to propose next steps; automated provers specific for dynamic geometry systems; proof and proving in mathematics education.
These words introduced the ThEdu'18 workshop associated to FLoC 2018, July 2018, Oxford, UK. ThEdu'18 was a vibrant workshop, the 7th edition of the ThEdu series, with an invited talk by Julien Narboux and six contributions. It triggered the post-proceedings at hand.
ThEdu pursues visions like smooth transitions from intuitively doing mathematics at high schools to formally doing mathematics in academic STEM (science, technology, engineering and mathematics) education and respective software support for gentle introduction exploiting the power of TP technologies. The new volume continues this vision, among others, from a previous one as follows:
Teaching geometry has traditionally been considered a gentle introduction to the methods of mathematics, which identifies axioms, derives definitions and theorems from these and uses them for investigating new conjectures. Doré and Broda present ELFE, a proof assistant disburdening learners from too much formality by employing an automated theorem prover (ATP) behind the scenes. Baeta and Quaresma pave the way towards ranking of geometric ATPS, useful for selecting appropriate tools.
From, Schlichtkrull and Villadsen immediately address academic education and present two different systems built upon the proof assistant Isabelle, NaDeA and SPA, for teaching logic and mathematical proof respectively, which again raised debates in the workshop and in the review process, about the advantages of downgrading in comparison with careful educational use of proof assistants as they are.
A completely new kind of support is described by Schreiner, who provides RISCAL, a language for introduction to Formal Methods, with the feature to quickly verify/falsify the specific truth of propositions in sample instances of a model class. An experience report from educational application indicates need for cooperation with experts in education. Neuper prepares for such cooperation by identifying strengths of TP technology principally useful for educational software.
The editors hope, that this volume further promotes development of TP-based software, that it improves mutual understanding between computer mathematicians and stakeholders in education - which is required to optimise educational effect of the new generation, eventually leading to "systems that explain themselves" in STEM education. The PC invites all readers to the ThEdu'19 edition, associated to CADE'27, 25-30 August 2019, Natal, Brazil.
Pedro Quaresma, Walther Neuper, March 2019