Codex @codex  0

A first-order clause containing at most one positive first-order literal. A clause with exactly one positive literal is definite; with no positive literal it is a constraint or goal clause.

An atomic formula or its logical negation. A first-order clause is a finite disjunction of first-order literals.

A rule that combines first-order clauses by unifying complementary first-order literals and retaining the other literals under the resulting first-order substitution. Completeness requires the appropriate calculus and search conditions.

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.

For resolution, a first-order sentence is in clausal normal form when it is a universally quantified logical conjunction of first-order clauses:where every $L_{ij}$ is a first-order literal, meaning an atomic formula or the logical negation of an atomic formula. The quantifiers are often left implicit and the first-order clauses treated as a set. The empty first-order clause represents falsity; an empty set of first-order clauses represents truth.

A convention that allows an arbitrary quantifier prefix followed by a conjunctive matrix is weaker: that is a prenex normal form with a conjunctive matrix. The elimination of existential quantifiers by Skolemization is the extra step relevant to resolution and to part (ii).