Skip to main content
View expanded cover

International Workshop on Automated Deduction in Geometry

ADG 2010: Automated Deduction in Geometry pp 201–220Cite as

A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

  • Conference paper

Part of the Lecture Notes in Computer Science book series (LNAI,volume 6877)

Abstract

We present a theorem prover ArgoCLP based on coherent logic that can be used for generating both readable and formal (machine verifiable) proofs in various theories, primarily geometry. We applied the prover to various axiomatic systems and proved tens of theorems from standard university textbooks on geometry. The generated proofs can be used in different educational purposes and can contribute to the growing body of formalized mathematics. The system can be used, for instance, in showing that modifications of some axioms do not change the power of an axiom system. The system can also be used as an assistant for proving appropriately chosen subgoals of complex conjectures.

This work has been partly supported by the grant 174021 of the Ministry of Science of Serbia and by the SNF SCOPES grant IZ73Z0_127979/1.

This is a preview of subscription content, access via your institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • DOI: 10.1007/978-3-642-25070-5_12
  • Chapter length: 20 pages
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
eBook
USD   54.99
Price excludes VAT (USA)
  • ISBN: 978-3-642-25070-5
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
Softcover Book
USD   69.99
Price excludes VAT (USA)
Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. The Review of Symbolic Logic (2009)

    Google Scholar 

  2. Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 246–260. Springer, Heidelberg (2005)

    CrossRef  Google Scholar 

  3. Bezem, M., Hendriks, D.: On the Mechanization of the Proof of Hessenberg’s Theorem in Coherent Logic. Journal of Automated Reasoning 40(1) (2008)

    Google Scholar 

  4. Borsuk, K., Szmielew, W.: Foundations of Geometry. Norht-Holland Publishing Company, Amsterdam (1960)

    MATH  Google Scholar 

  5. Buchberger, B.: An Algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal. PhD thesis. University of Innsbruck (1965)

    Google Scholar 

  6. Buchberger, B., et al.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic (2006)

    Google Scholar 

  7. Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1988)

    MATH  Google Scholar 

  8. Chou, S.-C., Gao, X.-S.: Automated reasoning in geometry. In: Handbook of Automated Reasoning. Elsevier (2001)

    Google Scholar 

  9. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)

    CrossRef  MATH  Google Scholar 

  10. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated production of traditional proofs for constructive geometry theorems. In: IEEE Symposium on Logic in Computer Science LICS. IEEE Computer Society Press (1993)

    Google Scholar 

  11. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, II. theorem proving with full-angles. Journal of Automated Reasoning 17 (1996)

    Google Scholar 

  12. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal Automated Reasoning 25(3) (2000)

    Google Scholar 

  13. Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in hilbert’s elementary geometry. In: Richter-Gebert, J., Wang, D. (eds.) ADG 2000. LNCS (LNAI), vol. 2061, pp. 306–323. Springer, Heidelberg (2001)

    CrossRef  Google Scholar 

  14. Duprat, J.: Une axiomatique de la géométrie plane en coq. In: Actes des JFLA 2008, INRIA (2008)

    Google Scholar 

  15. Fisher, J., Bezem, M.: Skolem Machines and Geometric Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 201–215. Springer, Heidelberg (2007)

    CrossRef  Google Scholar 

  16. Gelernter, H., Hanson, J.R., Loveland, D.W.: Empirical explorations of the geometry-theorem proving machine. In: Computers and Thought. MIT Press (1995)

    Google Scholar 

  17. Guilhot, F.: Formalisation en coq d’un cours de géométrie pour le lycée. Journées Francophones des Langages Applicatifs (2004)

    Google Scholar 

  18. Harrison, J.: Hol light: A Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)

    CrossRef  Google Scholar 

  19. Heath, T.L.: The Thirteen Books of Euclid’s Elements. Dover Publications, New-York (1956)

    MATH  Google Scholar 

  20. Hilbert, D.: Grundlagen der Geometrie, Leipzig (1899)

    Google Scholar 

  21. Janičić, P., Kordić, S.: EUCLID — the geometry theorem prover. FILOMAT 9(3) (1995)

    Google Scholar 

  22. Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution. Coq V5.10 (1995)

    Google Scholar 

  23. Kapur, D.: Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation 2(4) (1986)

    Google Scholar 

  24. Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane Geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol. 6301, pp. 141–162. Springer, Heidelberg (2011)

    CrossRef  Google Scholar 

  25. Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues’ theorem in Coq using ranks. In: ACM Symposium on Applied Computing. ACM (2009)

    Google Scholar 

  26. Meikle, L.I., Fleuriot, J.D.: Formalizing Hilbert’s Grundlagen in Isabelle/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 319–334. Springer, Heidelberg (2003)

    CrossRef  Google Scholar 

  27. Narboux, J.: Formalisation et automatisation du raisonnement géométrique en Coq. PhD thesis. Université Paris Sud (2006)

    Google Scholar 

  28. Narboux, J.: Mechanical theorem proving in tarski’s geometry. In: Botana, F., Recio, T. (eds.) ADG 2006. LNCS (LNAI), vol. 4869, pp. 139–156. Springer, Heidelberg (2007)

    CrossRef  Google Scholar 

  29. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  30. von Plato, J.: The axioms of constructive geometry. Annals of Pure and Applied Logic 76 (1995)

    Google Scholar 

  31. von Plato, J.: Formalization of Hilbert’s geometry of incidence and parallelism. Synthese 110 (1997)

    Google Scholar 

  32. Polonsky, A.: Proofs, Types, and Lambda Calculus. PhD thesis. University of Bergen (2011)

    Google Scholar 

  33. Quaife, A.: Automated development of Tarski’s geometry. Journal of Automated Reasoning 5(1) (1989)

    Google Scholar 

  34. Schwabhuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)

    CrossRef  MATH  Google Scholar 

  35. Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4) (2009)

    Google Scholar 

  36. Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. Journal of ACM 22(2) (1975)

    Google Scholar 

  37. Tarski, A.: What is elementary geometry? In: The Axiomatic Method, with Special Reference to Geometry and Physics. North-Holland (1959)

    Google Scholar 

  38. The Coq development team. The Coq proof assistant reference manual, Version 8.2. TypiCal Project (2009)

    Google Scholar 

  39. Trybulec, A.: Mizar. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol. 3600, pp. 20–23. Springer, Heidelberg (2006)

    CrossRef  Google Scholar 

  40. Wenzel, M.T.: Isar - a Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999)

    CrossRef  Google Scholar 

  41. Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica 21 (1978)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics, University of Belgrade, Studentski trg 16, 11000, Belgrade, Serbia

    Sana Stojanović, Vesna Pavlović & Predrag Janičić

Authors
  1. Sana Stojanović
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vesna Pavlović
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Predrag Janičić
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LSIIT, Pôle API, Boulevard Sébastien Brant, BP 10413, 67412, Illkirch Cédex, France

    Pascal Schreck & Julien Narboux & 

  2. Technische Universität München, Zentrum Mathematik (M10), Lehrstuhl für Geometrie und Visualisierung, Boltzmannstraße 3, 85748, Garching, Germany

    Jürgen Richter-Gebert

Rights and permissions

Reprints and Permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stojanović, S., Pavlović, V., Janičić, P. (2011). A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-25070-5_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-25069-9

  • Online ISBN: 978-3-642-25070-5

  • eBook Packages: Computer ScienceComputer Science (R0)