DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Special Relations in Automated Deduction,
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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, generalise to an arbitrary binary relation the paramodulation and 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.
APPROVED FOR PUBLIC RELEASE