Automated proofs using bracket algebra with Cinderella and OpenMath

D.A. Roozemond

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademic


    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].
    Originele taal-2Engels
    TitelNinth Rhine Workshop on Computer Algebra (RWCA'04, Nijmegen, The Netherlands, March 25-26, 2004)
    StatusGepubliceerd - 2004

    Vingerafdruk Duik in de onderzoeksthema's van 'Automated proofs using bracket algebra with Cinderella and OpenMath'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit