= Solution
For resolution, a <first-order sentence> is in <clausal normal form> when it is a universally quantified <logical conjunction> of <first-order clauses>:
$$
\boxed{\forall\bar x\,\bigwedge_{i=1}^{m}\bigvee_{j=1}^{k_i}L_{ij},}
$$
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).
Back to article page
