ThEdu 2015 - ThEdu'15 - Theorem Provers Components for Educational Software

THedu is a forum 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 and to enhance existing educational software as well as studying the design of the next generation of educational mathematical tools.
ThEdu's aims
Educational software tools have integrated technologies from Computer Algebra, from Dynamic Geometry, from Spreadsheets and others, but not from (computer) theorem proving (TP) with few exceptions: the latter have been developed to model mathematical reasoning in software; theorem provers (TPs) are successfully used to tackle difficult proofs in the science of mathematics, like the Four Color Problem or the Kepler Conjecture; and TPs are successfully used to verify safety critical software in industry.
This workshop addresses support for reasoning in mathematics education by use of TP technology.
The workshop addresses educators and designers and developers of TPs as well as of other educational mathematics software; and the discussions shall clarify the requirements of education, identify advantages and promises of TP for learning and motivate development of a novel kind of tools probably establishing a new generation of educational mathematical tools.
Points of interest include:
Adaption of TP - concepts and technologies for education: knowledge representation, simplifiers, reasoners; undefinednes, level of abstraction, etc.
Requirements on software support for reasoning - reasoning appears as the most advanced method of human thought, so at which age and what kind of support TP can provide?
Automated TP in geometry - relating intuitive evidence with logical rigor: specific provers, adaption of axioms and theorems, visual proofs, etc.
Levels of authoring - in order to cope with generality of TP: experts adapt to specifics of countries or levels, teachers adapt to courses and students.
Adaptive modules, students modeling and learning paths - services for user guidance provided by TP technology: which interfaces enable flexible generation of adaptive user guidance? Next-step-guidance, which suggests a next step when a student gets stuck in problem solving: which computational methods can extend TP for that purpose?
TP as unifying foundation - for the integration of technologies like CAS, DGS, Spreadsheets etc: interfaces for unified support of reasoning?
Continuous tool chains - for mathematics education from high-school to university, from algebra and geometry to graph theory etc.
Programme Committee
Francisco Botana, University of Vigo at Pontevedra, Spain
Roman Hašek, University of South Bohemia, Czech Republic
Filip Maric, 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, Portugal
Wolfgang Schreiner, Johannes Kepler University, Austria
Burkhart Wolff, University Paris-Sud, France