Result: Automated theorem proving in incidence geometry : A bracket algebra based elimination method

Title:
Automated theorem proving in incidence geometry : A bracket algebra based elimination method
Authors:
HONGBO LI, YIHONG WU
Source:
ADG 2000 : automated deduction in geometry (Zurich, 25-27 September 2000, revised papers)Lecture notes in computer science. :199-227
Publisher Information:
Berlin: Springer, 2001.
Publication Year:
2001
Physical Description:
print, 22 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Mathematics, Mathématiques, Sciences exactes et technologie, Exact sciences and technology, Sciences et techniques communes, Sciences and techniques of general use, Mathematiques, Mathematics, Analyse mathématique, Mathematical analysis, Fonctions de plusieurs variables complexes et espaces analytiques, Several complex variables and analytic spaces, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Intelligence artificielle, Artificial intelligence, Résolution de problèmes, jeux, Problem solving, game playing, Démonstration automatique, Automatic proving, Demostración automática, Démonstration théorème, Theorem proving, Demostración teorema, Elimination, Eliminación, Equation biquadratique, Biquadratic equation, Ecuación de segundo grado, Evaluation performance, Performance evaluation, Evaluación prestación, Méthode heuristique, Heuristic method, Método heurístico, Méthode polynomiale, Polynomial method, Método polinomial
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Academy of Mathematics and System Sciences, Chinese Academy of Sciences, Beijing 100080, China
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14047690
Rights:
Copyright 2002 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems

Mathematics
Accession Number:
edscal.14047690
Database:
PASCAL Archive

Further Information

In this paper we propose a bracket algebra based elimination method for automated generation of readable proofs for theorems in incidence geometry. This method features three techniques, the first being heuristic automated reordering of geometric constructions for the purpose of producing shorter proofs, the second being some heuristic elimination rules which improve the performance of the area method of Zhang and others without introducing signed length ratios, the third being a simplification technique called contraction, which reduces the size of bracket polynomials. More than twenty theorems in incidence geometry have been proved, for which short proofs can be produced very fast, together with the corresponding nondegeneracy conditions. An interesting phenomenon is that a proof composed of polynomials of at most two terms can always be found for any of these theorems, similar to that by the biquadratic final polynomial method of Richter-Gebert.