Interpolation Theorems for Resolution in Lower Predicate Calculus

Abstract

The resolution principle is an inference rule for quantifier-free first-order predicate calculus. In the past, the completeness theorems for resolution and its refinements have been stated and proved for finite sets of clauses. It is easy (by Gödel's Compactness Theorem) and of practical interest to extend them to countable sets, thus allowing schemata representing denumerably many axioms. In addition, some theorems similar to Craig's Interpolation Theorem are proved for deduction by resolution. In propositional calculus, the theorem proved is stronger, whereas in predicate calculus the theorems proved are in some ways stronger and in some ways weaker than Craig's theorem. These interpolation theorems suggest procedures which could be embodied in computer programs for automatic proof finding and consequence finding.