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 substitution t for an existentially bound variable y in some formula F, such that F{t/y} is provable. The term t is built of the function and predicate symbols in F, plus Boolean functions and a case splitting function if, defined in the standard way: if (True, x, y) = x and if (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 criteria R of a certain type, prohibiting the derivation of the substitution terms t for which R(t) fails. This enables us to specify, for example, that the substitution t must be in some special signature or must be type-correct, without losing completeness. We will also consider ordering restrictions for the A-calculus.