Using geometric rewrite rules for solving geometric problems symbolically
type: Item
instance of: scholarly article
title: Using geometric rewrite rules for solving geometric problems symbolically
zbMATH Open document ID: 0795.68175
DOI: 10.1016/0304-3975(93)90324-M
author: Beat Brüderlin
published in: Theoretical Computer Science
publication date: 1993-10-25T00:00:00Z
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.
reviewed by: Marius Zimand
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 417328
zbMATH Keywords: computer aided design
zbMATH Keywords: rewrite rule system
zbMATH Keywords: compass and ruler construction
zbMATH Keywords: congruence relation
MaRDI profile type: Publication
cites work: Algebraic simplification
cites work: Automated reasoning in geometry theorem proving with Prolog
cites work: Q4079605
cites work: Q4385532
cites work: Q3661541
cites work: A note on syntactic symmetry and the manipulation of formal systems by machine
cites work: A refutational approach to geometry theorem proving
cites work: Q5581665
cites work: Q5807665
cites work: Basic principles of mechanical theorem proving in elementary geometries
description: scientific article; zbMATH DE number 417328