Published: 21st February 2012|
|Preface of the Program Committee|
|Towards an Intelligent Tutor for Mathematical Proofs Serge Autexier, Dominik Dietrich and Marvin Schiller||1|
|An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support Ralph-Johan Back and Johannes Eriksson||29|
|Automatic Deduction in Dynamic Geometry using Sage Francisco Botana and Miguel A. Abánades||49|
|Formalization and Implementation of Algebraic Methods in Geometry Filip Marić, Ivan Petrović, Danijela Petrović and Predrag Janičić||63|
|Automated Generation of User Guidance by Combining Computation and Deduction Walther Neuper||82|
|The GF Mathematics Library Jordi Saludes and Sebastian Xambó||102|
|Integrating DGSs and GATPs in an Adaptative and Collaborative Blended-Learning Web-Environment Vanda Santos and Pedro Quaresma||111|
|Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs Wolfgang Schreiner||124|
|Isabelle/PIDE as Platform for Educational Tools Makarius Wenzel and Burkhart Wolff||143|
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:
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.