Automatic geometry theorem-proving and automatic geometry problem-solving

DOI10.1007/3-540-47997-X_1MaRDI QIDQ4946075zbMATH OpenFDO

Authors Wen-tsün Wu

Publication date 30 September 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-47997-X_1

zbMATH Keywords

polynomial equation-solving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Polynomials in number theory (11C08) Computational aspects and applications of commutative rings (13P99)

Review text

The present paper surveys work of the author and his colleagues in the MMRC (Math. Mech. Res. Center, Chinese Acad. of Sciences), on the topic of a general method of polynomial equation-solving. There are three sections in the paper; the first one actually states the method, which is based on a particular ordering of a finite set of polynomials in \(n\) unknowns, together with a well-ordering principle and two decomposition theorems (for zeroes and varieties). Not a single clue about the proofs is given, for further information it is referred to papers by various authors, but they are not cited in the text. The use of a particular ordering in the set of polynomials resembles the use of Gröbner bases, which are told to be equivalent to a special case of the introduced theory. In the second section some applications and examples are stated. The approach is based on different `principle methods' derived from the well-ordering principle and the decomposition theorems above. Several examples of problems in geometry are presented, and their solution is given, acknowledging the use of the method of polynomial equation-solving. The paper ends with a long section on historical discussions on the relationship between geometrical theorem-proving and geometrical problem-solving from the ancient Chinese mathematicians to Descartes. For the entire collection see [Zbl 0929.00067].

Recommendations

• scientific article; zbMATH DE number 1601215
• scientific article; zbMATH DE number 1555236
• A refutational approach to geometry theorem proving
• scientific article; zbMATH DE number 41286
• Basic principles of mechanical theorem proving in elementary geometries

Cited in

(14)

• Euclidean geometry in terms of automata theory
• Automatic generation of staged geometric predicates
• A deductive database approach to automated geometry theorem proving and discovering
• The dimension method in elementary and differential geometry
• Automated deduction and knowledge management in geometry
• Automatically building diagrams for olympiad geometry problems
• Automatted geometry theorem proving
• Towards the Automatic Discovery of Theorems in GeoGebra
• Realization of automatic reasoning system of geometry based on point-eliminating method
• scientific article; zbMATH DE number 3926284 (Why is no real title available?)
• scientific article; zbMATH DE number 176215 (Why is no real title available?)
• scientific article; zbMATH DE number 2079840 (Why is no real title available?)
• Automated discovering and proving for geometric inequalities
• A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry

This page was built for publication: Automatic geometry theorem-proving and automatic geometry problem-solving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4946075)