Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Theorem Proving in Infinitesimal Geometry
Authors: Jacques Fleuriot
Date: 2001
Publication Title:Logic Journal of the IGPL
Publication Type:Journal Article Publication Status:Published
Volume No:9(3) Page Nos:471-498
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.
Links To Paper
Subscription Required
Personal Page
Bibtex format
author = { Jacques Fleuriot },
title = {Theorem Proving in Infinitesimal Geometry},
journal = {Logic Journal of the IGPL},
publisher = {OUP},
year = 2001,
volume = {9(3)},
pages = {471-498},
doi = {10.1093/jigpal/9.3.447},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh