Proving geometry theorems with rewrite rules
From MaRDI portal
Publication:1101255
DOI10.1007/BF02328448zbMath0642.68162MaRDI QIDQ1101255
William F. Schelter, Shang-Ching Chou
Publication date: 1986
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to geometry (51-04) Analytic and descriptive geometry (51N99)
Related Items
On the application of Buchberger's algorithm to automated geometry theorem proving, Proof-checking Euclid, Wu's method and its application to perspective viewing, Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle, On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving, A refutational approach to geometry theorem proving, A generalized Euclidean algorithm for geometry theorem proving, Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems, Automatic deduction in (dynamic) geometry: Loci computation, Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method, Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method, Self-evident automated geometric theorem proving based on complex number identity, Automated reducible geometric theorem proving and discovery by Gröbner basis method, Limits of theory sequences over algebraically closed fields and applications., Mechanical geometry theorem proving based on Gröbner bases, Geometric theorem proving by integrated logical and algebraic reasoning, Automated reasoning in differential geometry and mechanics using the characteristic set method. I: An improved version of Ritt-Wu's decomposition algorithm
Cites Work
