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>P. C. Gilmore: A Proof Method for Quantification Theory: Its Justification and Realization. In: IBM Journal of Research and Development. Band 4, Nr. 1, Januar 1960, ISSN 0018-8646, S. 28–35, doi:10.1147/rd.41.0028 (IEEE-Eintrag oder Artikelkopie [abgerufen am 19. März 2026]).</ref><ref>Christian Fenske: Der Satz von Herbrand und einige Beweisprogramme. In: Beweisprogramme für die Prädikatenlogik und der Vollständigkeitssatz von Beth. VS Verlag für Sozialwissenschaften, Wiesbaden 1967, ISBN 978-3-322-96118-1, S. 41–52, doi:10.1007/978-3-322-96252-2_5 (springer.com [abgerufen am 19. März 2026]).</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>Alan Bundy: The computer modelling of mathematical reasoning. Academic Press, London ; New York 1983, ISBN 978-0-12-141252-4 (ed.ac.uk [PDF; abgerufen am 19. März 2026]).</ref>
Einzelnachweise
<references />