Proceedings 12th International Workshop on Theorem proving components for Educational software
arXiv:2404.03709 · doi:10.4204/EPTCS.400
Abstract
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. The 12th International Workshop on Theorem Proving Components for Educational Software(ThEdu'23), was a satellite event of the 29th international Conference on Automated Deduction (CADE 2023), July 1-4, 2023, Rome, Italy. ThEdu'23 was very successful, with one invited talk, by Yves Bertot (Inria, France), "The challenges of using Type Theory to teach Mathematics", and seven regular contributions. An open call for papers was then issued, to which eight contributions were submitted. Seven submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. We, the volume editors, hope that this collection of papers will further promote the development of theorem-proving based software, and that it will allow to improve the mutual understanding between computer scientists, mathematicians and stakeholders in education. PC Chairs:Julien Narboux (University of Strasbourg, France); Walther Neuper (JKU, Johannes Kepler University, Linz, Austria); Pedro Quaresma (University of Coimbra, Portugal)
References in corpus (14)
- How is ChatGPT's behavior changing over time?
- Autoformalization with Large Language Models
- Computational Logic: Its Origins and Applications
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
- Natural Deduction Assistant (NaDeA)
- ANITA: Analytic Tableau Proof Assistant
- A Proof Tree Builder for Sequent Calculus and Hoare Logic
- SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
- On Exams with the Isabelle Proof Assistant
- Natural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diproche
- Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
- Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode
- Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics
- Improving the Diproche CNL through Autoformalization via Large Language Models