Resolution Graphs

Abstract

This paper introduces a new notation, called "resolution graphs, 11 for deductions by resolution in first-order predicate calculus. A resolution graph consists of groups of nodes that represent initial clauses of a deduction and links that represent unifying substitutions. Each such graph uniquely represents a resultant clause that can be deduced by certain alternative but equivalent sequences of resolution and factoring operations. Resolution graphs are used to illustrate the significance of merges and tautologies in proofs by resolution. Finally, they provide a basis for proving the completeness of a proof strategy that combines the set of support, resolution with merging, linear format, and Loveland's subsumption conditions.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1970
Accession Number
ADA638143

Entities

People

  • Bertram Raphael
  • Robert A. Yates
  • Timothy P. Hart

Organizations

  • SRI International

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Artificial Intelligence
  • Automatic
  • Calculus
  • Collapse
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Information Operations
  • Mathematics
  • Notation
  • Sequences
  • Systems Science
  • Universities

Readers

  • Artificial Intelligence
  • Graph Algorithms and Convex Optimization.