Skolem normal form
= Skolem normal form
{c}
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>.