Der Algorithmus von Gilmore basiert auf dem Satz von Herbrand und liefert ein Semi-Entscheidungsverfahren um prädikatenlogische Formeln auf Unerfüllbarkeit zu testen. Es gilt:

mit E(F) sei die Herbrand-Expansion von F.

Verfahren

Die Menge E(F) mit

sei die Herbrand-Expansion zu F.

i = 1;
prüfe A₁ = :temp auf Unerfüllbarkeit (aussagenlogisch);

WHILE {

prüfe auf Unerfüllbarkeit (aussagenlogisch)

wenn Unerfüllbar, dann halt, i++ sonst;

}