= Clausal form
= Clausal normal form
{synonym}
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.
Back to article page
