%0 Report %@ 355 %A Manna, Zohar and Waldinger, Richard %T Special Relations In Automated Deduction %C 333 Ravenswood Ave., Menlo Park, CA 94025 %I AI Center, SRI International %D 1985 %K Deduction!Special relations %X 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. %U http://www.ai.sri.com/pubs/files/602.pdf
