Formalization of Hilbert's geometry of incidence and parallelism

DOI10.1023/A:1004959405270zbMath0933.03006MaRDI QIDQ1293015

Jan von Plato

Publication date: 21 March 2000

Published in: Synthese (Search for Journal in Brave)

zbMATH Keywords

axiomaticsformalization of geometryHilbert's geometry of incidence and parallelismJFM 30.0424.01JFM 34.0523.01JFM 47.0011.01JFM 56.0481.01type-theoretic formalization

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) Foundations of classical theories (including reverse mathematics) (03B30) History of mathematical logic and foundations (03-03) General theory of linear incidence geometry and projective geometries (51A05) History of geometry (51-03)

Related Items

Constructive geometrical reasoning and diagrams ⋮ The area method. A recapitulation ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs