Primary Paramodulation.
Abstract
Computers can directly use mathematical logic, that is first-order predicate calculus, in decision making and problem solving by the application of proof strategies involving resolution and paramodulation. A new category of problem solving strategies is defined which has the interesting and unusual property that refutations are formed by mixing certain primary paramodulants with resolvents obtained from any complete strategy in the predicate calculus without equality. Also, a new and easily applied technique is given for verifying that subsumed clauses can be eliminated from deductions. This technique is applied to all the strategies considered in this paper. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1971
- Accession Number
- AD0730714
Entities
People
- Alfred H. Morris Jr.
- Hartmul G. M. Huber
Organizations
- Naval Surface Warfare Center Dahlgren Division