Algorithmus von Gilmore

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:

$Gilmore\left(E\left(F\right)\right)=\begin{cases}halt, & \mbox{wenn }F\mbox{ unerfüllbar} \\ undef, & \mbox{wenn }F\mbox{ erfüllbar} \end{cases}$

Die abzählbare Menge $E\left(F\right)=\left\{A_1, A_2, ...\right\}$ sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.

Pseudocode:

• k: = 1
• Solange $\bigwedge_{i=1}^k A_i$ (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.