BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-85-1051
       ENTRY:: May 01, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Special relations in automated deduction
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Waldinger, Richard
        DATE:: May 1985
       PAGES:: 66
    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, generalize to an arbitrary
               binary relation the paramodulation and E-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.
       NOTES:: [Adminitrivia V1/Prg/19950501]
         END:: STAN//CS-TR-85-1051