Using geometric rewrite rules for solving geometric problems symbolically

DOI10.1016/0304-3975(93)90324-MMaRDI QIDQ685375zbMATH OpenFDO

Authors Beat Brüderlin

Publication date 25 October 1993

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(93)90324-M

zbMATH Keywords

compass and ruler constructioncomputer aided designcongruence relationrewrite rule system

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Symbolic computation and algebraic computation (68W30)

Review text

The paper develops a rewrite rule system operating on geometric predicates. The system is able to derive symbolic prescriptions for compass and ruler construction of configurations satisfying given constraints and to reason about congruence relation. Completeness and termination of the system are obtained by making the set of rewrite rules locally confluent and by introducing a simple, well-founded ordering of the terms of language. While the system is not fully presented (we assume this is realized in the author's thesis), enough details are given to make the reader fell how it works and what its capabilities are.

Recommendations

• scientific article; zbMATH DE number 194597
• Proving geometry theorems with rewrite rules
• scientific article; zbMATH DE number 1303337
• Geometric constraint solving with geometric transformation
• Solving geometry problems using a combination of symbolic and numerical reasoning

Cites work

• A note on syntactic symmetry and the manipulation of formal systems by machine
• A refutational approach to geometry theorem proving
• Algebraic simplification
• Automated reasoning in geometry theorem proving with Prolog
• Basic principles of mechanical theorem proving in elementary geometries
• scientific article; zbMATH DE number 3813580 (Why is no real title available?)
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)

Cited in

(6)

• Proving geometry theorems with rewrite rules
• Tolerances in geometric constraint problems
• Finding the Symbolic Solution of a Geometric Problem Through Numerical Computations
• Solving geometry problems using a combination of symbolic and numerical reasoning
• scientific article; zbMATH DE number 194597 (Why is no real title available?)
• A formalization of geometric constraint systems and their decomposition

This page was built for publication: Using geometric rewrite rules for solving geometric problems symbolically

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