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:

\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 $E\left(F\right)=\left\{A_{1},A_{2},...\right\}$ sei die Herbrand-Expansion zu F und dient als Eingabe des Algorithmus.

Pseudocode:

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

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.