Skip to main content
SpringerLink
Log in

Nonstandard Geometric Proofs

  • Conference paper
  • First Online:
Automated Deduction in Geometry (ADG 2000)

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

Included in the following conference series:

Abstract

This paper describes ongoing work in our formal investigation of some of the concepts and properties that arise when infinitesimal notions are introduced in a geometry theory. An algebraic geometry theory is developed in the theorem prover Isabelle using hyperreal vectors. We follow a strictly definitional approach and build our theory of vectors within the nonstandard analysis (NSA) framework developed in Isabelle. We show how this theory can be used to give intuitive, yet rigorous, nonstandard proofs of standard geometric theorems through the use of infinitesimal and infinite geometric quantities.

Acknowledgement

This research was funded by EPSRC grant GR/M45030 ‘Computational Modelling of Mathematical Reasoning’. I would like to thank the anonymous referees for their insightful comments.

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 54.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. M. E. Baron. The Origins of the Infinitesimal Calculus. Pergammon Press, 1969.

    Google Scholar 

  2. R. S. Boyer and J. S. Moore. A Computational Logic. ACM Monograph Series. ACM Press, 1979.

    Google Scholar 

  3. A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction-CADE-9, volume 310 of Lecture Notes in Computer Science, pages 111–120. Springer-Verlag, May 1988.

    Chapter  Google Scholar 

  4. S. C. Chou, X. S. Gao, and J. Z. Zhang. Automated geometry theorem proving by vector calculation. In ACM-ISSAC, Kiev, Ukraine, July 1993, pages 284–291. ACM Press, 1993.

    Google Scholar 

  5. S. C. Chou, X. S. Gao, and J. Z. Zhang. Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation. Journal of Automated Reasoning, 17:325–347, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. S. C. Chou, X. S. Gao, and J. Z. Zhang. Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. Journal of Automated Reasoning, 17:349–370, 1996.

    MATH  MathSciNet  Google Scholar 

  7. P. J. Davis and R. Hersh. The Mathematical Experience. Harmondsworth, Penguin, 1983.

    Google Scholar 

  8. J. Dieudonné. Linear Algebra and Geometry. Hermann, 1969. Translated from the original French text Algèbre linéaire et géométrie élémentaire.

    Google Scholar 

  9. S. Fevre and D. Wang. Proving geometric theorems using Clifford algebra and rewrite rules. In C. Kirchner and H. Kirchner, editors, Automated Deduction-CADE-15, volume 1421 of Lecture Notes in Artificial Intelligence, pages 17–32. Springer-Verlag, July 1998.

    Google Scholar 

  10. J. D. Fleuriot. On the mechanization of real analysis in Isabelle/HOL. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 146–162. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  11. J. D. Fleuriot and L. C. Paulson. A combination of geometry theorem proving and nonstandard analysis, with application to Newton’s Principia. In C. Kirchner and H. Kirchner, editors, Automated Deduction-CADE-15, volume 1421 of Lecture Notes in Artificial Intelligence, pages 3–16. Springer-Verlag, July 1998.

    Google Scholar 

  12. J. D. Fleuriot and L. C. Paulson. Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. In X.-S. Gao, D. Wang, and L. Yang, editors, Automated Deduction in Geometry, volume 1669 of Lecture Notes in Artificial Intelligence, pages 47–66. Springer-Verlag, 1999.

    Google Scholar 

  13. J. D. Fleuriot and L. C. Paulson. Mechanizing nonstandard real analysis. LMS Journal of Computation and Mathematics, 3:140–190, 2000.

    MATH  MathSciNet  Google Scholar 

  14. M. Gordon and T. Melham. Introduction to HOL: A theorem proving environment for Higher Order Logic. Cambridge U niversity Press, 1993.

    MATH  Google Scholar 

  15. John Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Also published as technical report 408 of the Computer Laboratory, University of Cambridge, 1996.

    Google Scholar 

  16. D. Kapur and M. Subramaniam. Lemma discovery in automating induction. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction-CADE-13, volume 1104 of Lecture Notes in Artificial Intelligence, pages 538–552. Springer-Verlag, August 1996.

    Google Scholar 

  17. H. J. Keisler. Foundations of Infinitesimal Calculus. Prindle, Weber & Schmidt, 1976.

    Google Scholar 

  18. W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, 1994.

    Google Scholar 

  19. L. C. Paulson. Isabelle’s object-logics. Technical Report 286, Computer Laboratory, University of Cambridge, February 1998.

    Google Scholar 

  20. A. Robinson. Non-standard Analysis. North-Holland, 1980.

    Google Scholar 

  21. D. Wang. Clifford algebraic calculus for geometric reasoning, with application to computer vision. In D. Wang, R. Caferra, L. Fariñas del Cerro, and H. Shi, editors, Automated Deduction in Geometry, ADG’96, volume 1360 of Lecture Notes in Artificial Intelligence, pages 115–140. Springer-Verlag, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Division of Informatics, University of Edinburgh, 80 South Bridge, Edinburgh, EH1 1HN

    Jacques D. Fleuriot

Authors
  1. Jacques D. Fleuriot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Zentrum Mathematik, SB4, Technische Universität München, 80290, München, Germany

    Jürgen Richter-Gebert

  2. Laboratoire d’Informatique de Paris 6, Université Pierre et Marie Curie — CNRS, 4 place Jussieu, 75252, Paris Cedex 05, France

    Dongming Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fleuriot, J.D. (2001). Nonstandard Geometric Proofs. In: Richter-Gebert, J., Wang, D. (eds) Automated Deduction in Geometry. ADG 2000. Lecture Notes in Computer Science(), vol 2061. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45410-1_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-45410-1_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42598-4

  • Online ISBN: 978-3-540-45410-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation