Implementing Euclid's straightedge and compass constructions in type theory

DOI10.1007/S10472-018-9603-0MaRDI QIDQ2631963zbMATH OpenOpenAlexFDO

Authors Ariel Kellison, Mark Bickford, Robert 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

foundations of geometryconstructive type theoryconstructive geometry

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 3119278 (Why is no real title available?)
• scientific article; zbMATH DE number 3150814 (Why is no real title available?)
• scientific article; zbMATH DE number 3899653 (Why is no real title available?)
• scientific article; zbMATH DE number 9972 (Why is no real title available?)
• scientific article; zbMATH DE number 3206716 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• A common axiom set for classical and intuitionistic plane geometry
• A constructive real projective plane
• A constructive theory of ordered affine geometry
• A constructive version of Tarski's geometry
• Axioms and hulls
• Brouwer and Euclid
• Constructive geometry
• Constructivity in Geometry
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• Innovations in computational type theory using Nuprl
• Logic of Ruler and Compass Constructions
• Mechanical Theorem Proving in Tarski’s Geometry
• OTTER proofs in Tarskian geometry
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Programs as proofs: A synopsis
• Tarski's System of Geometry
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry

Cited in

(1)

• The axioms of constructive geometry

Describes a project that uses

Uses Software

• Nuprl
• OTTER

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)