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

DOI10.1007/978-3-642-21046-4_3MaRDI QIDQ3003228zbMATH OpenOpenAlexFDO

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

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)

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 DE number 67120

Cited in

(14)

• Formalization of Wu's simple method in Coq
• Theorem of three circles in Coq
• Proof assistant decision procedures for formalizing origami
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• Computer theorem proving for verifiable solving of geometric construction problems
• A synthetic proof of Pappus' theorem in Tarski's geometry
• A case study in formalizing projective geometry in Coq: Desargues theorem
• Implementing the cylindrical algebraic decomposition within the Coq system
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Formalizing complex plane geometry
• Towards an intelligent and dynamic geometry book
• Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker

Describes a project that uses

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)