A synthetic proof of Pappus' theorem in Tarski's geometry
From MaRDI portal
Publication:2362204
DOI10.1007/s10817-016-9374-4zbMath1405.03034OpenAlexW2207132767MaRDI QIDQ2362204
Publication date: 6 July 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01176508/file/Pappus.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
Pappus's hexagon theorem in real projective plane ⋮ Finding proofs in Tarskian geometry ⋮ From informal to formal proofs in Euclidean geometry ⋮ Proof-checking Euclid ⋮ Euclid after Computer Proof-Checking ⋮ Towards an intelligent and dynamic geometry book ⋮ The Axiomatic Destiny of the Theorems of Pappus and Desargues ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Tarski geometry axioms. III
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The area method. A recapitulation
- A case study in formalizing projective geometry in Coq: Desargues theorem
- A constructive version of Tarski's geometry
- Formalization of the arithmetization of Euclidean plane geometry and applications
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Proof and Computation in Geometry
- From Tarski to Hilbert
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
- First-Class Type Classes
- ON PROJECTIONS IN PROJECTIVE SPACES
- Mechanical Theorem Proving in Tarski’s Geometry
This page was built for publication: A synthetic proof of Pappus' theorem in Tarski's geometry
