Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

DOI10.1007/s10817-017-9422-8zbMath1441.03011OpenAlexW2741938952MaRDI QIDQ1725841

Pascal Schreck, Pierre Boutry, Julien Narboux, Charly Gries

Publication date: 15 February 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01178236/file/parallel_postulates_revised.pdf

zbMATH Keywords

classificationTarskiHilbertCoqEuclidparallel postulateformalizationfoundations of geometryArchimedes' axiomLotschnittaxiomneutral geometryAristotle's axiomdecidability of intersectionSaccheri-Legendre theoremsum of angles

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Foundations of classical theories (including reverse mathematics) (03B30) Absolute planes in metric geometry (51F05) Euclidean geometries (general) and generalizations (51M05) Intuitionistic mathematics (03F55) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (7)

Implementing Euclid's straightedge and compass constructions in type theory ⋮ Proof-checking Euclid ⋮ Euclid after Computer Proof-Checking ⋮ Tarski geometry axioms. IV: Right angle ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ The ubiquitous axiom ⋮ Theorem proving as constraint solving with coherent logic

Uses Software

• Coq
• GeoCoq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A constructive version of Tarski's geometry
• Another equivalent of the Lotschnittaxiom
• Strasbourg master class on geometry
• Aristotle's axiom in the foundations of geometry
• Die Modelle des Hilbertschen Axiomensystems der absoluten Geometrie
• On the stepwise construction of the parallel postulate
• A set of postulates for plane geometry, based on scale and protractor
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Formalizing complex plane geometry
• A synthetic proof of Pappus' theorem in Tarski's geometry
• On the equivalence of Lagrange's axiom to the Lotschnittaxiom
• Zur Parallelenfrage
• HERBRAND’S THEOREM AND NON-EUCLIDEAN GEOMETRY
• From Tarski to Hilbert
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
• Old and New Results in the Foundations of Elementary Plane Euclidean and Non-Euclidean Geometries
• A new analytic approach to hyperbolic geometry
• Mathematical Expeditions
• Tarski's System of Geometry
• Hilbert's ϵ‐operator in intuitionistic type theories
• From absolute to affine geometry in terms of point-reections, midpoints, and collinearity
• CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
• Mechanical Theorem Proving in Tarski’s Geometry
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS

This page was built for publication: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq