\input zb-basic
\input zb-ioport
\iteman{io-port 01745042}
\itemau{Caferra, Ricardo; Peltier, Nicolas; Puitg, Fran\c{c}ois}
\itemti{Emphasizing human techniques in automated geometry theorem proving: A practical realization.}
\itemso{Richter-Gebert, J\"urgen (ed.) et al., Automated deduction in geometry. 3rd international workshop, ADG 2000, Z\"urich, Switzerland, September 25-27, 2000. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2061, 268-305 (2001).}
\itemab
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}}$ ({\bf H}uman {\bf O}riented {\bf A}utomated {\bf R}easoning on your {\bf D}esk) 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 {\it 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.
\itemrv{~}
\itemcc{}
\itemut{automated geometric reasoning; analogy; model (counter-example) building; proof structuring with diagrams; computer assisted learning}
\itemli{http://link.springer.de/link/service/series/0558/bibs/2061/20610268}
\end