|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:Theorem Proving in Infinitesimal Geometry |
| Authors:
Jacques Fleuriot
|
| Date: 2001 |
| Publication Title:Logic Journal of the IGPL |
| Publisher:OUP |
|
Publication Type:Journal Article
Publication Status:Published
|
|
Volume No:9(3)
Page Nos:471-498
|
|
DOI:10.1093/jigpal/9.3.447
|
- 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.
- Links To Paper
- Subscription Required
- Personal Page
- Bibtex format
- @Article{EDI-INF-RR-0482,
- 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 = {http://jigpal.oxfordjournals.org/cgi/reprint/9/3/447},
- }
|
