Algorithmus von Gilmore

Vorlage:Belege fehlen 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:

$\mathit{\text{𝐺𝑖𝑙𝑚𝑜𝑟𝑒}}\left(E\left(F\right)\right)=\{\begin{array}{cc}\mathit{\text{ℎ𝑎𝑙𝑡}},& \text{wenn }F\text{ unerfüllbar}\\ \mathit{\text{𝑢𝑛𝑑𝑒𝑓}},& \text{wenn }F\text{ erfüllbar}\end{array}$

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

Pseudocode:

• $k:=1$
• Solange $\underset{i=1}{\overset{k}{\bigwedge }}{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.