Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems
From MaRDI portal
Publication:3452277
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
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
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