This paper describes the results of a project intended to make it possible to put forward geometrical theorems by pointing and clicking, and then obtain a proof for that theorem automatically. This goal was achieved by adding various options to Cinderella , a computer program with which one can create geometrical configurations. Its internal ‘Randomized prover’ is able to discover theorems automatically. In the project the functionality was added to find proofs for these theorems with the aid of the computer algebra package GAP . Communication between these two programs and the various steps in generating the proof is done by means of OpenMath [5, 7]. The proofs are represented by bracket calculations as proposed in .
|Title of host publication||Ninth Rhine Workshop on Computer Algebra (RWCA'04, Nijmegen, The Netherlands, March 25-26, 2004)|
|Publication status||Published - 2004|