Pattern-Directed Invocation with Changing Equalities.

Abstract

The interaction of pattern-directed invocation with equality in an automated reasoning system give rise to a completeness problem. In such systems, a demon needs to be invoked not only when its pattern exactly matches a term in the reasoning data base, but also when it is possible to create a variant that matches. An incremental algorithm has been developed, which solves this problem without generating all possible variants of terms in the data base. The algorithm is shown to be complete for a class of demons, called transparent demons, in which there is a well-behaved logical relationship between the pattern and the body of the demon. Completeness is maintained when new demons, new terms, and new equalities are added in any order. Equalities can also be retracted via a truth maintenance system. The algorithm has been implemented as part of a reasoning system called BREAD. (KR)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1988
Accession Number
ADA198146

Entities

People

  • Charles Rich
  • Yishai A. Feldman

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Artificial Intelligence Computing
  • Corporations
  • Databases
  • Department Of Defense
  • Environment
  • Guarantees
  • Information Systems
  • Language
  • Law
  • Maintenance
  • Military Research
  • Notation
  • Programming Languages
  • Reasoning
  • Standards

Readers

  • Calculus or Mathematical Analysis
  • Computational Linguistics