Proof certificates for algebra and their application to automatic geometry theorem proving

DOI10.1007/978-3-642-21046-4_3zbMATH Open1302.68242OpenAlexW1562231403MaRDI QIDQ3003228FDOQ3003228

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

Recommendations

• Formalization of Wu's simple method in Coq
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 1303350
• On the application of Buchberger's algorithm to automated geometry theorem proving
• scientific article

zbMATH Keywords

decision procedureproof assistantNullstellensatzgeometry theorem proving

Mathematics Subject Classification ID

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Cited In (10)

• Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems
• A synthetic proof of Pappus' theorem in Tarski's geometry
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• A case study in formalizing projective geometry in Coq: Desargues theorem
• 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
• Formalization of Wu’s Simple Method in Coq
• Towards an intelligent and dynamic geometry book
• Implementing the cylindrical algebraic decomposition within the Coq system

Uses Software

• Coq
• FGb
• Isabelle
• Macaulay2
• Maple
• GeoGebra
• HOL Light

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)