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.
New to topics? Read the docs here!