Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems

DOI10.1007/978-3-319-21362-0_5zbMath1434.03032OpenAlexW2294949920MaRDI QIDQ3452277

Pascal Schreck, Vesna Marinković, Predrag Janičić

Publication date: 11 November 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-319-21362-0_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Geometric constructions in real or complex geometry (51M15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Constructibility classes for triangle location problems ⋮ Automatic constructibility checking of a corpus of geometric construction problems ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Using jointly geometry and algebra to determine RC-constructibility ⋮ Towards an intelligent and dynamic geometry book ⋮ On the mechanization of straightedge and compass constructions ⋮ New dynamics in dynamic geometry: dragging constructed points

Uses Software

• GCLC
• RegularChains
• OpenGeoProver
• ArgoCLP
• gcl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solvability by radicals is in polynomial time
• Variation of geometries based on a geometric-reasoning method
• Geometric construction by assembling solved subfigures
• Sketch-based pruning of a solution space within a formal geometric constraint solver
• Higher order rule characterization of heuristics of compass and straight edge constructions in geometry
• Geometric constraint solver
• Axiomatizing geometric constructions
• Geometry constructions language
• From Tarski to Hilbert
• Logic of Ruler and Compass Constructions
• Towards Understanding Triangle Construction Problems
• Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
• Formalization of Wu’s Simple Method in Coq
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
• DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
• Triangle Constructions with Three Located Points