Automated proofs using bracket algebra with Cinderella and OpenMath

D.A. Roozemond

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic


    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 [1], 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 [9]. 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 [8].
    Original languageEnglish
    Title of host publicationNinth Rhine Workshop on Computer Algebra (RWCA'04, Nijmegen, The Netherlands, March 25-26, 2004)
    Publication statusPublished - 2004


    Dive into the research topics of 'Automated proofs using bracket algebra with Cinderella and OpenMath'. Together they form a unique fingerprint.

    Cite this