A constructive version of Tarski's geometry
From MaRDI portal
Publication:490871
DOI10.1016/j.apal.2015.07.006zbMath1392.03059arXiv1407.4399OpenAlexW1479730010MaRDI QIDQ490871
Publication date: 21 August 2015
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1407.4399
Geometric constructions in real or complex geometry (51M15) Foundations of classical theories (including reverse mathematics) (03B30) Other constructive mathematics (03F65) Euclidean geometries (general) and generalizations (51M05)
Related Items (9)
A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Proof-checking Euclid ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE ⋮ Brouwer and Euclid ⋮ Negation-free and contradiction-free proof of the Steiner-Lehmus theorem ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Formalization of the Poincaré disc model of hyperbolic geometry
Cites Work
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Foundations of geometry (Festschrift 1899). Edited and commented by Klaus Volkert
- Über die Kreisaxiome
- Proof and Computation in Geometry
- From Tarski to Hilbert
- Forms of the Pasch axiom in ordered geometry
- Tarski's System of Geometry
- CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
- A further simplification of Tarski's axioms of geometry
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- 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
This page was built for publication: A constructive version of Tarski's geometry
