Proof certificates for algebra and their application to automatic geometry theorem proving
From MaRDI portal
Publication:3003228
DOI10.1007/978-3-642-21046-4_3zbMATH Open1302.68242OpenAlexW1562231403MaRDI QIDQ3003228FDOQ3003228
Authors: Benjamin Grégoire, Loïc Pottier, Laurent Théry 
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
Recommendations
Cited In (14)
- A synthetic proof of Pappus' theorem in Tarski's geometry
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Theorem of three circles in Coq
- Formalization of Wu's simple method in Coq
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Formalizing complex plane geometry
- Computer theorem proving for verifiable solving of geometric construction problems
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- Towards an intelligent and dynamic geometry book
- Implementing the cylindrical algebraic decomposition within the Coq system
- Proof assistant decision procedures for formalizing origami
Uses Software
This page was built for publication: Proof certificates for algebra and their application to automatic geometry theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003228)
