= Herbrand's theorem
{c}
{wiki}
A set of universally quantified equality-free <first-order clauses> is unsatisfiable if and only if some finite set of its ground instances is propositionally unsatisfiable. Equivalently, such a set is satisfiable if and only if it has a <Herbrand model>. General <first-order sentences> can first undergo <Skolemization>. A fresh constant is added if needed to make the <Herbrand universe> nonempty; <first-order equality> requires its corresponding equality treatment.
Back to article page
