REFINEMENT THEOREMS IN RESOLUTION THEORY,
Abstract
The paper discusses some basic refinements of the Resolution Principle which are intended to improve the speed and efficiency of theorem-proving programs based on this rule of inference. It is proved that two of the refinements preserve the logical completeness of the proof procedure when used separately, but not when used in conjunction. The results of some preliminary experiments with the refinements are given. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 24, 1969
- Accession Number
- AD0685613
Entities
People
- David Luckham
Organizations
- Stanford University