Algorithmus von Gilmore

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

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:

  • 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.