ThEdu Workshop series
ThEdu is a workshop series on theorem-proving components for educational software. The first ThEdu was held in 2011, and since then, it has been held annually, collocated with the CADE conference (or umbrella conferences containing CADE, e.g. IJCAR, FLoC).
The ThEdu group intends to gather the research communities for computer Theorem proving (TP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS) and Dynamic Geometry Systems (DGS).
The goal of this union is to combine and focus systems of these areas to enhance existing educational software as well as studying the design of the next generation of mechanised mathematics assistants (MMA).
ThEdu Mailing list
The address is: thedu@uc.pt
Archive of the mailing list is at: ml.ci.uc.pt/mhonarchive/thedu/.
ThEdu Board
Steering Committee:
- João Marcos, Federal University of Rio Grande do Norte, Brazil
- Filip Marić, University of Belgrade, Serbia
- Julien Narboux, University of Strasbourg, France
- Walther Neuper, Johannes Kepler University Linz, Austria
- Pedro Quaresma, University of Coimbra, Portugal
- Jørgen Villadsen, Technical University of Denmark, Denmark
ThEdu By-laws
By-laws of the "Theorem-proving components for Educational software (ThEdu)" Interest Group
The motivation for these by-laws is to guide the future directions and governance of the Theorem-proving components for Educational software (ThEdu) Workshop series. Ultimately, we hope to build a community of researchers and practitioners centred around the aims of the previous ThEdus, namely "to bring 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". Experts working on topics such as:
- proof and proving in mathematics education;
- 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;
- automatic/interactive provers applied to education.
To build such a community, we need continuity and some rules governing the central activity of any research community, namely, the ThEdu workshop. The following proposal is based on, and consistent with, the historical patterns observed in the first ten ThEdu (from 2011 to 2021). The proposal is deliberately minimal and under-specified. Therefore, their interpretations should be guided by historical patterns.
By-law 1: Organisation
Each ThEdu Workshop shall have the following organisational positions:
- General Chair
- Program Chair
- The Steering Committee
- Program Committee
In between workshops the Steering Committee is the governing body of the ThEdu Interest Group. Chair, could also mean Co-chairs. If needed a local Chair could be added to this structure for the purpose of the organisation of a given ThEdu Workshop.
By-law 2: Collocation
- The preferred collocation of ThEdu is the CADE conference (or umbrella conferences containing CADE, e.g. IJCAR, FLoC).
By-law 3: Appointments
The initial appointments, for ThEdu'22, are:
- General Chair: Pedro Quaresma, University of Coimbra;
- Program Chair: Walther Neuper, Johannes Kepler University Linz;
- Steering Committee: Pedro Quaresma, Walther Neuper and João Marcos, Universidade Federal do Rio Grande do Norte.
- The Steering Committee shall consist of the General Chair, Program Chair and any other members that they shall appoint.
- After the workshop, the Steering Committee appoints the General Chair for the next workshop.
- The General Chair, in consultation with the Steering Committee, appoints the Program Chair and, eventually, the Local Chair.
- The Program Chair, in consultation with the General Chair and the Steering Committee, appoints the Program Committee members.
By-law 4: Duties
- The General Chair, in collaboration with the Local Chair, will hold a ThEdu business meeting during each Workshop.
- The General Chair for the next workshop, should prepare a ThEdu workshop proposal, to be submitted to the conference to which the workshop will be collocated.
- The Steering Committee and the Local Chair shall maintain, for each workshop, the corresponding ThEdu website, including links to previous ThEdu Websites.
- The General Chair, in collaboration with the Local Chair, should publicise the Workshop through the appropriate channels, e.g. the Association for Automated Reasoning (AAR) newsletter.
- The Steering Committee, with the collaboration of the Local Chair, should manage the ThEdu's mailing list, with the names of authors and attendees of past ThEdu workshops.
By-law 5: Amendments
- The by-laws can be amended by ballot between workshop, given a proposal by the Steering Committee. A simple majority is enough for approval.
- Persons who have registered for at least one of the three preceding ThEdu workshops are eligible to vote.
- The ballot will be run by the Steering Committee.
ThEdu'22, 11 August 2022, Haifa, Israel.
ThEdu Proceedings
- ThEdu'24 - Proceedings
- Proceedings 13th International Workshop on Theorem proving components for Educational software, 11 or 12 August, Satellite event at IJCAR 2024, Nancy, France, July 1-6, 2024, EPTCS 419, 25th May 2025.
- ThEdu'23 - Proceedings
- Proceedings 12th International Workshop on Theorem proving components for Educational software, 5 of July 2023, workshop at the, 29th international Conference on Automated Deduction (CADE 2023), July 1-4, 2023, Rome, Italy, EPTCS 400, 10th March 2023.
- ThEdu'22 - Proceedings
- Proceedings 11th International Workshop on Theorem proving components for Educational software, 11 or 12 August, workshop at FLoC 2022, July 31 – August 12, 2022, Haifa, Israel, EPTCS 375, 10th March 2023.
- ThEdu'21 - Proceedings
- Proceedings 10th International Workshop on Theorem proving components for Educational software, July 2021, Carnegie Mellon University, Pittsburgh, PA, United States of America (virtual), EPTCS 354, 8th February 2022.
- ThEdu'20 - Proceedings
- Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu'20), Paris, France, June 2020 (canceled due COVID-19), EPTCS 328, 30th October 2020.
- ThEdu'19 - Proceedings
- Proceedings 8th International Workshop on Theorem Proving Components for Educational software (ThEdu'19), 25 August 2019, Natal, Brazil, EPTCS 313, 28th February 2020.
- ThEdu'18 - Proceedings
- Proceedings 7th International Workshop on Theorem proving components for Educational software (ThEdu'18), Oxford, United Kingdom, 18 July 2018, EPTCS 290, 1 April 2019.
- ThEdu'17 - Proceedings
- Proceedings 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg Sweden, 6 August 2017, EPTCS 267, 2 March 2018.
- ThEdu'16 - Proceedings
- Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016. CEUR-WS, 1785.
- ThEdu'15 - Proceedings
- Proceedings 4th International Workshop on Theorem proving components for Educational software (ThEdu'15). July 15, 2015, Washington DC, USA CISUC TR2016-01.
- ThEdu'14 - Proceedings
- Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM co-located with Conferences on Intelligent Computer Mathematics (CICM 2014), Coimbra, Portugal, July 7-11, 2014. CEUR-WS, 1186.
- ThEdu'13 - Proceedings
- Joint Proceedings of the MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at CICM co-located with Conferences on Intelligent Computer Mathematics (CICM 2013), Bath, UK, July 9 - 10, 2013. CEUR-WS, 1010.
- ThEdu'11 - Proceedings
- Post-Proceedings of the First Workshop on CTP Components for Educational Software, Wrocław, Poland, 31 July 2011. EPTCS 79, 2012.
ThEdu'26
Presentation
ThEdu'26 will be held on 19 July 2026, collocated with FLoC 2026, in Lisbon, Portugal.
Important Dates
| Extended Abstracts : | 29 April 2026 (firm deadline imposed by FLoC) |
| Author Notification : | 27 May 2026 |
| Workshop Early Registration Deadline: | 1 June 2026 |
| Workshop Day: | 19 July 2026 |
Program Committee (tentative)
- João Marcos, Federal University of Rio Grande do Norte, Brazil
- Julien Narboux, University of Strasbourg, France (co-chair)
- Walther Neuper, Johannes Kepler University Linz, Austria (co-chair)
- Pedro Quaresma, University of Coimbra, Portugal
- Jim Portegies, Eindhoven University of Technology
- Vanda Santos, University of Aveiro, Portugal
- Wolfgang Schreiner, Johannes Kepler University, Austria
- M. Pilar Vélez, Nebrija University, Spain
- Jørgen Villadsen, Technical University of Denmark, Denmark
Call for extended abstracts and demonstrations
ThEdu is open to all aspects of the design or use of logical tools (proof assistants, automated theorem provers, model checkers, model finders, rich type systems, property-based testing, and more) for education in science (especially in the teaching of logic, mathematics and computer science). This includes work about the design of tools and libraries for education, experience reports, and evaluation of their effectiveness for learning.Activities
ThEdu will have two kinds of activities:- Regular paper presentations;
- Demonstrations, where the presenters shows their tool to all the attendees
Submissions
In your submission, please make clear what kind of activity you are proposing.- Research Papers:
- These should be in the usual form of a scientific paper. They must be original, unpublished work that has not been submitted for publication elsewhere. Accepted papers will receive a plenary presentation slot.
- Repeat Papers:
- These are about works strongly tied to the theme of the workshop, have already been published elsewhere, but would be of real interest to the attendees. These submissions will not become part of the formal academic record of the workshop; their only trace will be a listing in the program. Authors are therefore welcome to submit an already-published paper whose copyright they may or may not own. The submission should be preceded by a cover page that describes why this paper is relevant, and indicates where and when it was published. Accepted papers will receive a plenary presentation slot.
- Plenary Demos:
- These should describe the artifact (tool, website, etc.) to be demoed. The submission should explain what the presentation is likely to entail.
At least one of the authors of each accepted submission is expected to attend and present their work.
Program
TBA in June 2026.
Post-proceedings: call for papers
We plan to publish post-proceedings for ThEdu'26 after the workshop after a second round of reviewing using EPCTS as in previous years. This will be discussed during the business meeting of ThEdu'26.