Special Relations In Automated Deduction
by Manna, Zohar and Waldinger, Richard
Technical Note 355
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave., Menlo Park, CA 94025
Jun 1985.
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.
 Adobe PDF |
 BibTeX |
 EndNote |
| Name | Title | ||
|---|---|---|---|
 |
Waldinger, Richard J | Principal Scientist |  |
