Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
From MaRDI portal
Publication:3003228
DOI10.1007/978-3-642-21046-4_3zbMath1302.68242OpenAlexW1562231403MaRDI QIDQ3003228
Loïc Pottier, Laurent Théry, Benjamin Grégoire
Publication date: 26 May 2011
Published in: Automated Deduction in Geometry (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00504719/file/pottier.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Towards an intelligent and dynamic geometry book ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Formalization of Wu’s Simple Method in Coq ⋮ Formalizing complex plane geometry
Uses Software
This page was built for publication: Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
