Proving geometry theorems with rewrite rules

DOI10.1007/BF02328448zbMATH Open0642.68162MaRDI QIDQ1101255FDOQ1101255

Authors: Shang-Ching Chou, William F. Schelter 

Publication date: 1986

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

Recommendations

• scientific article; zbMATH DE number 1303337
• Using geometric rewrite rules for solving geometric problems symbolically
• Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
• Automatted geometry theorem proving
• Proving and rewriting

zbMATH Keywords

geometry theorem provingrewrite rulesGröbner bases

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Analytic and descriptive geometry (51N99) Software, source code, etc. for problems pertaining to geometry (51-04)

Cites Work

• Graded algebras of global dimension 3
• Title not available (Why is that?)
• Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Non-negative integer basis algorithms for linear equations with integer coefficients

Cited In (24)

• Using geometric rewrite rules for solving geometric problems symbolically
• A refutational approach to geometry theorem proving
• Geometry machines: from AI to SMC
• Mechanical geometry theorem proving based on Gröbner bases
• Wu's method and its application to perspective viewing
• Self-evident automated geometric theorem proving based on complex number identity
• Proof-checking Euclid
• Limits of theory sequences over algebraically closed fields and applications.
• On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving
• 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
• Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
• On the application of Buchberger's algorithm to automated 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
• Geometric theorem proving by integrated logical and algebraic reasoning
• Title not available (Why is that?)
• A Geometric Procedure with Prover9
• Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle
• Automated reducible geometric theorem proving and discovery by Gröbner basis method
• Automated reasoning in differential geometry and mechanics using the characteristic set method. I: An improved version of Ritt-Wu's decomposition algorithm
• Ritt-Wu's decomposition algorithm and geometry theorem proving
• Rewriting input expressions in complex algebraic geometry provers
• Proving and rewriting
• Automatic deduction in (dynamic) geometry: Loci computation

This page was built for publication: Proving geometry theorems with rewrite rules

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