Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation

DOI10.1007/BF00283133zbMATH Open0865.68109OpenAlexW2022751246MaRDI QIDQ5961492FDOQ5961492

Shang-Ching Chou, Xiao-Shan Gao, Jingzhong 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

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

zbMATH Keywords

automated reasoningautomated geometry theorem provingCeva-Menelaus configurationsmultiple proofshortest proof

Mathematics Subject Classification ID

Cites Work

• Automated reasoning in geometry theorem proving with Prolog
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Machine Proofs in Geometry
• Depth-first iterative-deepening: An optimal admissible tree search
• Title not available (Why is that?)
• 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

Cited In (18)

• A review and prospect of readable machine proofs for geometry theorems
• A graphical user interface for formal proofs in geometry
• Self-evident automated geometric theorem proving based on complex number identity
• Taxonomies of geometric problems
• Measuring the readability of geometric proofs: the area method case
• Automatic generation of staged geometric predicates
• Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry
• The area method. A recapitulation
• Automatic Verification of Regular Constructions in Dynamic Geometry Systems
• Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
• Automated deduction and knowledge management in geometry
• A program to create new geometry proof problems
• Automated discovery of angle theorems
• Automated production of traditional proofs in solid geometry
• Geometric constraint solving with geometric transformation
• 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

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)