Completeness of Resolution for Definite Answers

摘要

We investigate the problem of finding a computable witness for the existential quantifier in a formula of the classical first-order predicate logic. The A-resolution calculus which is essentially the same as the program derivation algorithm A of C.-L. Chang, R.C-T. Lee and R.Waldinger is used for finding a definite substitutiontfor an existentially bound variableyin some formulaF, such thatF{t/y}is provable. The termtis built of the function and predicate symbols inF, plus Boolean functions and a case splitting functionif, defined in the standard way:if (True, x,y)=xandif(False, x,y)=y. We prove that the A-resolution calculus is complete in the following sense: if such a definite substitution exists, then the A-calculus derives a clause giving such a substitution. The result is strengthened by allowing the usage of liftable criteriaRof a certain type, prohibitin the derivation of the substitution termstfor whichR(t)fails. The enables us to specify, for example, that the substitutiontmust be in some special signature or must be type-correct, without losing completeness. We will also consider ordering restrictions for the A-calculus.