A constructive theory of ordered affine geometry

DOI10.1016/S0019-3577(98)80034-7zbMath0926.51014OpenAlexW2165887062MaRDI QIDQ1279729

Jan von Plato

Publication date: 21 November 1999

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0019-3577(98)80034-7

zbMATH Keywords

affine geometryprojective geometryconstructive geometryAnother Logical Frameworkapartness geometry

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Ordered geometries (ordered incidence structures, etc.) (51G05) Other constructive mathematics (03F65) Intuitionistic mathematics (03F55)

Related Items

A constructive real projective plane, Implementing Euclid's straightedge and compass constructions in type theory, CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE, Simplifying the axiomatization for ordered affine geometry via a theorem prover, Axiomatizing geometric constructions, The axiomatics of ordered geometry: I. Ordered incidence spaces, A FORMAL SYSTEM FOR EUCLID’SELEMENTS

Uses Software

• ALF

Cites Work

• Unnamed Item
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry
• Organization and development of a constructive axiomatization