Preface of the Program Committee

The reader is welcome to the post-proceedings of THedu'11, a workshop associated to CADE 23, July 31 2011, Wrocław, Poland. The workshop gathered the research communities for Computer Theorem proving (CTP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS) and Dynamic Geometry Systems (DGS). The workshop tried 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). Elements for next-generation MMA's include:

• Declarative Languages for Problem Solution: education in applied sciences and in engineering is mainly concerned with problems, which are understood as operations on elementary objects to be transformed to an object representing a problem solution. Preconditions and postconditions of these operations can be used describe the possible steps in the problem space; thus, ATP-systems can be used to check if an operation sequence given by the user does actually present a problem solution. Such "Problem Solution Languages" encompass declarative proof languages like Isabelle/Isar or Coq's Mathematical Proof Language, but also more specialized forms such as, for example, geometric problem solution languages that express a proof argument in Euklidian Geometry or languages for graph theory.
• Consistent Mathematical Content Representation: Libraries of existing ITP-Systems, in particular those following the LCF-prover paradigm, usually provide logically coherent and human readable knowledge. In the leading provers, mathematical knowledge is covered to an extent beyond most courses in applied sciences. However, the potential of this mechanised knowledge for education is clearly not yet recognised adequately: renewed pedagogy calls for inquiry-based learning from concrete to abstract --- and the knowledge's logical coherence supports such learning: for instance, the formula 2·π depends on the definition of reals and of multiplication; close to these definitions are the laws like commutativity etc. However, the complexity of the knowledge's traceable interrelations poses a challenge to usability design.
• User-Guidance in Stepwise Problem Solving: Such guidance is indispensable for independent learning, but costly to implement so far, because so many special cases need to be coded by hand. However, CTP technology makes automated generation of user-guidance reachable: declarative languages as mentioned above, novel programming languages combining computation and deduction, methods for automated construction with ruler and compass from specifications, etc --- all these methods 'know how to solve a problem'; so, use the methods' knowledge to generate user-guidance mechanically, is an appealing challenge for ATP and ITP, and probably for compiler construction!

These three points identify the common grounds of the contributions to the post-proceedings at hand. The contributions comprise a wide range of MMAs from proving to calculating (and even hiding CTP completely), from engineering to software technology, even to geometry --- a variety showing a field far from being settled.

So, the PC hopes that this publication will appear as the cradle of a new generation of educational mathematics software in a few years, attracting further researchers in the field already in THedu'12 --- the vision is, from the present point of view, for MMAs being models of mathematics: The challenge addressed by this workshop series is to provide appealing models which are interactive and which explain themselves such that interested students can independently learn by inquiry and experimentation.

The Program Committee and THedu Board:

Chairs:

• Ralf-Johan Back, Åbo University, Finland
• Pedro Quaresma, University of Coimbra, Portugal

Program Committee:

• Francisco Botana, University of Vigo at Pontevedra, Spain
• Florian Haftmann, Munich University of Technology, Germany
• Predrag Janičić, University of Belgrade, Serbia
• Cezary Kaliszyk, University of Tsukuba, Japan
• Filip Marić, University of Belgrade, Serbia
• Julien Narboux, University of Strasbourg, France
• Walther Neuper, Graz University of Technology, Austria
• Wolfgang Schreiner, Johannes Kepler University, Linz, Austria
• Laurent Théry, Sophia Antipolis, INRIA, France
• Makarius Wenzel, University Paris-Sud, France
• Burkhart Wolff, University Paris-Sud, France