Emphasizing human techniques in automated geometry theorem proving: A practical realization.

*(English)*Zbl 0985.68058
Richter-Gebert, Jürgen (ed.) et al., Automated deduction in geometry. 3rd international workshop, ADG 2000, Zürich, Switzerland, September 25-27, 2000. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2061, 268-305 (2001).

Summary: The underlying principles and main original techniques used in a running generic logic-based theorem prover are presented. The system (a prototype) is called \(\text{HOARD}_{\text{ATINF}}\) (Human Oriented Automated Reasoning on your Desk) and has been specialized in this work to proof learning through geometry. It is based on a new calculus, particularly suited to the class of problems we deal with. The calculus allows treatment of equality and automatic model building. \(\text{HOARD}_{\text{ATINF}}\) has some other original characteristics such as proving by analogy (using matching techniques), some possibilities of discovering lemmata (using diagrams), handling standard theories in geometry such as commutativity and symmetry (by encoding them in the unification algorithm used by the calculus), and proof verification in a rather large sense (by using capabilities of the calculus).

As this work is intended to set theoretical bases of a new logic-based approach to geometry theorem proving, a comparison of features of our system with respect to those of other important, representative logic-based systems is given. Some running examples give a good taste of the \(\text{HOARD}_{\text{ATINF}}\) capabilities. One of these examples allows us to compare qualitatively our approach with that of a powerful prover described in a recent paper. Some directions of future research are mentioned.

For the entire collection see [Zbl 0971.00045].

As this work is intended to set theoretical bases of a new logic-based approach to geometry theorem proving, a comparison of features of our system with respect to those of other important, representative logic-based systems is given. Some running examples give a good taste of the \(\text{HOARD}_{\text{ATINF}}\) capabilities. One of these examples allows us to compare qualitatively our approach with that of a powerful prover described in a recent paper. Some directions of future research are mentioned.

For the entire collection see [Zbl 0971.00045].

##### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

68U05 | Computer graphics; computational geometry (digital and algorithmic aspects) |

03B35 | Mechanization of proofs and logical operations |