Accession Number : ADA326043
Title : Special Relations in Automated Deduction,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Manna, Zohar ; Waldinger, Richard
PDF Url : ADA326043
Report Date : MAY 1985
Pagination or Media Count : 64
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, 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.
Descriptors : *MATHEMATICAL LOGIC, REPRINTS, RESOLUTION, BINARY PROCESSORS, THEOREMS.
Subject Categories : Operations Research
Distribution Statement : APPROVED FOR PUBLIC RELEASE