Advertisement

Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2061)

Abstract

The underlying principles and main original techniques used in a running generic logic-based theorem prover are presented. The system (a prototype) is called HOARDATINF (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. HOARDATINF 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 HOARDATINF capabilities. One of these examples allows us to compare qualitatively our approach with that of a powerful prover described in a recent paper [8]. Some directions of future research are mentioned.

Keywords

Automated geometric reasoning analogy model (counter-example) building proof structuring with diagrams computer assisted learning 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    N. Balacheff. Apprendre la preuve. In J. Sallantin and J.-J. Szczeniarz (eds.), Le concept de preuve à la lumière de l’intelligence artificielle, pages 197–236. PUF, Paris, 1999.Google Scholar
  2. 2.
    W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1–35, 1977.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    C. Bourely, G. Défourneaux, and N. Peltier. Building proofs or counterexamples by analogy in a resolution framework. In Proceedings of JELIA 96, LNAI 1126, pages 34–49. Springer, 1996.Google Scholar
  4. 4.
    R. Caferra and M. Herment. A generic graphic framework for combining inference tools and editing proofs and formulae. Journal of Symbolic Computation, 19(2):217–243, 1995.zbMATHCrossRefGoogle Scholar
  5. 5.
    R. Caferra, M. Herment, and N. Zabel. User-oriented theorem proving with the ATINF graphic proof editor. In Fundamentals of Artificial Intelligence Research, LNCS 535, pages 2–10. Springer, 1991.Google Scholar
  6. 6.
    R. Caferra and N. Peltier. Extending semantic resolution via automated model building: Applications. In Proceeding of IJCAI’95, pages 328–334. Morgan Kaufman, 1995.Google Scholar
  7. 7.
    R. Caferra and N. Peltier. Disinference rules, model building and abduction. Logic at Work. Essays dedicated to the memory of Helena Rasiowa (Part 5: Logic in Computer Science, Chap. 20). Physica-Verlag, 1998.Google Scholar
  8. 8.
    S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3):219–246, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    S.-C. Chou. Mechanical Geometry Theorem Proving. Mathematics and its Applications. D. Reidel, 1988.Google Scholar
  10. 10.
    H. Coelho and L. Moniz Pereira. Automated reasoning in geometry theorem proving with Prolog. Journal of Automated Reasoning, 2(4):329–390, 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    G. Défourneaux, C. Bourely, and N. Peltier. Semantic generalizations for proving and disproving conjectures by analogy. Journal of Automated Reasoning, 20(1-2):27–45, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    G. Défourneaux and N. Peltier. Analogy and abduction in automated reasoning. In M. E. Pollack (ed.), Proceedings of IJCAI’97, pages 216–225. Morgan Kaufmann, 1997.Google Scholar
  13. 13.
    G. Défourneaux and N. Peltier. Partial matching for analogy discovery in proofs and counter-examples. In W. McCune (ed.), Proceedings of CADE-14, LNAI 1249, pages 431–445. Springer, 1997.Google Scholar
  14. 14.
    C. Fermüller and A. Leitsch. Decision procedures and model building in equational clause logic. Journal of the IGPL, 6(1):17–41, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    H. Gelernter, J. Hansen, and D. Loveland. Empirical explorations of the geometry theorem-proving machine. In J. Siekmann and G. Wrightson (eds.), Automation of Reasoning, vol. 1, pages 140–150. Springer, 1983. Originally published in 1960.Google Scholar
  16. 16.
    H. Hong, D. Wang, and F. Winkler. Algebraic Approaches to Geometric Reasoning. Special issue of the Annals of Mathematics and Artificial Intelligence 13 (1–2). Baltzer, Amsterdam, 1995.Google Scholar
  17. 17.
    J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559–587, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    D. Kapur and J. E. Mundy. Geometric Reasoning. MIT Press, 1989.Google Scholar
  19. 19.
    A. Leitsch. The Resolution Calculus. Texts in Theoretical Computer Science. Springer, 1997.Google Scholar
  20. 20.
    V. Luengo. A semi-empirical agent for learning mathematical proof. In S. P. Lajoie and M. Vivet (eds.), Artificial Intelligence and Education, pages 475–482. IOS Press, Amsterdam, 1999.Google Scholar
  21. 21.
    V. Luengo. Cabri-Euclide: Un micromonde de preuve intégrant la réfutation. Thèse de doctorat, I.N.P.G., France, Septembre 1997.Google Scholar
  22. 22.
    N. Peltier. Combining resolution and enumeration for finite model building. In P. Baumgartner and H. Zhang (eds.), FTP’00 (Third International Workshop on First-Order Theorem Proving), St-Andrews, Scotland, pages 170–181. Technical Report, Universität Koblenz-Landau, July 2000.Google Scholar
  23. 23.
    N. Peltier. On the decidability of the PVD class with equality. Technical report, LEIBNIZ Laboratory, 2000. To appear in the Logic Journal of the IGPL.Google Scholar
  24. 24.
    D. A. Plaisted and Y. Zhu. Ordered semantic hyperlinking. Journal of Automated Reasoning, 25(3):167–217, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    G. Polya. How to Solve It: A New Aspect of Mathematical Method (second edition). Princeton University Press, 1973.Google Scholar
  26. 26.
    F. Puitg and J.-F. Dufourd. Formal specifications and theorem proving breakthroughs in geometric modelling. In Theorem Proving in Higher-Order Logics, LNCS 1479, pages 401–422. Springer, 1998.CrossRefGoogle Scholar
  27. 27.
    F. Puitg and J.-F. Dufourd. Formalizing mathematics in higher-order logic: A case study in geometric modelling. Theoretical Computer Science, 234:1–57, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  28. 28.
    A. Quaife. Automated development of Tarski’s geometry. Journal of Automated Reasoning, 5:97–118, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    T. Recio and M. Vélez. Automatic discovery of theorems in elementary geometry. Journal of Automated Reasoning, 23(1):63–82, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  30. 30.
    R. Reiter. A semantically guided deductive system for automatic theorem proving. IEEE Transactions on Computers, C-25(4):328–334, 1976.CrossRefMathSciNetGoogle Scholar
  31. 31.
    J. Richter-Gebert and U. Kortenkamp. The Interactive Geometry Software Cinderella. Springer, 2000.Google Scholar
  32. 32.
    M. Rusinowitch. Démonstration automatique par des techniques de réécriture. Thèse d’état, Université Nancy 1, France, 1987. Also available as textbook, Inter Editions, Paris, 1989.Google Scholar
  33. 33.
    J. R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687–697, 1967.zbMATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    J. Slaney. scott: A model-guided theorem prover. In Proceedings IJCAI-93, vol. 1, pages 109–114. Morgan Kaufmann, 1993.Google Scholar
  35. 35.
    L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, 1988.Google Scholar
  36. 36.
    L. Wos, R. Overbeek, E. Lush, and J. Boyle. Automated Reasoning: Introduction and Applications (second edition). McGraw-Hill, 1992.Google Scholar
  37. 37.
    L. Wos, G. Robinson, and D. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12:536–541, 1965.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  1. 1.Laboratoire LEIBNIZ-IMAGGrenoble CedexFrance

Personalised recommendations