Thumbnail
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

   Open content in new tab
Source: ACM Digital Library