Dieser Artikel oder nachfolgende Abschnitt ist nicht hinreichend mit Belegen (beispielsweise Einzelnachweisen) ausgestattet. Angaben ohne ausreichenden Beleg könnten demnächst entfernt werden. Bitte hilf Wikipedia, indem du die Angaben recherchierst und gute Belege einfügst.

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.^[1][2]

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. Die Resolventenmethode von Robinson überkommt einige Nachteile des Algorithmus von Gilmore.^[3]

1. ↑ 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]). 
2. ↑ 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]). 
3. ↑ 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]).