Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
From MaRDI portal
Publication:5961492
DOI10.1007/BF00283133zbMath0865.68109OpenAlexW2022751246MaRDI QIDQ5961492
Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang
Publication date: 1996
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00283133
automated reasoningautomated geometry theorem provingCeva-Menelaus configurationsmultiple proofshortest proof
Related Items
Geometric constraint solving with geometric transformation, Self-evident automated geometric theorem proving based on complex number identity, Measuring the readability of geometric proofs: the area method case, Automated discovery of angle theorems, A program to create new geometry proof problems, Towards an intelligent and dynamic geometry book, The area method. A recapitulation, A review and prospect of readable machine proofs for geometry theorems, A graphical user interface for formal proofs in geometry, Automated deduction and knowledge management in geometry, Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles, Automatic Verification of Regular Constructions in Dynamic Geometry Systems, Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry, Taxonomies of geometric problems, GeoThms — a Web System for Euclidean Constructive Geometry
Cites Work
- Unnamed Item
- Depth-first iterative-deepening: An optimal admissible tree search
- Automated reasoning in geometry theorem proving with Prolog
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- Plane geometry theorem proving using forward chaining
- Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
- An examination of the geometry theorem machine
- Machine Proofs in Geometry
