Special Relations in Automated Deduction,

Abstract

Two deduction rules are introduced to give streamlined treatment to relations of special importance in an automated theorem proving system. These rules, the relation replacement and relation matching rules, generalise to an arbitrary binary relation the paramodulation and resolution rules, respectively, for equality, and may operate within a nonclausal or clausal system. The new rules depend on an extension of the notion of polarity to apply to subterms as well as to subsentences, with respect to a given binary relation. The rules allow us to eliminate troublesome axioms, such as transitivity and monotonicity, from the system; proofs are shorter and more comprehensible, and the search space is correspondingly deflated.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1985
Accession Number
ADA326043

Entities

People

  • Richard Waldinger
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Artificial Intelligence
  • Computer Programming
  • Computer Science
  • Computers
  • Language
  • New York
  • Notation
  • Numbers
  • Permutations
  • Polarity
  • Programming Languages
  • Real Numbers
  • Theorems
  • United States
  • Universities

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • Space