Herbrand-Theorie

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

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


Wikimedia Foundation.

Игры ⚽ Нужно решить контрольную?

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

  • Theorie de la demonstration — Théorie de la démonstration La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle …   Wikipédia en Français

  • Théorie de la preuve — Théorie de la démonstration La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle …   Wikipédia en Français

  • Théorie la démonstration — Théorie de la démonstration La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle …   Wikipédia en Français

  • Herbrand-Interpretation — 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

  • Théorie de la démonstration — La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle. Hilbert a proposé cette… …   Wikipédia en Français

  • Herbrand's theorem — is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). [J. Herbrand: Recherches sur la theorie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et… …   Wikipedia

  • HERBRAND (J.) — HERBRAND JACQUES (1908 1931) Logicien et mathématicien français né à Paris et mort à Saint Christophe en Oisans dans un accident de montagne. La brève carrière de Jacques Herbrand est marquée par sa démonstration, essentiellement correcte, d’un… …   Encyclopédie Universelle

  • Théorie d'Iwasawa — La théorie d Iwasawa peut être vue comme une tentative d étendre les résultats arithmétiques classiques sur les corps de nombres (extensions finies du corps des rationnels) à des extensions infinies de , par des procédés de passage à la limite… …   Wikipédia en Français

  • Jacques Herbrand — Pour les articles homonymes, voir Herbrand. Dernière photographie de Jacques Herbrand prise au cours de l excursion où il trouva la mort Jacques Herbrand, né à Paris le 12 février …   Wikipédia en Français

  • 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

Share the article and excerpts

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