The axioms of constructive geometry

DOI10.1016/0168-0072(95)00005-2zbMath0836.03034OpenAlexW2067558609WikidataQ114684038 ScholiaQ114684038MaRDI QIDQ1902978

Jan von Plato

Publication date: 2 May 1996

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(95)00005-2

zbMATH Keywords

affine geometryorthogonal geometryconstructive type theoryprojective geometryconstructive geometryAnother Logical Frameworkapartness geometry

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) General theory of linear incidence geometry and projective geometries (51A05) Other constructive mathematics (03F65) Linear incidence geometric structures with parallelism (51A15) Congruence and orthogonality in metric geometry (51F20) Intuitionistic mathematics (03F55)

Related Items

A constructive real projective plane ⋮ Formalizing generalized maps in Coq ⋮ Current Status of the I2GATP Common Format ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Two cryptomorphic formalizations of projective incidence geometry ⋮ Constructive geometrical reasoning and diagrams ⋮ The ILTP problem library for intuitionistic logic ⋮ CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ Syntactic categories in the language of mathematics ⋮ Brouwer and Euclid ⋮ Using the prover ANDP to simplify orthogonality. ⋮ The area method. A recapitulation ⋮ Simplifying von Plato's axiomatization of constructive apartness geometry ⋮ Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof ⋮ A resolution theorem prover for intuitionistic logic ⋮ Organization and development of a constructive axiomatization ⋮ Constructivity in Geometry ⋮ Axiomatizing geometric constructions ⋮ In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs ⋮ Real numbers and projective spaces: intuitionistic reasoning with undecidable basic relations ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Mechanical Theorem Proving in Tarski’s Geometry ⋮ Constructibility and Geometry ⋮ Building Mathematics-Based Software Systems to Advance Science and Create Knowledge ⋮ A ModalWalk Through Space ⋮ A constructive theory of ordered affine geometry ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ Automating Theories in Intuitionistic Logic ⋮ A common axiom set for classical and intuitionistic plane geometry ⋮ A FORMAL SYSTEM FOR EUCLID’SELEMENTS ⋮ Formalizing constructive projective geometry in Agda ⋮ Formalizing complex plane geometry

Uses Software

• ALF

Cites Work

• Constructive mathematics and computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item