= Solution
Write $S,T,U,M,F,Q,J$ for the <atomic formulas> $\mathit{Student}(x)$, $\mathit{Takes}(x,\mathit{KRR},2015)$, $\mathit{Undergrad}(x)$, $\mathit{Masters}(x)$, $\mathit{FacultyMember}(x)$, $\mathit{GreaterOrEqual}(\mathit{CountSupervise}(x),2)$, and $\mathit{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:
$$
\begin{array}{ll}
\text{(i)}&\neg S\lor\neg T\lor U\lor M,\\
&\neg S\lor\neg T\lor\neg U\lor\neg M;\\[2pt]
\text{(ii)}&\neg U\lor\mathit{SupervisedBy}(x,f(x)),\\
&\neg M\lor\mathit{SupervisedBy}(x,f(x));\\[2pt]
\text{(iii)}&\neg F\lor\neg Q\lor\neg J\lor\mathit{Busy}(x).
\end{array}
$$
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>:
$$
((F(x)\land Q(x)\land\exists y\,\mathit{Teach}(x,y))\to\mathit{Busy}(x))
\equiv\forall y\,((F(x)\land Q(x)\land\mathit{Teach}(x,y))\to\mathit{Busy}(x)).
$$
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 $\mathit{SupervisedBy}(x,f(x))$ or $\mathit{Busy}(x)$. A fair saturation must still consider all permitted inferences. Functions do not invalidate this completeness theorem, although they can prevent termination. <Rewriting Conjunctive Queries under Description Logic Constraints>[Section 2, “Resolution with Free Selection”: the selection condition and Horn resolution calculus]{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.
Back to article page
