Algorithmus von Gilmore

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:

$\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 $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. Die Resolventenmethode von Robinson überkommt einige Nachteile des Algorithmus von Gilmore.