Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
From MaRDI portal
(Redirected from Publication:5961492)
automated reasoningautomated geometry theorem provingCeva-Menelaus configurationsmultiple proofshortest proof
Recommendations
- Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
- A review and prospect of readable machine proofs for geometry theorems
- Automated generation of readable proofs for constructive geometry statements with the mass point method
- Automated production of traditional proofs in solid geometry
- Machine Proofs in Geometry
Cites work
- scientific article; zbMATH DE number 3586510 (Why is no real title available?)
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- An examination of the geometry theorem machine
- Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
- Automated reasoning in geometry theorem proving with Prolog
- Depth-first iterative-deepening: An optimal admissible tree search
- Machine Proofs in Geometry
- Plane geometry theorem proving using forward chaining
Cited in
(22)- A review and prospect of readable machine proofs for geometry theorems
- A graphical user interface for formal proofs in geometry
- Taxonomies of geometric problems
- Self-evident automated geometric theorem proving based on complex number identity
- Measuring the readability of geometric proofs: the area method case
- Automatic generation of staged geometric predicates
- The area method. A recapitulation
- Automatic Verification of Regular Constructions in Dynamic Geometry Systems
- Automated deduction and knowledge management in geometry
- Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
- Automated generation of illustrated proofs in geometry and beyond
- A program to create new geometry proof problems
- Automated discovery of angle theorems
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Automated generation of readable proofs for constructive geometry statements with the mass point method
- Automated production of traditional proofs in solid geometry
- Geometric constraint solving with geometric transformation
- Towards automated proving in solid geometry
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- GeoThms -- a web system for Euclidean constructive geometry
- Towards an intelligent and dynamic geometry book
- Some lemmas to hopefully enable search methods to find short and human readable proofs for incidence theorems of projective geometry
This page was built for publication: Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5961492)