Experiments with a heuristic theorem-proving program for predicate calculus with equality

摘要

A new theorem-proving program to solve problems expressed in the first-order predicate calculus with equality has been implemented and extensively tested. The basic algorithm employs resolution and paramodulation as its rules of inference, and uses set-of-support and input strategies. It has been augmented by numerous heuristics, some newly devised, enabling the successful solution of a large number of problems with widely differing characteristics. Among the heuristics, a sequencing table and other means of taking into account user-supplied information about hypotheses when deciding on the next step to perform have proved to be most powerful. Without them, satisfactory performance would not have been attained. Different heuristics were found to be more effective for different classes of problems. The paper discusses the significance of this research, gives a complete description of the program, and presents a detailed account of the experiments which have been conducted.