A Proof Procedure Using Connection Graphs

Abstract

Various deficiencies of resolution systems are investigated and a new theorem-proving system designed to remedy those deficiencms is presented The system is notable for eliminating redundancies present in SL-resolutlon, for incorporating preprocessing procedures, for liberahzing the order in which subgoals can be activated, for incorporating multidirectmnal searches, and for giving immediate access to pairs of clauses which resolve Examples of how the new system copes with the defic2encies of other theorem-proving systems are chosen from the areas of predicate logic programming and language parsing. The paper emphasizes the historical development of the new system, beginning as a supplement to SL-resolution in the form of classificatmn trees and incorporating an analogue of the Waltz algorithm for picture Interpretation The paper ends with a discussion of the opportunities for using look-ahead to guide the search for proofs