A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

DOI10.1007/978-3-642-25070-5_12zbMath1252.68264OpenAlexW144472580MaRDI QIDQ3102745

Vesna Pavlović, Sana Stojanović, Predrag Janičić

Publication date: 25 November 2011

Published in: Automated Deduction in Geometry (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25070-5_12

zbMATH Keywords

coherent logicgeometric theorem proving

Mathematics Subject Classification ID

Related Items (14)

Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems ⋮ From informal to formal proofs in Euclidean geometry ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Invited Talk: Coherentisation of First-Order Logic ⋮ Towards Understanding Triangle Construction Problems ⋮ Measuring the readability of geometric proofs: the area method case ⋮ Towards an intelligent and dynamic geometry book ⋮ Automated deduction and knowledge management in geometry ⋮ GEOMETRISATION OF FIRST-ORDER LOGIC ⋮ ArgoCLP ⋮ A Vernacular for Coherent Logic ⋮ Taxonomies of geometric problems ⋮ Theorem proving as constraint solving with coherent logic ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Coq
• Theorema
• TPTP
• Isar
• HOL Light
• EUCLID

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A case study in formalizing projective geometry in Coq: Desargues theorem
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Using Gröbner bases to reason about geometry problems
• Formalization of Hilbert's geometry of incidence and parallelism
• A deductive database approach to automated geometry theorem proving and discovering
• Automated development of Tarski's geometry
• The axioms of constructive geometry
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Formalizing Projective Plane Geometry in Coq
• Skolem Machines and Geometric Logic
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Efficiency of a Good But Not Linear Set Union Algorithm
• Machine Proofs in Geometry
• Automating Coherent Logic
• Mechanical Theorem Proving in Tarski’s Geometry
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles

This page was built for publication: A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs