Special relations in automated deductionSpecial relations in automated deduction

Access Restriction
Subscribed

 Author Manna, Zohar ♦ Waldinger, Richard Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©1986 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science 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 $\textit{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. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1986-01-02 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 33 Issue Number 1 Page Count 59 Starting Page 1 Ending Page 59

Open content in new tab

Source: ACM Digital Library