Theorem Proving in Infinitesimal Geometry

Research output: Contribution to journalArticlepeer-review

Abstract

This paper describes some of the work done in our formal investigation of concepts and properties that arise when infinitely small and infinite notions are introduced in a geometry theory. An algebraic geometry theory is developed in the theorem prover Isabelle using real and hyperreal vectors. We use this to investigate some new geometric relations as well as ways of rigorously mechanizing geometric proofs that involve infinitesimal and infinite arguments. We follow a strictly definitional approach and build our theory of vectors within the nonstandard analysis framework developed in Isabelle.
Original languageEnglish
Pages (from-to)447-474
Number of pages28
JournalLogic Journal of the Interest Group in Pure and Applied Logic
Volume9
Issue number3
DOIs
Publication statusPublished - 2001

Fingerprint

Dive into the research topics of 'Theorem Proving in Infinitesimal Geometry'. Together they form a unique fingerprint.

Cite this