Jacques Herbrand entwickelte die Herbrand-Theorie, welche ein Semi-Entscheidungsverfahren für die Unerfüllbarkeit von prädikatenlogischen Formeln liefert. Gesucht ist eine (einfache) Teilklasse von Strukturen/ Modellen, so dass eine Formel genau dann unerfüllbar (bzw. erfüllbar) wird, wenn sie kein (bzw. ein) Modell in dieser Teilklasse hat.

Herbrand-Universum, Herbrand-Struktur, Herbrand-Interpretation, Herbrand-Modell