Formalization of Wu’s Simple Method in Coq

DOI10.1007/978-3-642-25379-9_8zbMath1350.68234OpenAlexW120661248MaRDI QIDQ3100204

Julien Narboux, Pascal Schreck, Jean-David Génevaux

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_8

zbMATH Keywords

geometryautomationproof assistantCoqformalizationWu's method

Mathematics Subject Classification ID

Related Items (5)

Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems ⋮ Two cryptomorphic formalizations of projective incidence geometry ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Towards an intelligent and dynamic geometry book ⋮ Formalizing complex plane geometry

Uses Software

• Coq
• MMP/Geometer
• GEOTHER 1.1
• GeoProof
• GCLCprover
• GeoThms
• OCaml
• GEX
• JGEX

Cites Work

• Unnamed Item
• Unnamed Item
• The area method. A recapitulation
• A new theorem discovered by computer prover
• A graphical user interface for formal proofs in geometry
• Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
• An Introduction to Java Geometry Expert
• A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
• Without Loss of Generality
• Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
• Machine Proofs in Geometry
• Context Aware Calculation and Deduction
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Automated Deduction in Geometry
• Automated Deduction in Geometry

This page was built for publication: Formalization of Wu’s Simple Method in Coq