Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles

DOI10.1007/BF00283134zbMath0865.68110OpenAlexW2762770850MaRDI QIDQ5961493

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

Publication date: 20 February 1997

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

Full work available at URL: https://doi.org/10.1007/bf00283134

zbMATH Keywords

automated geometry theorem provingbackward chainingforward chainingfull-angle method

Mathematics Subject Classification ID

Related Items (20)

GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry ⋮ Automated theorem proving in GeoGebra: current achievements ⋮ Generalizing Morley's and other theorems with automated realization ⋮ 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 ⋮ Self-evident automated geometric theorem proving based on complex number identity ⋮ Measuring the readability of geometric proofs: the area method case ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ Towards an intelligent and dynamic geometry book ⋮ The area method. A recapitulation ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry. ⋮ Automated deduction and knowledge management in geometry ⋮ A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs ⋮ Automated generation of illustrations for synthetic geometry proofs ⋮ Open geometry prover community project ⋮ A method for the automated discovery of angle theorems ⋮ 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 ⋮ Taxonomies of geometric problems

Cites Work

• 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
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• An examination of the geometry theorem machine
• Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation

This page was built for publication: Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles