Automated production of traditional proofs for constructive geometry theorems
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The authors present a method that can produce traditional proofs for a class of geometry statements whose hypotheses can be described constructively and whose conclusions can be represented by polynomial equations of three kinds of geometry quantities: ratios of lengths, areas of triangles, and Pythagoras differences of triangles. This class covers a large portion of the geometry theorems about straight lines and circles. The method involves the elimination of the constructed points from the conclusion using a few basic geometry propositions. The authors' program, Euclid, implements this method and can produce traditional proofs of many hard geometry theorems. Currently, it has produced proofs of 400 nontrivial theorems entirely automatically, and the proofs produced are generally short and readable. This method seems to be the first one to produce traditional proofs for hard geometry theorems efficiently.Keywords
This publication has 7 references indexed in Scilit:
- Proving geometry theorems with rewrite rulesJournal of Automated Reasoning, 1986
- Automated geometry theorem proving using Buchberger's algorithmPublished by Association for Computing Machinery (ACM) ,1986
- Geometry theorem proving using Hilbert's NullstellensatzPublished by Association for Computing Machinery (ACM) ,1986
- Proving Elementary Geometry Theorems Using Wu’s AlgorithmPublished by American Mathematical Society (AMS) ,1984
- On the Decision Problem and the Mechanization of Theorem-Proving in Elementary GeometryContemporary Mathematics, 1984
- Problems and Experiments for and with Automated Theorem-Proving ProgramsIEEE Transactions on Computers, 1976
- Plane geometry theorem proving using forward chainingArtificial Intelligence, 1975