Skip to main content
SpringerLink
Log in

From Tarski to Hilbert

  • Conference paper
Automated Deduction in Geometry (ADG 2012)

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

Included in the following conference series:

Abstract

In this paper, we report on the formal proof that Hilbert’s axiom system can be derived from Tarski’s system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabäuser, Szmielew and Tarski’s book: Metamathematische Methoden in der Geometrie. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

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. Review of Symbolic Logic 2, 700–768 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  2. Coq development team: The Coq Proof Assistant Reference Manual, Version 8.3. TypiCal Project (2010)

    Google Scholar 

  3. 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–324. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Paulson, L.C.: The Isabelle reference manual (2006)

    Google Scholar 

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

    Chapter  Google Scholar 

  6. Scott, P.: Mechanising hilbert’s foundations of geometry in isabelle. Master’s thesis, University of Edinburgh (2008)

    Google Scholar 

  7. Scott, P., Fleuriot, J.: An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol. 6877, pp. 182–200. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Tarski, A., Givant, S.: Tarski’s system of geometry. The Bulletin of Symbolic Logic 5(2) (June 1999)

    Google Scholar 

  9. Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer (1983) (in German)

    Google Scholar 

  10. Quaife, A.: Automated development of Tarski’s geometry. Journal of Automated Reasoning 5(1), 97–118 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  11. Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)

    Google Scholar 

  12. Guilhot, F.: Formalisation en Coq et visualisation d’un cours de géométrie pour le lycée. TSI 24, 1113–1138 (2005) (in French)

    Google Scholar 

  13. Pham, T.M.: Description formelle de propriété géométriques. PhD thesis, Université de Nice - Sophia-Antipolis (2011)

    Google Scholar 

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

    Google Scholar 

  15. Narboux, J.: A decision procedure for geometry in Coq. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 225–240. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Google Scholar 

  17. Janicic, P., Narboux, J., Quaresma, P.: The Area Method: a Recapitulation. Journal of Automated Reasoning 48(4), 489–532 (2012)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  19. Génevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu’s simple method in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 71–86. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Pham, T.-M., Bertot, Y., Narboux, J.: A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2011, Part IV. LNCS, vol. 6785, pp. 368–383. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ICube, UMR 7357, University of Strasbourg - CNRS, France

    Gabriel Braun & Julien Narboux

Authors
  1. Gabriel Braun
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Julien Narboux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, 1006, Laboratory of Advanced Research, University of Tsukuba, 305-8573, Tsukuba, Japan

    Tetsuo Ida

  2. School of Informatics, Informatics Forum, University of Edinburgh, 10 Crichton Street, EH8 9AB, Edinburgh, UK

    Jacques Fleuriot

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Braun, G., Narboux, J. (2013). From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds) Automated Deduction in Geometry. ADG 2012. Lecture Notes in Computer Science(), vol 7993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40672-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40672-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40671-3

  • Online ISBN: 978-3-642-40672-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation