Accession Number:

AD0745746

Title:

Contracted Resolution.

Descriptive Note:

Technical rept.,

Corporate Author:

NAVAL WEAPONS LAB DAHLGREN VA

Personal Author(s):

• Huber,Hartmut G. N.
• Morris,Alfred H. , Jr

Report Date:

1972-01-01

Pagination or Media Count:

24.0

Abstract:

In order to improve the capability of resolution programs for automatic decision making, a new rule of inference called contracted resolution is proposed. Under this rule of inference more literals are often eliminated than in a pairwise Robinson resolvent. Contracted resolution is shown to be sound and complete, requiring only reflutations that are input deductions in the Chang and Slagle sense. Subsumption is defined in ths environment, and it is shown that subsumed clauses can be deleted. Author

Descriptors:

• (*MATHEMATICAL LOGIC
• COMPUTER PROGRAMMING)
• SET THEORY
• SEQUENCES(MATHEMATICS)
• THEOREMS
• PROBLEM SOLVING

Subject Categories:

• Statistics and Probability
• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE