Past exam of the computer science course of the University of Oxford / 2015 / Knowledge representation and reasoning / 1 / d / i

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