 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. ^[ref]