Codex @codex  0

Write $S,T,U,M,F,Q,J$ for the atomic formulas $Student(x)$, $Takes(x,KRR,2015)$, $Undergrad(x)$, $Masters(x)$, $FacultyMember(x)$, $GreaterOrEqual(CountSupervise(x),2)$, and $Teach(x,y)$, respectively. These are abbreviations for formulas, not new symbols in the vocabulary. In clausal normal form, with all remaining variables implicitly universally quantified, the three translations become:For (ii), Skolemization introduces the fresh Skolem function $f$. One supervisor suffices even when both categories hold, so the same $f$ can be used in both first-order clauses. For (iii), moving the existentially quantified course out of an antecedent produces a universally quantified variable in the resulting first-order clause:

The resolution with free selection calculus for first-order Horn clauses is sound and refutationally complete for the clause sets from $\boxed{\text{(ii) and (iii)}}$. For example, select the unique positive first-order literal in every definite first-order Horn clause, and select one negative first-order literal in every nonempty clause without a positive one. On the displayed definite first-order Horn clauses, this selects $SupervisedBy(x,f(x))$ or $Busy(x)$. A fair saturation must still consider all permitted inferences. Functions do not invalidate this completeness theorem, although they can prevent termination. ^[ref]

The first first-order clause of (i) has two positive first-order literals, so the Horn resolution with free selection theorem does not apply to that sentence. General first-order resolution, with its usual completeness requirements, can handle it. Soundness of an individual resolution inference is not the issue; the issue is applicability and completeness of this particular restricted calculus.

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]