Automated proofs using bracket algebra with Cinderella and OpenMath

D.A. Roozemond

Automated proofs using bracket algebra with Cinderella and OpenMath

D.A. Roozemond

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

Abstract

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 language	English
Title of host publication	Ninth Rhine Workshop on Computer Algebra (RWCA'04, Nijmegen, The Netherlands, March 25-26, 2004)
Publication status	Published - 2004

Cite this

@inproceedings{d0081652d49548f3b5f22d415be186de,

title = "Automated proofs using bracket algebra with Cinderella and OpenMath",

abstract = "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 {\textquoteleft}Randomized prover{\textquoteright} 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].",

author = "D.A. Roozemond",

year = "2004",

language = "English",

booktitle = "Ninth Rhine Workshop on Computer Algebra (RWCA'04, Nijmegen, The Netherlands, March 25-26, 2004)",

}

TY - GEN

T1 - Automated proofs using bracket algebra with Cinderella and OpenMath

AU - Roozemond, D.A.

PY - 2004

Y1 - 2004

N2 - 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].

AB - 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].

M3 - Conference contribution

BT - Ninth Rhine Workshop on Computer Algebra (RWCA'04, Nijmegen, The Netherlands, March 25-26, 2004)

ER -

Automated proofs using bracket algebra with Cinderella and OpenMath

Abstract

Fingerprint

Cite this