= Resolution with free selection
A family of resolution calculi for <first-order Horn clauses>. A selection function chooses either the positive head atom alone or a nonempty set of body atoms. Permitted inferences respect those choices; fair saturation is refutationally complete. Function symbols need not be excluded, so completeness does not by itself guarantee termination. <Rewriting Conjunctive Queries under Description Logic Constraints>[Section 2, “Resolution with Free Selection”]{ref}
Back to article page
