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)

• Proof assistant decision procedures for formalizing origami
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• A synthetic proof of Pappus' theorem in Tarski's geometry
• 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
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• 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

Describes a project that uses

Uses Software

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

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)