A method for the mechanical derivation of formulas in elementary geometry

DOI10.1007/BF00243793MaRDI QIDQ1099656zbMATH OpenOpenAlexFDO

Authors Shang-Ching Chou

Publication date 1987

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00243793

zbMATH Keywords

geometry theorem provingGröbner basisRitt's decomposition algorithm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Symbolic computation and algebraic computation (68W30)

Review text

The author gives a method for proving theorems in elementary geometry, which is in the spirit of \textit{Wu Wen-tsün}'s method [Sci. Sin. 21, 157-172 (1978; Zbl 0376.68057)]. The problem consists in calculating a polynomial g under conditions, represented by zero conditions on other polynomials. Ritt's decomposition algorithm is applied to get all components general in set of variables by which the solution is to be expressed. Afterwards, the polynomial g is normalized by a Gröbner basis of the ideal generated by the components. The author shows, how to apply the method to get unknown constants in geometrical problems, as for example the radius of an inscribed circle in a triangle in terms of the three sides. Unfortunately, many information needed in this paper only exists in unpublished form (as in the proof of a theorem).

Recommendations

• scientific article; zbMATH DE number 4031634
• Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle
• scientific article; zbMATH DE number 41286
• scientific article; zbMATH DE number 3926285
• Ritt-Wu's decomposition algorithm and geometry theorem proving

Cited in

(9)

• Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle
• On the automatic derivation of a set of geometric formulae
• scientific article; zbMATH DE number 4031634 (Why is no real title available?)
• scientific article; zbMATH DE number 4050980 (Why is no real title available?)
• scientific article; zbMATH DE number 1145330 (Why is no real title available?)
• scientific article; zbMATH DE number 1390433 (Why is no real title available?)
• Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems
• Geometry machines: from AI to SMC
• On protocols for the automated discovery of theorems in elementary geometry

This page was built for publication: A method for the mechanical derivation of formulas in elementary geometry

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