Algorithmus von Gilmore
Vorlage:Hinweisbaustein 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.<ref>{{#invoke:Vorlage:Literatur|f}}</ref><ref>{{#invoke:Vorlage:Literatur|f}}</ref>
Es gilt:
- <math>\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}</math>
Die abzählbare Menge <math>E\left(F\right)=\left\{A_1, A_2, ...\right\}</math> sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.
- <math>k {:=} 1</math>
- Solange <math>\bigwedge_{i=1}^k A_i</math> (aussagenlogisch) erfüllbar ist, setze <math>k{:=}k+1</math>
- 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.<ref>{{#invoke:Vorlage:Literatur|f}}</ref>
Einzelnachweise
<references />