A deductive database approach to automated geometry theorem proving and discovering

From MaRDI portal
Publication:1581854

DOI10.1023/A:1006171315513zbMath0961.68121OpenAlexW2120243289MaRDI QIDQ1581854

Shang-Ching Chou, Jing-Zhong Zhang, Xiao-Shan Gao

Publication date: 10 June 2001

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1006171315513



Related Items

GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry, Learning to solve geometric construction problems from images, The Relation Tool in GeoGebra 5, Automated discovery of geometric theorems based on vector equations, Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method, Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method, Towards an Automated Geometer, Self-evident automated geometric theorem proving based on complex number identity, Eliminating redundant search space on backtracking for forward chaining theorem proving, The area method. A recapitulation, A review and prospect of readable machine proofs for geometry theorems, Automated detection of interesting properties in regular polygons, A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs, Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry, A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs, Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method, A mechanical geometer, Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices, DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY, Taxonomies of geometric problems, Automated generation of geometric theorems from images of diagrams