Plane Geometry Theorem Proving Using Forward Chaining,
Abstract
A computer program is described which operates on a subset of plane geometry. Its performance not only compares favorably with previous computer programs, but within its limited problem domain (e.g. no curved lines nor introduction of new points), it also invites comparison with the best human theorem provers. The program employs a combination of forward and backward chaining with the forward component playing the more important role. This, together with a deeper use of diagrammatic information, allows the program to dispense with the diagram filter in contrast with its central role in previous programs. An inportant aspect of human problem solving may be the ability to structure a problem space so that forward chaining techniques can be used effectively.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1974
- Accession Number
- ADA004223
Entities
People
- Arthur J. Nevins
Organizations
- Massachusetts Institute of Technology