Algorithmus von Gilmore
aus Wikipedia, der freien Enzyklopädie
Der Algorithmus von Gilmore (auch Gilmore-Algorithmus) basiert auf dem Satz von Herbrand und liefert ein Semi-Entscheidungsverfahren um prädikatenlogische Formeln auf Unerfüllbarkeit zu testen. Es gilt:
Die abzählbare Menge 
sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.
Pseudocode:
- k: = 1
- Solange
(aussagenlogisch) erfüllbar ist, setze k: = k + 1 - Halt. (Ausgabe: unerfüllbar)
Man sieht, dass der Algorithmus semi-entscheidbar ist, da er nur in endlicher Zeit hält, wenn er Unerfüllbarkeit feststellt.
