Published: 2nd March 2018
DOI: 10.4204/EPTCS.267
ISSN: 2075-2180


Proceedings 6th International Workshop on
Theorem proving components for Educational software
Gothenburg, Sweden, 6 Aug 2017

Edited by: Pedro Quaresma and Walther Neuper

Learning how to Prove: From the Coq Proof Assistant to Textbook Style
Sebastian Böhne and Christoph Kreitz
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
Arno Ehle, Norbert Hundeshagen and Martin Lange
Improving QED-Tutrix by Automating the Generation of Proofs
Ludovic Font, Philippe R. Richard and Michel Gagnon
A Theorem Prover for Scientific and Educational Purposes
Mario Frank and Christoph Kreitz
Carnap: An Open Framework for Formal Reasoning in the Browser
Graham Leach-Krouse
Prototyping "Systems that Explain Themselves" for Education
Alan Krempler and Walther Neuper
Exchange of Geometric Information Between Applications
Pedro Quaresma, Vanda Santos and Nuno Baeta
Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models
Wolfgang Schreiner, Alexander Brunhuemer and Christoph Fürst
Natural Deduction and the Isabelle Proof Assistant
Jørgen Villadsen, Andreas Halkjær From and Anders Schlichtkrull


The reader is welcome to the post-proceedings of THedu'17.

(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 ThEdu'17 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.

These words introduced the ThEdu'17 workshop associated to CADE26, 6 Aug 2017, Gothenburg, Sweden. ThEdu'17 was a vibrant workshop, with one invited talk and eight contributions. It triggered the post-proceedings at hand.

ThEdu'17 is the 6th edition of the ThEdu series of workshops. The major aim of the ThEdu workshop series was to link developers interested in adapting TP to needs of education and to inform mathematicians and mathematics educators about TP's potential for educational software--together with a parallel workshop series in the Conference on Digital Tools in Mathematics Education (CADGME) conferences, primarily addressing educators responsible for STEM (Science, Technology, Engineering and Mathematics) studies. Looking back to seven years of the parallel workshop series shows that the "new TP-based generation" is gaining acceptance in a wider public, that ideas about specific use of TP technologies prosper and that envisaged applications address an increasing range of issues.

The contributions to ThEdu are diverse reflecting the communities the authors come from. ThEdu's program committee reflects this diversity, too. Collaboration between these communitiesis required to path the way towards the new generation mentioned above. So we face this diversity as positive, making the break lines explicit in the survey on contributions below--indicating referees' objections.

Schreiner et al. presented a specification language plus automated (conter-)example generation as the basis of a tool chain already well established in education--and were criticised for lack of educational experience with the basis of the chain. On the other hand, Böhne et al. presented empirical research about academic education in proving based on a mini-adaption of Coq--and were criticised for bypassing recent systems' features of structured proof and for disregarding their usability in education. Villadsen et al. presented a comprehensive substitution for Isabelle's front-end (while keeping the logical background transparent) in order in improve educational use--and were confronted with a detailed description how Isabelle "as is" can be used for the same educational purpose.

Using an opposite approach, three contributions even start building a TP from scratch for educational purposes--with objections from the point of logical trustability as well as from "re-inventing the wheel", see "Isabelle: The Next 700 Theorem Provers". The three respective technological bases are different: Leach-Krouse presents a Haskell-based implementation generic for various kinds of "baby" provers. Ehle et al. focus sequent calculus and base their implementation on Java. Frank et al. focus untyped lambda calculus as a starting point for a logical framework even incorporating ITP (and base their implementation on C++).

Geometry is an exercise field for learning to prove, in particular in Anglo-American countries. Two contributions act on this relevance and provide respective software support: Quaresma et al. presented a new connection between an e-learning platform and a repository of geometry problems for theorem provers plus a wealth of ideas for exploitation in education--and were criticised that their paper reads more like a research proposal rather than a publishable description of research results (in terms of technology). Richard et al. build an inference engine in Prolog from scratch, which is considered more efficient than adaption of existing TPs, given the restricted problem space in geometry education--and were criticised for limited functionality inhibiting transition to higher levels of education.

One contribution not even mentions "proof": Krempler et al. use Isabelle's components to support "engineering mathematics" by interactive formal specification and subsequent step-wise construction of solutions (where the latter is forward proof using a specific format).

So there are good reasons for criticism from both sides, from the side of TP as well as from the side of education. The PC invested much effort to balance the two sides and to ensure quality of contributions appropriate to EPTCS.

The small collection of papers in this volume makes a colourful carpet of various ideas and divergent processes--divergent not only alongside the two communities brought together by the workshop series, but even within these communities. That is the present picture in the interdisciplinary approach to the novel challenge posed by ThEdu's call. It's ultimate aim, improvement of software support in learning mathematics, will require collaboration. Such collaboration is not in sight of the present collection.

The PC hopes that this publication will increase mutual understanding between the two sides and attract new researchers from several communities in order to enhance existing educational software as well as study of new software developments. The PC invites all readers to the ThEdu'18 edition, associated to FLOC, Oxford, UK, 6-19 July 2018.

Pedro Quaresma, Walther Neuper, January 2018

ThEdu'17 Program Committee

Francisco Botana, University of Vigo at Pontevedra, Spain
Achim Brucker, University of Sheffield, United Kingdom
Roman Hašek, University of South Bohemia, Czech Republic
Filip Marić, University of Belgrade, Serbia
Walther Neuper, Graz University of Technology, Austria (co-chair)
Pavel Pech , University of South Bohemia, Czech Republic
Pedro Quaresma, University of Coimbra, Portugal (co-chair)
Vanda Santos, CISUC/University of Coimbra, Portugal
Wolfgang Schreiner, Johannes Kepler University, Austria
Burkhart Wolff, University Paris-Sud, France