Publication in BibTeX Format

@TECHREPORT{AICPub602:1985,
  AUTHOR={Manna, Zohar and Waldinger, Richard},
  TITLE={Special Relations In Automated Deduction},
  ADDRESS={333 Ravenswood Ave., Menlo Park, CA 94025},
  INSTITUTION={AI Center, SRI International},
  MONTH={Jun},
  NUMBER={355},
  YEAR={1985},
  KEYWORDS={Deduction!Special relations},
  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.}
}