Citation Hunt

Bestenliste

Das unten stehende Wikipedia-Snippet wird von keiner verlässlichen Quelle unterstützt. Kannst du eine finden?

Klicke auf Verstanden!, um zu Wikipedia zu gehen und das Snippet zu reparieren, oder Nächstes!, um ein anderes zu sehen. Viel Glück!

In Seite 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 ( F ) = { A 1 , A 2 , . . . } {\displaystyle 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 {\displaystyle k{:=}1}
  • Solange ⋀ i = 1 k A i {\displaystyle \bigwedge _{i=1}^{k}A_{i}} (aussagenlogisch) erfüllbar ist, setze k := k + 1 {\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.