Call for Extended Abstracts & Demonstrations 

Theorem proving components for Educational software
CICM 2015
Conferences on Intelligent Computer Mathematics
July 13-17, 2015
 Washington DC, USA

THedu'15 Scope

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.

Important Dates

     * Extended Abstracts:     31 May 2015
     * Author Notification:     14 June 2015
     * Final Version:             28 June 2015
     * Workshop Day:           15 July 2015

Submissions via THedu'15 easychair (closed)

ThEdu's aims

The distinguishing feature of mathematics is reasoning: questionable statements are proved by the laws of logic. This kind of reasoning makes mathematics a central thinking technology of modern science.

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.


We welcome submission of extended abstracts and demonstration proposals presenting original unpublished work which is not been submitted for publication elsewhere.

All accepted extended abstracts and demonstrations will be presented at the workshop. The extended abstracts will be made available online.

Extended abstracts and demonstration proposals should be submitted via THedu'15 easychair (https://www.easychair.org/conferences/?conf=thedu15).

Extended abstracts and demonstration proposals should be no more than 4 pages in length and are to be submitted in PDF format. They must conform to the EPTCS style guidelines (http://style.eptcs.org/).

At least one author of each accepted extended abstract/demonstration proposal is expected to attend THedu'15 and presents his/her extended abstract/demonstration.

Program Committee

    Francisco Botana, University of Vigo at Pontevedra, Spain
    Walther Neuper, Graz University of Technology, Austria (co-chair)
    Filip Maric, University of Belgrade, Serbia
    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

Informal Proceedings

Following ThEdu'13 and ThEdu'14 practise we expect to have a joint proceedings of the workshops co-located with Conferences on Intelligent Computer Mathematics.