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

DOI10.1007/BF00283134zbMATH Open0865.68110OpenAlexW2762770850MaRDI QIDQ5961493FDOQ5961493

Jingzhong 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

Recommendations

• Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
• Automated production of traditional proofs in solid geometry
• Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
• Machine Proofs in Geometry
• scientific article; zbMATH DE number 1263331

zbMATH Keywords

backward chainingforward chainingautomated geometry theorem provingfull-angle method

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

Cited In (23)

• A review and prospect of readable machine proofs for geometry theorems
• A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs
• Proving geometry theorems with rewrite rules
• Self-evident automated geometric theorem proving based on complex number identity
• Taxonomies of geometric problems
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
• Measuring the readability of geometric proofs: the area method case
• Automated theorem proving in GeoGebra: current achievements
• Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
• The area method. A recapitulation
• 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
• Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
• Automated deduction and knowledge management in geometry
• Automated generation of illustrated proofs in geometry and beyond
• Generalizing Morley's and other theorems with automated realization
• GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry
• A method for the automated discovery of angle theorems
• Automated generation of illustrations for synthetic geometry proofs
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Towards an intelligent and dynamic geometry book
• Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method
• Open geometry prover community project
• Title not available (Why is that?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5961493)