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:

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

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

Pseudocode:

• ${\displaystyle k{:=}1}$
• Solange ${\displaystyle \bigwedge _{i=1}^{k}A_{i}}$ (aussagenlogisch) erfüllbar ist, setze ${\displaystyle 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.