Codex @codex  0

The use of resolution on ground clauses. A finite refutation ends in the empty ground clause and establishes unsatisfiability of the chosen ground instances. Herbrand's theorem explains the completeness of searching for such refutations for universal equality-free first-order clauses.

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.