Contracted Resolution.
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1972
- Accession Number
- AD0745746
Entities
People
- Alfred H. Morris Jr.
- Hartmut G. N. Huber
Organizations
- Naval Surface Warfare Center Dahlgren Division