Report Number: CS-TR-85-1051
Institution: Stanford University, Department of Computer Science
Title: Special relations in automated deduction
Author: Manna, Z ohar
Author: Waldinger, Richard
Date: May 1985
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/85/1051/CS-TR-85-1051.pdf