Der Algorithmus von Gilmore (auch Gilmore-Algorithmus) liefert ein Semi-Entscheidungsverfahren um prädikatenlogische Formeln auf Unerfüllbarkeit zu testen. Es basiert auf dem Satz von Herbrand und wurde von Paul C. Gilmore 1960 veröffentlicht.
Es gilt:
Die abzählbare Menge sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.
Pseudocode:
Solange (aussagenlogisch) erfüllbar ist, setze 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. Die Resolventenmethode von Robinson überkommt einige Nachteile des Algorithmus von Gilmore.
Einzelnachweise
Gilmore, Algorithmus von Kategorie:Mathematische Logik