Published: 21st February 2012
DOI: 10.4204/EPTCS.79
ISSN: 2075-2180

EPTCS 79

Proceedings First Workshop on
CTP Components for Educational Software
Wrocław, Poland, 31th July 2011

Edited by: Pedro Quaresma and Ralph-Johan Back

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

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:

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:
Program Committee: