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:

Gilmore\left(E\left(F\right)\right)=\begin{cases}halt, & \mbox{wenn }F\mbox{ unerfüllbar} \\ undef, & \mbox{wenn }F\mbox{ 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.


Wikimedia Foundation.

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Gilmore — ist der Familienname folgender Personen: Alan C. Gilmore, neuseeländischer Astronom Alexie Gilmore (* 1976), US amerikanische Schauspielerin Alfred Gilmore (1812–1858), US amerikanischer Politiker Artis Gilmore (* 1948), US amerikanischer… …   Deutsch Wikipedia

  • Gilmore-Algorithmus — 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 sei die Herbrand… …   Deutsch Wikipedia

  • Satz von Herbrand — Der Satz von Herbrand ist ein Satz aus der Prädikatenlogik und wurde nach dem französischen Logiker Jacques Herbrand benannt. Er macht eine Aussage über die Erfüllbarkeit einer prädikatenlogischen Formel. Der Satz lautet: Sei F eine geschlossene… …   Deutsch Wikipedia

  • Herbrand-Theorie — Der nach Jacques Herbrand, einem französischen Logiker, benannte Satz von Herbrand (engl. Herbrand s theorem, was gelegentlich nicht ganz korrekt als Herbrand Theorie übersetzt wird) in der Prädikatenlogik lautet: Sei F eine geschlossene Formel… …   Deutsch Wikipedia

  • John M. Pollard — John Michael Pollard ist ein britischer Mathematiker, der Algorithmen zur Faktorisierung von großen Zahlen und für die Berechnung von diskreten Logarithmen entwickelt hat. Er war bis zu seiner Pensionierung bei der British Telecom beschäftigt. Zu …   Deutsch Wikipedia

  • Cutting Stock Problem — Das eindimensionale Zuschnittproblem (engl. one dimensional cutting stock problem) ist ein schweres ganzzahliges lineares Optimierungsproblem mit dem Ziel, eindimensionale Teile in vorgegebenen Bedarfszahlen aus möglichst wenig Stücken Material… …   Deutsch Wikipedia

  • Eindimensionales Zuschnittproblem — Das eindimensionale Zuschnittproblem (engl. one dimensional cutting stock problem) ist ein schweres ganzzahliges lineares Optimierungsproblem mit dem Ziel, eindimensionale Teile in vorgegebenen Bedarfszahlen aus möglichst wenig Stücken Material… …   Deutsch Wikipedia

  • Zuschnittproblem — Das eindimensionale Zuschnittproblem (engl. one dimensional cutting stock problem) ist ein schweres ganzzahliges lineares Optimierungsproblem mit dem Ziel, eindimensionale Teile in vorgegebenen Bedarfszahlen aus möglichst wenig Stücken Material… …   Deutsch Wikipedia

  • Zuschnittsproblem — Das eindimensionale Zuschnittproblem (engl. one dimensional cutting stock problem) ist ein schweres ganzzahliges lineares Optimierungsproblem mit dem Ziel, eindimensionale Teile in vorgegebenen Bedarfszahlen aus möglichst wenig Stücken Material… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”