Wichtiger Hinweis zum Inhalt des Online-LexikonsBei den auf dieser Seite aufgeführten Texten/Artikeln/Inhalten handelt es sich ausschließlich um fremde Inhalte, die sich die Aschendorff Verlag GmbH & Co. KG ausdrücklich nicht zu Eigen macht. Diese fremden Inhalte, die keiner regelmäßigen Überprüfung unterliegen, sind ausnahmslos solche der freien Enzyklopädie Wikipedia, für die keinerlei Verantwortung übernommen wird.

---

Lizenzbestimmungen Der Text/Artikel/Inhalt auf dieser Seite innerhalb der Rubrik "Online Lexikon" basiert, soweit nicht anders angegeben, auf dem Artikel Algorithmus von Gilmore aus der freien Enzyklopädie Wikipedia. Die Inhalte stehen unter der GNU Lizenz für freie Dokumentation. Eine Liste der Autoren ist dort abrufbar.

Algorithmus von Gilmore

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:
:

Die abzählbare Menge $E\backslash left(F\backslash right)=\backslash left\backslash \{A\_1,\; A\_2,\; ...\backslash right\backslash \}$ sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.

Pseudocode:
* $k\; \{:=\}\; 1$
* Solange $\backslash bigwedge\_\{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.

       VIDEO-NEWS UND ANGEBOTE