Published: 28th February 2020
DOI: 10.4204/EPTCS.313
ISSN: 2075-2180


Proceedings 8th International Workshop on
Theorem Proving Components for Educational Software
Natal, Brazil, 25th August 2019

Edited by: Pedro Quaresma, Walther Neuper and João Marcos

João Marcos, Walther Neuper and Pedro Quaresma
Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context
Ludovic Font, Sébastien Cyr, Philippe R. Richard and Michel Gagnon
Providing Hints, Next Steps and Feedback in a Tutoring System for Structural Induction
Josje Lodder, Bastiaan Heeren and Johan Jeuring
A Mobile Application for Self-Guided Study of Formal Reasoning
David M. Cerna, Rafael P.D. Kiesel and Alexandra Dzhiganskaya
Tools in Term Rewriting for Education
Sarah Winkler and Aart Middeldorp
Teaching a Formalized Logical Calculus
Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen
Towards a Geometry Automated Provers Competition
Nuno Baeta, Pedro Quaresma and Zoltán Kovács


Computer Theorem Proving 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'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth instalment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call for papers was issued having attracted seven submissions, six of which have been accepted by the reviewers, and collected in the present post-proceedings volume.

The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise.

Tutorial systems where automated deduction methods or tools are integrated in learning environments are in the core of ThEdu. Ludovic Font et al. anticipate the students next step by building, automatically, the graph of all possible inferences, for a given geometric statement. Josje Lodder et al. discuss the design of a tutoring system, LogInd, that helps students with constructing stepwise inductive proofs by providing hints, next steps and feedback. David Cerna et al. open the door to learning at anytime and everywhere, by describing an Android application, AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Teaching logical deduction is also a subject in the realm of ThEdu, Sarah Winkler and Aart Middeldorp present several automatic tools to analyse term rewrite systems which were developed by the Computational Logic Group at the University of Innsbruck, they claim that those tools already proved to be invaluable for teaching, e.g., in multiple editions of the International Summer School on Rewriting. Asta Halkjær From et al. present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL and discuss the use of such formalization in a bachelor course on logic for computer science. Last but not least, Nuno Baeta et al. introduce a Geometry Automated Theorem Provers System Competition whose first pre-edition (0.1) was run during the workshop. GASC has as main goal to push for new developments and applications in the area of automated deduction in geometry including applications in education. In their paper the authors describe the many steps needed to put together such a competition, describing the second pre-edition of GASC, towards a Geometry Automated Provers Competition.

The volume editors hope that this collection of papers will further promote the development of theorem-proving-based software, and that it will collaborate on improving mutual understanding between computer mathematicians and stakeholders in education. For their help in reviewing the papers, the editors would like to thank the other members of the Programme Committee of ThEdu'19 and the external reviewers, namely Francisco Botana (University of Vigo at Pontevedra, Spain), Filip Marić (University of Belgrade, Serbia), Adolfo Neto (UTFPR, Brazil), Carlos Olarte (UFRN, Brazil), Philippe Richard (Université de Montréal, Canada), Umberto Rivieccio (UFRN, Brazil), Vanda Santos (University of Aveiro, Portugal), and Wolfgang Schreiner (Johannes Kepler University, Austria). While this volume goes to press, the next edition of the ThEdu workshop is also being organized: ThEdu'20 will be a satellite event of IJCAR 2020, and will happen in Paris on June 29, 2020.

PC Chairs:
João Marcos (UFRN, Brazil)
Walther Neuper (Graz University of Technology, Austria)
Pedro Quaresma (University of Coimbra, Portugal)