Implementing Euclid’s straightedge and compass constructions in type theory
| Autor: | Ariel Kellison, Mark Bickford, Robert L. Constable |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Straightedge
Computer science Applied Mathematics Mathematics::History and Overview Proof assistant Nuprl 02 engineering and technology Intuitionistic type theory Predicate (mathematical logic) Constructive Type theory Artificial Intelligence Euclidean geometry 0202 electrical engineering electronic engineering information engineering Calculus 020201 artificial intelligence & image processing |
| Zdroj: | Annals of Mathematics and Artificial Intelligence. 85:175-192 |
| ISSN: | 1573-7470 1012-2443 |
| DOI: | 10.1007/s10472-018-9603-0 |
| Popis: | Constructions are central to the methodology of geometry presented in the Elements. This theory therefore poses a unique challenge to those concerned with the practice of constructive mathematics: can the Elements be faithfully captured in a modern constructive framework? In this paper, we outline our implementation of Euclidean geometry based on straightedge and compass constructions in the intuitionistic type theory of the Nuprl proof assistant. A result of our intuitionistic treatment of Euclidean geometry is a proof of the second proposition from Book I of the Elements in its full generality; a result that differs from other formally constructive accounts of Euclidean geometry. Our formalization of the straightedge and compass utilizes a predicate for orientation, which enables a concise and intuitive expression of Euclid’s constructions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink