Accession Number:

ADA326043

Title:

Special Relations in Automated Deduction,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Manna, Zohar
• Waldinger, Richard

Report Date:

1985-05-01

Pagination or Media Count:

64.0

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