ISSN:
1573-0670
Keywords:
automated reasoning
;
automated geometry theorem proving
;
area method
;
multiple proof
;
shortest proof
;
68T15
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract In this series of papers, we discuss how to use a fixed set of high level geometry lemmas or rules related to geometric invariants, such as area, full-angle, etc., to produce short and human-readable proofs in geometry, especially to produce multiple and shortest proofs of a given geometry theorem. These rules are proved to be much more effective and concise than the rules based on triangle congruence used in related work before. The success of our approach is partially due to a skillful selection of geometric invariants and the related rules. Control and search strategies are proposed and experimented with to enhance the efficiency of the pover. In part I of this series, the high level geometry lemmas are about area and the Ceva-Menelaus configurations.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00283133
Permalink
