A Nonclausal Connection-Graph Resolution Theorem-Proving Program

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 program's implementation and future status.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1982
Accession Number
ADA460606

Entities

People

  • Mark E. Stickel

Organizations

  • SRI International

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Application Software
  • Applied Computer Science
  • Artificial Intelligence
  • Artificial Intelligence Software
  • Availability
  • Classification
  • Computer Languages
  • Computer Programs
  • Computer Science
  • Contracts
  • Digital Information
  • Formal Languages
  • Information Operations
  • Language
  • Natural Language Understanding
  • Natural Languages

Readers

  • Computational Linguistics
  • Systems Analysis and Design

Technology Areas

  • AI & ML
  • AI & ML - Information Retrieval
  • AI & ML - Machine Learning Algorithms
  • Space