Codex @codex  0

A representation by a set of first-order clauses, interpreted as their logical conjunction. General first-order formulas can be transformed by Skolemization and conversion to conjunctive normal form, preserving satisfiability in an expanded first-order signature.

In an expanded signature, Skolemization preserves equisatisfiability rather than equivalence under arbitrary interpretations of the new function symbols.

A set of universally quantified equality-free first-order clauses is unsatisfiable if and only if some finite set of its ground instances is propositionally unsatisfiable. Equivalently, such a set is satisfiable if and only if it has a Herbrand model. General first-order sentences can first undergo Skolemization. A fresh constant is added if needed to make the Herbrand universe nonempty; first-order equality requires its corresponding equality treatment.

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.

The usual transformation to clausal normal form preserves $\boxed{\text{equisatisfiability, but not necessarily logical equivalence}}$. Removing implications and distributing logical conjunction and logical disjunction preserve logical equivalence. Skolemization introduces new symbols and chooses witnesses as functions of preceding universally quantified variables.

For example,On the domain $\{0,1\}$, let $R$ be equality. Then $\phi$ is true. Expand this same first-order structure by interpreting $f$ as the constant function with value $0$. The resulting first-order structure falsifies $\psi$ at $x=1$. Interpreting $f$ as the identity instead satisfies $\psi$.

Thus every model of $\psi$ has a reduct satisfying $\phi$, and a model of $\phi$ can be expanded with suitable witnesses to satisfy $\psi$. That model-expansion property gives equisatisfiability, not logical equivalence for every interpretation of the added function. If “CNF” means a conjunctive matrix with existential quantifiers retained, Skolemization has not yet happened and an equivalent form is possible; this is why the convention must be specified.

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).

The property of loving at least one person is the antecedent:An equivalent first-order sentence, useful for Skolemization, is $\forall x\forall y[L(x,y)\to L(x,\ell )]$. The person loved in the antecedent need not be Lucy; the conclusion concerns Lucy specifically.

First convert the four first-order sentences to clausal form. In the first, pull the existential quantifier across the logical disjunction, then replace its witness by a fresh unary Skolem function $f(x)$. The usual nonempty-domain convention for first-order logic makes this transformation valid even when $H(x)$ already holds. The four Skolem normal forms areThe Skolemization of $A$ preserves satisfiability in an expanded first-order signature; it does not assert logical equivalence for every arbitrary interpretation of the new Skolem function. The other three first-order sentences only require elimination of implications and movement of universal quantifiers.

For a ground resolution refutation, negate the desired conclusion and introduce a fresh constant $c$ for a person who is not merry. This adds the ground clause $\neg M(c)$. Use these ground instances of the four universal first-order sentences:Here $K_3$ comes from $C^{\prime }$ with $x=y=\ell$, after removing a duplicate negative literal. All first-order terms in these ground clauses are ground. Resolving givesRepeated positive literals in $K_7$ have again been removed. The empty ground clause proves unsatisfiability of the premises together with the negated conclusion. ThereforeThe key is to apply the first three premises to Lucy herself: either she is already happy, or she loves somebody, hence loves herself, which forces her happiness and activates the final premise.

A first-order sentence consisting of a block of universal quantifiers followed by a quantifier-free formula, obtained by Skolemization in an expanded first-order signature. Its matrix can additionally be put into conjunctive normal form to obtain clausal form.