Implementing Euclid's straightedge and compass constructions in type theory
DOI10.1007/S10472-018-9603-0zbMATH Open1479.03009OpenAlexW2893738687MaRDI QIDQ2631963FDOQ2631963
Robert Constable, Mark Bickford, Ariel Kellison
Publication date: 16 May 2019
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-018-9603-0
Recommendations
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Reading between the lines in constructive type theory
- The geometry of types
- Intersection types from a proof-theoretic perspective
- Working with Mathematical Structures in Type Theory
- Publication:4204148
- Expressing computational complexity in constructive type theory
- Constructing inductive-inductive types in cubical type theory
- Formalising Mathematics in Simple Type Theory
- Exploring abstract algebra in constructive type theory
Mechanization of proofs and logical operations (03B35) Intuitionistic mathematics (03F55) Elementary problems in Euclidean geometries (51M04) Type theory (03B38)
Cites Work
- Innovations in computational type theory using Nuprl
- A constructive theory of ordered affine geometry
- A common axiom set for classical and intuitionistic plane geometry
- The axioms of constructive geometry
- `Outside' as a primitive notion in constructive projective geometry
- A constructive real projective plane
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Mechanical Theorem Proving in Tarski’s Geometry
- Axioms and hulls
- Constructivity in Geometry
- Tarski's System of Geometry
- Title not available (Why is that?)
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- Logic of Ruler and Compass Constructions
- Programs as proofs: A synopsis
- A constructive version of Tarski's geometry
- Title not available (Why is that?)
- Brouwer and Euclid
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- OTTER Proofs in Tarskian Geometry
- Title not available (Why is that?)
Cited In (1)
Uses Software
This page was built for publication: Implementing Euclid's straightedge and compass constructions in type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2631963)
