Proceedings 7th International Workshop on Theorem proving components for Educational software

TL;DR

The paper summarizes the 7th ThEdu workshop focused on integrating theorem proving components into educational software, highlighting methods, applications, and discussions on automated deduction in math education.

Contribution

It presents the workshop's discussions, contributions, and the potential of theorem proving tools for enhancing educational software and mathematics teaching.

Findings

Workshop facilitated discussions on automated deduction in education

Highlighted potential of theorem proving for educational software

Presented new methods for dynamic geometry systems

Abstract

The 7th International Workshop on Theorem proving components for Educational software (ThEdu'18) was held in Oxford, United Kingdom, on 18 July 2018. It was associated to the conference, Federated Logic Conference 2018 (FLoC2018). The major aim of the ThEdu workshop series was to link developers interested in adapting Computer Theorem Proving (TP) to the needs of education and to inform mathematicians and mathematics educators about TP's potential for educational software. 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. ThEdu'18 was a vibrant workshop, with one invited talk and six contributions. It triggered the post-proceedings at hand.