Nonclausal Connection-Graph Resolution Theorem-Proving Program.

摘要

This paper describes the theory behind, and features of, a new theorem-proving program that combines the use of nonclausal resolution and connection graphs. The program is being developed as a reasoning component of a natural-language-understanding system. The most important characteristics of the program are as follows: (1) nonclausal resolution is used as the inference system, which eliminates some of the redundancy and unreadability of clause- based systems; (2) a connection graph is used to represent permitted resolution operations, which restricts the search space and facilitates the use of graph searching for efficient deduction; and (3) heuristic search and special logical connectives are used for program control. This paper describes these aspects of the program, citing their advantages and disadvantages, and reviews the program's implementation and future status.