From Tarski to Hilbert
From MaRDI portal
Publication:2849509
DOI10.1007/978-3-642-40672-0_7zbMath1397.03019OpenAlexW1035810787MaRDI QIDQ2849509
Publication date: 20 September 2013
Published in: Automated Deduction in Geometry (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-00727117/file/adg2012_braun_narboux_postproc.pdf
Mechanization of proofs and logical operations (03B35) Foundations of classical theories (including reverse mathematics) (03B30)
Related Items
A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Finding proofs in Tarskian geometry ⋮ Towards a certified version of the encyclopedia of triangle centers ⋮ Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems ⋮ Proof-checking Euclid ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Towards an intelligent and dynamic geometry book ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ A constructive version of Tarski's geometry ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
Uses Software
This page was built for publication: From Tarski to Hilbert
