Computer theorem proving for verifiable solving of geometric construction problems
DOI10.1007/978-3-319-21362-0_5zbMATH Open1434.03032OpenAlexW2294949920MaRDI QIDQ3452277FDOQ3452277
Pascal Schreck, Vesna Marinkovic, 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
Recommendations
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)
Cites Work
- Geometry constructions language
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
- The RegularChains library in Maple 10
- Geometric constraint solver
- Solvability by radicals is in polynomial time
- Higher order rule characterization of heuristics of compass and straight edge constructions in geometry
- From Tarski to Hilbert
- Towards Understanding Triangle Construction Problems
- DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
- Triangle Constructions with Three Located Points
- Title not available (Why is that?)
- Title not available (Why is that?)
- Axiomatizing geometric constructions
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
- Logic of Ruler and Compass Constructions
- Title not available (Why is that?)
- 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
- Formalization of Wu’s Simple Method in Coq
Cited In (11)
- Validity proof of Lazard's method for CAD construction
- Computer-aided construction of finite geometric spaces: Automated verification of geometric constraints
- On the mechanization of straightedge and compass constructions
- New dynamics in dynamic geometry: dragging constructed points
- Portfolio theorem proving and prover runtime prediction for geometry
- Automatic Verification of Regular Constructions in Dynamic Geometry Systems
- Automatic constructibility checking of a corpus of geometric construction problems
- Constructibility classes for triangle location problems
- Using jointly geometry and algebra to determine RC-constructibility
- Title not available (Why is that?)
- Towards an intelligent and dynamic geometry book
Uses Software
This page was built for publication: Computer theorem proving for verifiable solving of geometric construction problems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3452277)
