Accession Number:

ADA460606

Title:

A Nonclausal Connection-Graph Resolution Theorem-Proving Program

Descriptive Note:

Technical note

Corporate Author:

SRI INTERNATIONAL MENLO PARK CA ARTIFICIAL INTELLIGENCE CENTER

Personal Author(s):

Report Date:

1982-10-01

Pagination or Media Count:

15.0

Abstract:

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 programs implementation and future status.

Subject Categories:

  • Linguistics
  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE