Implementing Euclid's straightedge and compass constructions in type theory

DOI10.1007/s10472-018-9603-0zbMath1479.03009OpenAlexW2893738687MaRDI QIDQ2631963

Mark Bickford, Ariel Kellison, Robert L. Constable

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

zbMATH Keywords

constructive type theoryfoundations of geometryconstructive geometry

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Elementary problems in Euclidean geometries (51M04) Intuitionistic mathematics (03F55) Type theory (03B38)

Uses Software

• OTTER
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A constructive real projective plane
• A constructive version of Tarski's geometry
• Innovations in computational type theory using Nuprl
• Programs as proofs: A synopsis
• Axioms and hulls
• A constructive theory of ordered affine geometry
• A common axiom set for classical and intuitionistic plane geometry
• Brouwer and Euclid
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry
• Constructivity in Geometry
• Logic of Ruler and Compass Constructions
• OTTER Proofs in Tarskian Geometry
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Tarski's System of Geometry
• Mechanical Theorem Proving in Tarski’s Geometry
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS

This page was built for publication: Implementing Euclid's straightedge and compass constructions in type theory