Satz von Herbrand

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 Formel in Skolemform,
F ist genau dann unerfüllbar, wenn es eine endliche Teilmenge der Herbrand-Expansion E(F) gibt, die - im aussagenlogischen Sinn - unerfüllbar ist.

Der Satz von Herbrand kann auch folgendermaßen formuliert werden:

Wenn eine geschlossene Formel kein Herbrand-Modell besitzt, so ist sie unerfüllbar.[1]

Anwendung des Satzes von Herbrand

Der Satz bildet die Grundlage eines Semi-Entscheidungsverfahrens für die Unerfüllbarkeit von prädikatenlogischen Formeln. Gesucht ist eine (einfache) Teilklasse von Strukturen/ Modellen, so dass eine Formel genau dann unerfüllbar (bzw. erfüllbar) wird, wenn sie kein (bzw. ein) Modell in dieser Teilklasse hat.

Will man von einer beliebigen prädikatenlogischen Formel F die Unerfüllbarkeit nachweisen, bringt man diese zuerst mittels gebundener Umbenennung in eine bereinigte Form. Anschließend bildet man den Existenzabschluss, um die freien Variablen zu entfernen und so eine geschlossene Formel zu erhalten. Die Quantoren werden nach links umgestellt, sodass man eine Pränex-Normalform erhält. Anschließend werden die Existenzquantoren entfernt, um eine Skolemform zu erhalten. Die Formel F', die man nach diesen Umformungsschritten erhält, ist nicht mehr äquivalent, aber erfüllbarkeitsäquivalent zur Ausgangsformel F. Diese recht schwache Eigenschaft genügt, um Unerfüllbarkeit von F nachzuweisen.

Nun bildet man zur Formel F' ein Herbrand-Universum, eine Herbrand-Struktur und darauf aufbauend eine Herbrand-Expansion. Jedes Element der Expansion lässt sich mittels einer aussagenlogischen Formel identifizieren. Dazu weist man jedem Prädikat eine aussagenlogische Variable zu. Die Belegungsfunktion bel weist einer aussagenlogischen Variable genau dann 1 zu, wenn auch das Prädikat den Wahrheitswert 1 hat. Die aussagenlogische Formel ist somit genau dann erfüllbar, wenn auch die prädikatenlogische Formel F' erfüllbar ist.

Mit dem Algorithmus von Gilmore kann man anschließend die Unerfüllbarkeit von F' und somit auch F zeigen.

Siehe auch

Einzelnachweise

  1. Gerhard Goos, Wolf Zimmermann: Vorlesungen über Informatik: Band 1: Grundlagen Und Funktionales Programmieren. ISBN 3540244050. S. 203.

Wikimedia Foundation.

Игры ⚽ Поможем сделать НИР

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

  • Herbrand — bezeichnet Herbrand (Waggonfabrik), eine ehemalige Waggonfabrik in Köln Den Familiennamen Herbrand tragen: Jacob Heerbrand (1521 1600), deutscher reformierter Theologe Jacques Herbrand (1908 1931), französischer Logiker Siehe auch: Herbrand… …   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

  • Herbrand-Universum — Mit Herbrand Universum bezeichnet man eine Menge in der Prädikatenlogik, die als Grundmenge zur Definition der Herbrand Struktur herangezogen wird. Beide Begriffe sind Teil des Herbrand Theorems, benannt nach Jacques Herbrand. Definition Sei F… …   Deutsch Wikipedia

  • Herbrand-Expansion — Die Herbrand Expansion stellt eine Menge von prädikatenlogischen Formeln dar, die aus einer gegebenen Formel F durch eine spezielle Art der Substitution abgeleitet werden können. Mit Hilfe dieser Formelmenge kann die Unerfüllbarkeit einer… …   Deutsch Wikipedia

  • Herbrand-Struktur — Eine zu einer prädikatenlogischen Formel F passende Struktur heißt Herbrand Struktur, wenn folgende Eigenschaften erfüllt sind: Das Universum ist das aus F generierte Herbrand Universum, also . Die Interpretationen I sind Herbrand… …   Deutsch Wikipedia

  • Jacques Herbrand — (* 12. Februar 1908 in Paris; † 27. Juli 1931 in La Bérarde) war ein französischer Logiker, Algebraiker und Zahlentheoretiker. Inhaltsverzeichnis …   Deutsch Wikipedia

  • Liste von Sätzen der Informatik — Inhaltsverzeichnis A B C D E F G H I J K L M N O P Q R S T U V W X Y Z C Satz von Cook: Es existiert eine Teilmenge von …   Deutsch Wikipedia

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

  • herbrandscher Satz —   [ɛr brã ], von dem französischen Mathematiker und Logiker Jacques Herbrand (* 1908, ✝ 1931) 1929 bewiesener Satz: Ist A eine Aussage der Prädikatenlogik, so lässt sich eine Disjunktion A1 ∨. .. ∨ An von aussagenlogischen Aussagen …   Universal-Lexikon

  • Liste mathematischer Sätze — Inhaltsverzeichnis A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A Satz von Abel Ruffini: eine allgemeine Polynomgleichung vom …   Deutsch Wikipedia

Share the article and excerpts

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