Plane geometry theorem proving using forward chaining

DOI10.1016/0004-3702(75)90013-2zbMath0301.68086OpenAlexW2091926481MaRDI QIDQ1215410

Arthur J. Nevins

Publication date: 1975

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1721.1/6218

Mathematics Subject Classification ID

Related Items (17)

Automated reasoning in geometry theorem proving with Prolog ⋮ Automated discovery of geometric theorems based on vector equations ⋮ Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems ⋮ 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 ⋮ The area method. A recapitulation ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ A relaxation approach to splitting in an automatic theorem prover ⋮ Non-resolution theorem proving ⋮ Automatic theorem proving in set theory ⋮ Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation ⋮ Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles ⋮ Towards a geometry deductive database prover ⋮ Automated generation of geometry proof problems based on point geometry identity ⋮ Geometry machines: from AI to SMC ⋮ Conservation principles and action schemes in the synthesis of geometric concepts ⋮ Geometric theorem proving by integrated logical and algebraic reasoning

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A relaxation approach to splitting in an automatic theorem prover
• A man-machine theorem-proving system
• A Human Oriented Logic for Automatic Theorem-Proving
• Experiments With a Multipurpose, Theorem-Proving Heuristic Program

This page was built for publication: Plane geometry theorem proving using forward chaining