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:

𝐺𝑖𝑙𝑚𝑜𝑟𝑒 (E (F)) = {\begin{matrix} ℎ𝑎𝑙𝑡, & wenn F unerfüllbar \\ 𝑢𝑛𝑑𝑒𝑓, & wenn F erfüllbar \end{matrix}

Die abzählbare Menge $E (F) = {A_{1}, A_{2}, ...}$ sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.

Pseudocode:

$k := 1$
Solange $⋀_{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.

Einzelnachweise

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

[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]).