AussagenlogikPrädikatenlogik
Vorlesung “Logik”Wintersemester 2020/21Universität Duisburg-Essen
Barbara KönigÜbungsleitung: Richard Eggert
Barbara König Logik 1
AussagenlogikPrädikatenlogik
Wie geht es los?
OrganisatorischesVorstellungAblauf der Vorlesung und der Übungen (in Zeiten vonCorona . . . )Prüfung & KlausurLiteratur & Folien
Einführung und Motivation: Logik in der InformatikInhalt der Vorlesung
Barbara König Logik 2
AussagenlogikPrädikatenlogik
Wer sind wir?
Dozentin: Prof. Barbara KönigRaum LF 264E-Mail: [email protected]: nach Vereinbarung
Übungsleitung: Richard EggertRaum LF 265E-Mail: [email protected]
Web-Seite:www.uni-due.de/theoinf/teaching/ws202021_logik.php
Barbara König Logik 3
AussagenlogikPrädikatenlogik
Moodle
Wir verwenden Moodle, um:Vorlesungs- und Übungsvideos zu veröffentlichen,die Aufgabenblätter zur Verfügung zu stellen,die Hausaufgaben elektronisch (nur PDF!) abzugeben undum (anonyme) Diskussionsforen bereitzustellen.
Link:https://moodle.uni-due.de/course/view.php?id=23179
Tragen Sie sich in den Kurs “Logik (Angewandte Informatik &ISE)” (Wintersemester 2020/21 → Ingenieurwissenschaften →Informatik und Angewandte Kognitionswissenschaft) ein. Bittemöglichst mit Uni-Kennung anmelden!
Kein Zugangsschlüssel erforderlich!
Barbara König Logik 4
AussagenlogikPrädikatenlogik
Ablauf & Fragestunde
Leider können in diesem Semester keine Präsenzveranstaltungenstattfinden. Stattdessen stellen wir Vorlesungs- und Übungsvideosbereit und korrigieren Ihre Hausaufgaben.
Außerdem gibt es jede Woche eine Fragestunde per BigBlueButton(Videokonferenzsystem):
Termin wird noch per Abstimmung festgelegt, unterhttps://amazon.inf.uni-due.de/b/bar-u2k-2cr-cyh
Sie können diesen Link bereits jetzt mit Ihrem Kopfhörer, Mikrofonund Kamera testen. Für die Teilnahme an den Fragestunden sindMikrofon und vor allem Kamera nicht zwingend erforderlich.
Barbara König Logik 5
AussagenlogikPrädikatenlogik
Hinweise zu den Übungen
Machen Sie die Hausaufgaben und sehen Sie sich dieÜbungsvideos an!Stellen Sie aktiv Fragen in den (anonymen) Diskussionsforenund in den Video-Fragestunden!
Diesen Stoff kann man nur durch regelmäßiges Üben erlernen.Auswendiglernen hilft nicht besonders viel.
Barbara König Logik 6
AussagenlogikPrädikatenlogik
Hinweise zu den Übungen
Die Übungsblätter werden jeweils am Mittwoch der Vorwocheins Netz gestellt. Das erste Übungsblatt wird am 11.11.bereitgestellt.Abgabe der gelösten Aufgaben bis Mittwoch der folgendenWoche, 12:00 Uhr. In dieser Woche werden dann auch diedazugehörenden Übungsvideos hochgeladen.Elektronische Abgabe über die Lernplattform Moodle
Barbara König Logik 7
AussagenlogikPrädikatenlogik
Hinweise zu den Übungen
Bitte geben Sie auf Ihrer Lösung deutlich Ihren Namen, IhreMatrikelnummer und das Fach an.Abgaben sind nur als PDF zulässig! Bitte benennen SieDateien nach folgendem Schema (um eine eindeutigeNamenswahl zu gewährleisten): <nachname>-<blattnr>.pdfSie dürfen in Zweier-Gruppen abgeben, pro Gruppe nur eineAbgabe! Bitte beide Namen im PDF angeben!Plagiate oder das Kopieren alter Musterlösungen sindselbstverständlich nicht erlaubt! In diesem Fall vergeben wirkeine Punkte.
Barbara König Logik 8
AussagenlogikPrädikatenlogik
Prüfung
Die Prüfung findet als Klausur statt.
Voraussichtlicher Termin:
Freitag, 26. März 2021, 8:30-10:30 Uhr
Anmeldung über das Prüfungsamt im Anmeldezeitraum30.11.2020–11.12.2020
Barbara König Logik 9
AussagenlogikPrädikatenlogik
Prüfung
Es gibt folgende Bonusregelung:Wenn Sie 50% der Hausaufgabenpunkte erzielt haben, soerhalten Sie einen Bonus für die Klausur und für dieModulprüfung.Auswirkung: Verbesserung um eine Notenstufe; z.B. von 2,3auf 2,0Bonuspunkte aus dem WS 2019/20 (oder früher) gelten nichtmehr!
Barbara König Logik 10
AussagenlogikPrädikatenlogik
Literatur
Die Vorlesung basiert im Wesentlichen auf folgendem Buch:Uwe Schöning: Logik für Informatiker. Spektrum, 2000.
Weitere relevante Bücher:Jon Barwise, John Etchemendy: Language, Proof, and Logic.Seven Bridges Press, 2000.Auf Deutsch: Sprache, Beweis und Logik, Band I – Aussagen-und Prädikatenlogik. mentis, 2005.Kreuzer, Kühling: Logik für Informatiker, Pearson, 2006.
Barbara König Logik 11
AussagenlogikPrädikatenlogik
Literatur
Einführende/unterhaltsame Literatur:Douglas R. Hofstadter: Gödel, Escher, Bach: An EternalGolden Braid. Basic Books, 1999.Auf Deutsch: Gödel, Escher, Bach: Ein Endloses GeflochtenesBand. dtv, 1991.
Barbara König Logik 12
AussagenlogikPrädikatenlogik
Folien
Folien werdenim Web bereitgestellt,regelmäßig aktualisiert,im Wesentlichen den Folien des letzten Semesters (WS 19/20)entsprechen
Ein eigenes Skript gibt es – neben dem Buch von Schöning – nicht.
Barbara König Logik 13
AussagenlogikPrädikatenlogik
Geschichte der Logik
Beginn in Griechenland: Aristoteles (384–322 v.Chr.)untersucht das Wesen der Argumentation und des logischenSchließensVerschiedene Werke, u.a.: Analytica priora, AnalyticaposterioraSeither: Weiterentwicklung der Logik, Formalisierung,Verwendung in der Mathematik und Informatik
Barbara König Logik 14
AussagenlogikPrädikatenlogik
Syllogismen (I)
Aristoteles entwickelte den Begriff des Syllogismus:A syllogism is discourse in which, certain things beingstated, something other than what is stated follows of ne-cessity from their being so. I mean by the last phrase thatthey produce the consequence, and by this, that no fur-ther term is required from without in order to make theconsequence necessary.
Wenn alle Menschen sterblich sind undSokrates ein Mensch ist,dann ist Sokrates sterblich.
Barbara König Logik 15
AussagenlogikPrädikatenlogik
Syllogismen (II)
Alle Dackel sind HundeAlle Hunde sind TiereDann sind alle Dackel Tiere
Alle P sind MAlle M sind SAlle P sind S
(Barbara)
Keine Blume ist ein TierAlle Hunde sind TiereDann ist keine Blume ein Hund
Kein P ist MAlle S sind MKein P ist S
(Cesare)
Alle Delfine leben im MeerAlle Delfine sind SäugetiereDann leben einige Säugetiere im Meer
Alle M sind PAlle M sind SEinige S sind P
(Darapti)
Barbara König Logik 16
AussagenlogikPrädikatenlogik
Verschiedene Logiken
Es gibt viele verschiedene Logiken:AussagenlogikPrädikatenlogik (1. Stufe)Prädikatenlogik höherer StufeModale und temporale LogikenIntuitionistische Logik. . .
Wir beschäftigen uns in dieser Vorlesung nur mit Aussagenlogik undPrädikatenlogik 1. Stufe.
Barbara König Logik 17
AussagenlogikPrädikatenlogik
Aussagenlogik (I)
George Boole (1848)
Verknüpfung von Aussagen, die entweder wahr oder falsch seinkönnen, mit einfachen Operatoren(und; oder; nicht; wenn . . . , dann . . . )
Beispiel:Aussagen: “Es regnet”, “Die Straße ist nass”Verknüpfungen:Es regnet und die Straße ist nass.Wenn es regnet, dann ist die Straße nass.Wenn die Straße nicht nass ist, dann regnet es nicht.
Barbara König Logik 18
AussagenlogikPrädikatenlogik
Aussagenlogik (II)
Der Stoff im Bereich “Aussagenlogik” umfasst unter anderem:Syntax der Aussagenlogik:Was sind Operatoren? Was ist eine Formel? Welche Formelnsind syntaktisch korrekt?Semantik der Aussagenlogik:Was ist die Bedeutung einer Formel? Welche Formeln sindallgemeingültig, d.h. immer wahr? Welche Formeln sindunerfüllbar, d.h. immer falsch?Verfahren und Methoden, die überprüfen, ob eine Formelallgemeingültig oder unerfüllbar ist
Barbara König Logik 19
AussagenlogikPrädikatenlogik
Prädikatenlogik
Frege, Peano, Russell (Ende des 19. Jahrhunderts)
Mit der Prädikatenlogik kann man zusätzlichEigenschaften von und Beziehungen zwischen Objektenbeschreibenexistentielle Aussagen treffen: “es gibt ein x , so dass . . . ”universelle Aussagen treffen: “für jedes x gilt, dass . . . ”
Beispiel: Für jede natürliche Zahl x gilt, dass es eine natürliche Zahly gibt, so dass x kleiner als y ist.
Barbara König Logik 20
AussagenlogikPrädikatenlogik
Anwendungen in der Informatik (I)
Modellierung und Spezifikation: Eindeutige Beschreibung vonkomplexen SystemenVerifikation: Beweisen, dass ein Programm das gewünschteVerhalten zeigtSchaltkreisentwurf: Schaltkreise lassen sich als logischeFormeln darstellen Entwurf und Optimierung von SchaltungenDatenbanken: Formulierung von Anfragen an Datenbanken Abfragesprache SQL (Structured query language)Künstliche Intelligenz: Schlussfolgerungen automatisieren,insbesondere in Expertensystemen
Barbara König Logik 21
AussagenlogikPrädikatenlogik
Anwendungen in der Informatik (II)
Theorembeweiser: Der Computer beweist mathematische Sätze automatischer Beweis von wichtigen Sätzen im Bereich derBooleschen AlgebrenKombinatorische Optimierung (SAT-Solver)Logische Programmiersprachen: Prolog
Außerdem: Logik ist ein Paradebeispiel für Syntax und formaleSemantik
Ein Zitat von Edsger W. Dijkstra:Informatik = VLSAL (Very large scale application of logics)
(In Anspielung auf VLSI = Very large scale integration, ein Begriffaus dem Chipdesign)
Barbara König Logik 22
AussagenlogikPrädikatenlogik
Formale Syntax und Semantik
Auch wenn die Beispiele bisher mit natürlicher Sprache beschriebenwurden, werden wir in der Vorlesung meist auf natürliche Spracheverzichten.
Beispiele:
Natürliche Sprache FormalisierungEs regnet und die Straße ist nass. R ∧ N
Wenn es regnet, dann ist die Straße nass. R → N
Für jede natürliche Zahl x gilt, ∀x∃y(x < y)dass es eine natürliche Zahl y gibt,so dass x kleiner als y ist.
Frage: Warum nicht natürliche Sprache?
Barbara König Logik 23
AussagenlogikPrädikatenlogik
Probleme mit natürlicher Sprache (I)
Problem: Zuordnung von Wahrheitswerten zu natürlichsprachigenAussagen ist problematisch.
Beispiele:Jede gerade Zahl größer als 4 ist die Summe zweierPrimzahlen. (Goldbach’sche Vermutung, unbewiesen)Dieser Satz hat zwei Vehler.
Barbara König Logik 24
AussagenlogikPrädikatenlogik
Probleme mit natürlicher Sprache (II)
Problem: Natürliche Sprache ist oft schwer verständlich.Beispiel: Auszug aus der “Analytica Priora” von AristotelesDie Aussage: If the middle term is related universally to one of the extremes, aparticular negative syllogism must result whenever the middle term is relateduniversally to the major whether positively or negatively, and particularly tothe minor and in a manner opposite to that of the universal statement.Der Beweis: For if M belongs to no N, but to some O, it is necessary that Ndoes not belong to some O. For since the negative statement is convertible,N will belong to no M: but M was admitted to belong to some O: thereforeN will not belong to some O: for the result is reached by means of the firstfigure. Again if M belongs to all N, but not to some O, it is necessary that Ndoes not belong to some O: for if N belongs to all O, and M is predicated alsoof all N, M must belong to all O: but we assumed that M does not belongto some O. And if M belongs to all N but not to all O, we shall concludethat N does not belong to all O: the proof is the same as the above. But ifM is predicated of all O, but not of all N, there will be no syllogism.
Barbara König Logik 25
AussagenlogikPrädikatenlogik
Probleme mit natürlicher Sprache (III)
Problem: Natürliche Sprache ist mehrdeutig.
Beispiel:
Ich sah den Mann auf dem Berg mit dem Fernrohr.
Barbara König Logik 26
AussagenlogikPrädikatenlogik
Ich sah den Mann . . .
(((Ich sah den Mann) auf dem Berg) mit dem Fernrohr)
Barbara König Logik 27
AussagenlogikPrädikatenlogik
Ich sah den Mann . . .
((Ich sah (den Mann auf dem Berg)) mit dem Fernrohr)
Barbara König Logik 28
AussagenlogikPrädikatenlogik
Ich sah den Mann . . .
((Ich sah den Mann) (auf dem Berg mit dem Fernrohr))
Barbara König Logik 29
AussagenlogikPrädikatenlogik
Ich sah den Mann . . .
(Ich sah ((den Mann auf dem Berg) mit dem Fernrohr))
Barbara König Logik 30
AussagenlogikPrädikatenlogik
Ich sah den Mann . . .
(Ich sah (den Mann (auf dem Berg mit dem Fernrohr)))
Barbara König Logik 31
AussagenlogikPrädikatenlogik
Ich sah den Mann . . .
(((Ich sah den Mann) auf demBerg) mit dem Fernrohr)
((Ich sah (den Mann auf demBerg)) mit dem Fernrohr)
((Ich sah den Mann) (auf demBerg mit dem Fernrohr))
(Ich sah ((den Mann auf demBerg) mit dem Fernrohr))
(Ich sah (den Mann (auf demBerg mit dem Fernrohr)))
5 möglicheInterpretationen!
Barbara König Logik 32
AussagenlogikPrädikatenlogik
Inhalt der Vorlesung
Aussagenlogik:Grundbegriffe, Normalformen und ÄquivalenzResolution
Prädikatenlogik:Grundbegriffe, Normalformen und ÄquivalenzHerbrand-TheorieResolutionGrundlagen der Logikprogrammierung
Barbara König Logik 33
AussagenlogikPrädikatenlogik
Logik-Tools
Aussagenlogik:SAT-Solver: Überprüfen der Erfüllbarkeit vonaussagenlogischen Formeln limboole (http://fmv.jku.at/limboole/)
Prädikatenlogik:Anschauliche Lehrsoftware für die Prädikatenlogik Tarski’s WorldTheorembeweiser für die Prädikatenlogik 1. Stufe(basierend auf Resolution) otter (http://www.cs.unm.edu/˜mccune/otter/)
Barbara König Logik 34
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Menge: Menge X von Elementen, wird beschrieben als Aufzählung
X = {A1,A2,A3,A7}
oder als Menge von Elementen mit einer bestimmten Eigenschaft
X = {Ai | i ∈ N, 1 ≤ i ≤ 3 oder i = 7}.
Barbara König Logik 35
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Bemerkungen:Die Elemente einer Menge sind ungeordnet, d.h., ihre Ordnungspielt keine Rolle. Beispielsweise gilt:
{1, 2, 3} = {1, 3, 2} = {2, 1, 3} = {2, 3, 1} = {3, 1, 2} = {3, 2, 1}
Ein Element kann nicht “mehrfach” in einer Menge auftreten.Es ist entweder in der Menge, oder es ist nicht in der Menge.Beispielsweise gilt:
{1, 2, 3} 6= {1, 2, 3, 4} = {1, 2, 3, 4, 4}
Barbara König Logik 36
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Element einer Menge: Wir schreiben x ∈ X , falls ein Element x inder Menge X enthalten ist.
Teilmengenbeziehung: Für zwei Mengen X ,Y schreiben wirX ⊆ Y , falls jedes Element von X auch in Y enthalten ist. DieRelation ⊆ heißt auch Inklusion.
Leere Menge: Mit ∅ oder {} bezeichnet man die leere Menge. Sieenthält keine Elemente und ist Teilmenge jeder anderen Menge.
Barbara König Logik 37
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Kreuzprodukt (kartesisches Produkt)
Seien X ,Y zwei Mengen. Die Menge X × Y ist die Menge allerPaare (x , y), wobei die erste Komponente des Paars aus X , diezweite aus Y kommt.
X × Y = {(x , y) | x ∈ X , y ∈ Y }
Beispiel:{1, 2} × {3, 4, 5} = {(1, 3), (1, 4), (1, 5), (2, 3), (2, 4), (2, 5)}
Barbara König Logik 38
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Relation zwischen der Menge X und der Menge Y
Eine Teilmenge R ⊆ X × Y des Kreuzprodukts von X und Y heißtRelation zwischen X und Y .
Beispiel:
X = {1, 2, 3} Y = {a, b, c, d}R = {(1, a), (1, b), (2, b), (3, d)} ⊆ X × Y
Barbara König Logik 39
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Funktion von der Menge X in die Menge Y
Eine Relation f ⊆ X × Y heißt Funktion, wenn folgendes gilt:für jedes Element x ∈ X gibt es genau ein Element y ∈ Y mit(x , y) ∈ f .
Anschaulich: jedem Element der Menge X wird genau ein Elementder Menge Y zugeordnet.
Barbara König Logik 40
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengen, Relationen und Funktionen
Notation von Funktionen
f : X → Y
x 7→ f (x)
Die Funktion f bildet ein Element x ∈ X auf ein Element f (x) ∈ Yab. Dabei ist X der Definitionsbereich und Y der Wertebereich vonf .
Beispiel:
f : {A1,A2,A3,A7} → {0, 1}A1 7→ 0, A2 7→ 1, A3 7→ 0, A7 7→ 1
alternativ: f (A1) = 0, f (A2) = 1, f (A3) = 0, f (A7) = 1
Barbara König Logik 41
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Syntax der Aussagenlogik
Eine atomare Formel hat die Form Ai (wobei i = 1, 2, 3, . . .).
Definition (Formel)
Formeln werden durch folgenden induktiven Prozess definiert:1 Alle atomaren Formeln sind Formeln2 Für alle Formeln F und G sind (F ∧ G ) und (F ∨ G ) Formeln.3 Für jede Formel F ist ¬F eine Formel.
Sprechweise:(F ∧ G ): “F und G , “Konjunktion von F und G ”(F ∨ G ): “F oder G ”, “Disjunktion von F und G ”¬F : “nicht F ”, “Negation von F ”
Barbara König Logik 42
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Formel als Syntaxbaum
Jede Formel kann auch durch einen Syntaxbaum dargestellt werden.
Beispiel: F = ¬((¬A4 ∨ A1) ∧ A3)
¬
¬
A4
∨ A3
∧
A1
Barbara König Logik 43
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Teilformel
Die Teilformeln einer Formel F entsprechen den Teilbäumen.
A4
¬
¬
∨ A3
∧
A4
A1 A1
¬
¬
A4
∨ A3
∧
A1 A3
¬
¬
A4
∨
∧
A3
A1
¬A4
¬
∨ A3
∧
A4
¬ A1 (¬A4 ∨ A1)
¬
A3
∧
A4
∨
¬ A1
((¬A4 ∨ A1) ∧ A3)
¬
A4
∨
¬
∧
A3
A1 ¬((¬A4 ∨ A1) ∧ A3)
¬
A4
∨
¬
∧
A3
A1
Barbara König Logik 44
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Semantik der Aussagenlogik (I)
Die Elemente der Menge {0, 1} heißen Wahrheitswerte.
Eine Belegung ist eine Funktion A : D → {0, 1}, wobei D eineTeilmenge der atomaren Formeln ist.
Wir erweitern A zu einer Funktion A : E → {0, 1}, wobei E ⊇ Ddie Menge aller Formeln ist, die nur aus den atomaren Formeln inD aufgebaut sind.
Barbara König Logik 45
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Semantik der Aussagenlogik (II)
A(A) = A(A) falls A ∈ D eine atomare Formel ist
A((F ∧ G )) =
{1 falls A(F ) = 1 und A(G ) = 10 sonst
A((F ∨ G )) =
{1 falls A(F ) = 1 oder A(G ) = 10 sonst
A((¬F )) =
{1 falls A(F ) = 00 sonst
Wir schreiben A statt A.
Barbara König Logik 46
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Verknüpfungstafeln (I)
Beobachtung: Der Wert A(F ) hängt nur davon ab, wie A auf denden in F vorkommenden atomaren Formeln definiert ist.
Berechnung von A mit Hilfe von Verknüpfungstafeln, auchWahrheitstafeln genannt.
Tafeln für die Operatoren ∨, ∧, ¬:
A B A ∨ B
0 0 0 0 00 1 0 1 11 0 1 1 01 1 1 1 1
A B A ∧ B
0 0 0 0 00 1 0 0 11 0 1 0 01 1 1 1 1
A ¬ A
0 1 01 0 1
Barbara König Logik 47
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Abkürzungen
A,B,C oder P,Q,R oder . . . statt A1,A2,A3 . . .
(F1 → F2) statt (¬F1 ∨ F2)(F1 ↔ F2) statt ((F1 ∧ F2) ∨ (¬F1 ∧ ¬F2))
(n∨
i=1
Fi ) statt (. . . ((F1 ∨ F2) ∨ F3) ∨ . . . ∨ Fn)
(n∧
i=1
Fi ) statt (. . . ((F1 ∧ F2) ∧ F3) ∧ . . . ∧ Fn)
Barbara König Logik 48
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Verknüpfungstafeln (II)
Tafeln für die Operatoren →, ↔:
A B A → B
0 0 0 1 00 1 0 1 11 0 1 0 01 1 1 1 1
Name: Implikation, Folgerung
Interpretation: Wenn A gilt,dann muss auch B gelten.
A B A ↔ B
0 0 0 1 00 1 0 0 11 0 1 0 01 1 1 1 1
Name: Äquivalenz, Biimplikation
Interpretation: A gilt genau dann,wenn B gilt.
Barbara König Logik 49
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Präzedenzen
Präzedenz der Operatoren:
↔ bindet am schwächsten→ . . .∨ . . .∧ . . .¬ bindet am stärksten
Die FormelA↔ B ∨ ¬C → D ∧ ¬E
wird also wie folgt gelesen:
(A↔ ((B ∨ ¬C )→ (D ∧ ¬E )))
Dennoch: Zusätzliche Klammern schaden im allgemeinen nicht
Barbara König Logik 50
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Formalisierung natürlicher Sprache (I)
Ein Gerät besteht aus einem Bauteil A, einem Bauteil B und einemroten Licht. Folgendes ist bekannt:
Bauteil A oder Bauteil B (oder beide) sind kaputt.Wenn Bauteil A kaputt ist, dann ist auch Bauteil B kaputt.Wenn Bauteil B kaputt ist und das rote Licht leuchtet, dannist Bauteil A nicht kaputt.Das rote Licht leuchtet.
Formalisieren Sie diese Situation als aussagenlogische Formel undstellen Sie die Wahrheitstafel zu dieser Formel auf. Verwenden Siedazu folgende atomare Formeln: RL (rotes Licht leuchtet), AK(Bauteil A kaputt), BK (Bauteil B kaputt)
Barbara König Logik 51
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Formalisierung natürlicher Sprache (II)
Gesamte Wahrheitstafel:
(((AK ∨ BK ) ∧ (AK → BK )) ∧RL AK BK ((BK ∧ RL)→ ¬AK )) ∧ RL0 0 0 00 0 1 00 1 0 00 1 1 01 0 0 01 0 1 11 1 0 01 1 1 0
Barbara König Logik 52
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Modelle
Sei F eine Formel und A eine Belegung.Falls A für alle in F vorkommenden atomaren Formeln definiert ist,so heißt A zu F passend.
Sei A passend zu F :
Falls A(F ) = 1 so schreiben wir A |=Fund sagen F gilt unter Aoder A ist ein Modell für F
Falls A(F ) = 0 so schreiben wir A 6|=Fund sagen F gilt nicht unter Aoder A ist kein Modell für F
Barbara König Logik 53
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Gültigkeit und Erfüllbarkeit
Definition (Erfüllbarkeit)
Eine Formel F heißt erfüllbar, falls F mindestens ein Modell besitzt,andernfalls heißt F unerfüllbar.Eine (endliche oder unendliche!) Menge von Formeln M heißterfüllbar, falls es eine Belegung gibt, die für jede Formel in M einModell ist. (In diesem Fall sagt man auch, die Belegung ist einModell für die Menge M.)
Definition (Gültigkeit)
Eine Formel F heißt gültig (oder allgemeingültig oder Tautologie)falls jede zu F passende Belegung ein Modell für F ist. Wirschreiben |= F , falls F gültig ist, und 6|= F sonst.
Barbara König Logik 54
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Aufgabe
Gültig Erfüllbar UnerfüllbarA
A ∨ B
A ∨ ¬AA ∧ ¬AA→ ¬AA→ B
A→ (B → A)
A→ (A→ B)
A↔ ¬A
Barbara König Logik 55
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Aufgabe
Gelten die folgenden Aussagen?
J/N Gegenb.Wenn F gültig, dann F erfüllbarWenn F erfüllbar, dann ¬F unerfüllbarWenn F gültig, dann ¬F unerfüllbarWenn F unerfüllbar, dann ¬F gültig
Barbara König Logik 56
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Spiegelungsprinzip
¬FFG
gültigeFormeln
¬G
erfüllbare, abernicht gültige
Formeln
unerfüll-bareFormeln
Barbara König Logik 57
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Ein Gültigkeitstest
Wie kann man überprüfen, ob eine Formel F gültig (erfüllbar,unerfüllbar) ist?
Eine Möglichkeit: Wahrheitstafel aufstellen
Angenommen, die Formel F enthält n verschiedene atomareFormeln. Wie groß ist die Wahrheitstafel?
Anzahl Zeilen in der Wahrheitstafel: 2n
Geht es auch effizienter? Diese Frage wird im Laufe der Vorlesungbeantwortet.
Barbara König Logik 58
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Folgerung
Definition (Folgerung)
Eine Formel G heißt eine Folgerung der Formeln F1, . . . ,Fk falls fürjede Belegung A, die sowohl zu F1, . . . ,Fk als auch zu G passendist, gilt:
Wenn A Modell von {F1, . . . ,Fk} ist, dann ist A auchModell von G .
Wir schreiben F1, . . . ,Fk |= G , falls G eine Folgerung vonF1, . . . ,Fk ist.
Barbara König Logik 59
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Folgerung: Beispiel
(AK ∨ BK ), (AK → BK ),
((BK ∧ RL)→ ¬AK ),RL |= RL ∧ ¬AK ∧ BK
Wenn Bauteil A oder Bauteil B kaputt ist und daraus, dassBauteil A kaputt ist, immer folgt, dass Bauteil B kaputt ist und . . .
. . . dann kann man die Folgerung ziehen: das rote Licht leuchtet,Bauteil A ist nicht kaputt und Bauteil B ist kaputt.
Barbara König Logik 60
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Aufgabe
M F Gilt M |= F?A (A ∨ B)
A (A ∧ B)
A,B (A ∨ B)
A,B (A ∧ B)
(A ∧ B) A
(A ∨ B) A
A, (A→ B) B
Barbara König Logik 61
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Folgerung, Gültigkeit und Unerfüllbarkeit
Zeigen Sie, dass folgende Aussagen äquivalent sind:1 F1, . . . ,Fk |= G , d.h., G ist eine Folgerung von F1, . . . ,Fk .2 ((
∧ki=1 Fi )→ G ) ist gültig.
3 ((∧k
i=1 Fi ) ∧ ¬G ) ist unerfüllbar.
Barbara König Logik 62
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Äquivalenz
(Semantische) Äquivalenz
Zwei Formeln F und G heißen (semantisch) äquivalent, falls für alleBelegungen A, die sowohl für F als auch für G passend sind,A(F ) = A(G ) gilt. Hierfür schreiben wir F ≡ G .
Barbara König Logik 63
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Aufgabe
Gelten die folgenden Äquivalenzen?
(A ∧ (A ∨ B)) ≡ A
¬(A ∨ B) ≡ (¬A ∧ ¬B)(A ∧ (B ∨ C )) ≡ ((A ∧ B) ∨ C )
(A ∧ (B ∨ C )) ≡ ((A ∧ B) ∨ (A ∧ C ))
Barbara König Logik 64
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Die Hauptprobleme
ModellprüfungSei F eine Formel und sei A eine passende Belegung. GiltA(F ) = 1?ErfüllbarkeitSei F eine Formel. Ist F erfüllbar?GültigkeitSei F eine Formel. Ist F gültig?FolgerungSeien F und G Formeln. Gilt F |= G?ÄquivalenzSeien F und G Formeln. Gilt F ≡ G?
Barbara König Logik 65
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Reduktion von Problemen (I)
Welche Probleme lassen sich auf welche reduzieren?
Gültigkeit ⇐⇒ (Nicht)Erfüllbarkeit:F gültig gdw. ¬F nicht erfüllbarF erfüllbar gdw. ¬F nicht gültig
Gültigkeit =⇒ Folgerung:F gültig gdw. T |= F (T ist beliebige gültige Formel)Folgerung =⇒ Gültigkeit:
F |= G gdw. F → G gültig
Barbara König Logik 66
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Reduktion von Problemen (II)
Unerfüllbarkeit =⇒ Folgerung:F unerfüllbar gdw. F |= U
(U ist beliebige unerfüllbare Formel)Folgerung =⇒ Unerfüllbarkeit:
F |= G gdw. F ∧ ¬G unerfüllbar
Barbara König Logik 67
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Reduktion von Problemen (III)
Gültigkeit =⇒ Äquivalenz:F gültig gdw. F ≡ T (T ist beliebige gültige Formel)Äquivalenz =⇒ Gültigkeit:
F ≡ G gdw. F ↔ G gültig
Bemerkung: Eine gültige Formel bezeichnet man manchmal auchmit 1, eine unerfüllbare Formel mit 0.
Barbara König Logik 68
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Eigenschaften der Äquivalenz
Wir betrachten nun wieder die Äquivalenz auf Formeln. Sie hatfolgende Eigenschaften:
reflexiv: Es gilt F ≡ F für jede Formel F (jede Formel ist zusich selbst äquivalent)
symmetrisch: Falls F ≡ G gilt, so gilt auch G ≡ F
transitiv: Falls F ≡ G und G ≡ H gilt, so gilt auch F ≡ H
abgeschlossen unter Operatoren: Falls F1 ≡ F2 und G1 ≡ G2 gilt,so gilt auch (F1 ∧ G1) ≡ (F2 ∧ G2),(F1 ∨ G1) ≡ (F2 ∨ G2) und ¬F1 ≡ ¬F2.
Reflexive, symmetrische, transitive Relation Äquivalenzrelation
Äquivalenzrelation + Abgeschlossenheit unterOperatoren Kongruenzrelation
Barbara König Logik 69
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Ersetzbarkeitstheorem
Die Abgeschlossenheit unter Operatoren lässt sich auchfolgendermaßen formulieren:
Satz (Ersetzbarkeitstheorem)
Seien F und G äquivalente Formeln (F ≡ G ). Sei H eine Formelmit (mindestens) einem Vorkommen der Teilformel F . Dann ist Häquivalent zu H ′ (d.h. H ≡ H ′), wobei H ′ aus H hervorgeht, indem(irgend)ein Vorkommen von F in H durch G ersetzt wird.
Barbara König Logik 70
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Äquivalenzen (I)
Satz
Es gelten die folgenden Äquivalenzen:
(F ∧ F ) ≡ F(F ∨ F ) ≡ F (Idempotenz)
(F ∧ G ) ≡ (G ∧ F )
(F ∨ G ) ≡ (G ∨ F ) (Kommutativität)
((F ∧ G ) ∧ H) ≡ (F ∧ (G ∧ H))
((F ∨ G ) ∨ H) ≡ (F ∨ (G ∨ H)) (Assoziativität)
(F ∧ (F ∨ G )) ≡ F
(F ∨ (F ∧ G )) ≡ F (Absorption)
Barbara König Logik 71
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Äquivalenzen (II)
(F ∧ (G ∨ H)) ≡ ((F ∧ G ) ∨ (F ∧ H))(F ∨ (G ∧ H)) ≡ ((F ∨ G ) ∧ (F ∨ H)) (Distributivität)
¬¬F ≡ F (Doppelnegation)
¬(F ∧ G ) ≡ (¬F ∨ ¬G ) (de Morgansche¬(F ∨ G ) ≡ (¬F ∧ ¬G ) Regeln)
(F ∨ G ) ≡ F , falls F gültig (Tautologie-(F ∧ G ) ≡ G , falls F gültig regeln)
(F ∨ G ) ≡ G , falls F unerfüllbar (Unerfüllbarkeits-(F ∧ G ) ≡ F , falls F unerfüllbar regeln)
Barbara König Logik 72
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Äquivalenzen
Die Tautologie- und Unerfüllbarkeitsregeln können auchfolgendermaßen geschrieben werden:
(1 ∨ G ) ≡ 1(1 ∧ G ) ≡ G (Tautologieregeln)
(0 ∨ G ) ≡ G
(0 ∧ G ) ≡ 0 (Unerfüllbarkeitsregeln)
Daraus folgt unter anderem, dass 1 (= gültige Formel) das neutraleElement der Konjunktion und 0 (= unerfüllbare Formel) dasneutrale Element der Disjunktion ist.
Barbara König Logik 73
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Normalformen (I)
Definition (Normalformen)
Ein Literal ist eine atomare Formel oder die Negation eineratomaren Formel. (Im ersten Fall sprechen wir von einem positiven,im zweiten Fall von einem negativen Literal).Eine Formel F ist in konjunktiver Normalform (KNF), falls sie eineKonjunktion von Disjunktionen von Literalen ist:
F = (n∧
i=1(mi∨j=1
Li ,j)),
wobei Li ,j ∈ {A1,A2, · · · } ∪ {¬A1,¬A2, · · · }
Eine Disjunktion von Literalen nennt man auch Klausel. EineFormel in KNF besteht also aus einer Konjunktion von Klauseln.
Barbara König Logik 74
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Normalformen (II)
Eine Formel F ist in disjunktiver Normalform (DNF), falls sie eineDisjunktion von Konjunktionen von Literalen ist:
F = (n∨
i=1(mi∧j=1
Li ,j)),
wobei Li ,j ∈ {A1,A2, · · · } ∪ {¬A1,¬A2, · · · }
Barbara König Logik 75
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Umformungsmethode (in KNF)
Gegeben: eine Formel F , die in eine äquivalente Formel in KNFumgeformt wird.
1 Ersetze in F jedes Vorkommen einer Teilformel der Bauart
¬¬G durch G
¬(G ∧ H) durch (¬G ∨ ¬H)
¬(G ∨ H) durch (¬G ∧ ¬H)
bis keine derartige Teilformel mehr vorkommt.2 Ersetze jedes Vorkommen einer Teilformel der Bauart
(F ∨ (G ∧ H)) durch ((F ∨ G ) ∧ (F ∨ H))
((F ∧ G ) ∨ H) durch ((F ∨ H) ∧ (G ∨ H))
bis keine derartige Teilformel mehr vorkommt.Barbara König Logik 76
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Umformungsmethode (in KNF)
Aufwand der UmformungsmethodeBei der Umwandlung einer Formel in KNF kann die Formelexponentiell größer werden.
Beispiel: F = (A1 ∧ B1) ∨ (A2 ∧ B2) ∨ · · · ∨ (An ∧ Bn)(bestehend aus n Konjunktionen).Bei Umwandlung in KNF ergeben sich durch das Distributivgesetz2n Disjunktionen, da jede Kombination von Literalen (eines ausjeder Konjunktion) eine neue Disjunktion ergibt.
F ≡ (A1 ∨ A2 ∨ · · · ∨ An)
∧ (B1 ∨ A2 ∨ · · · ∨ An)
∧ (A1 ∨ B2 ∨ · · · ∨ An)
∧ . . .
Barbara König Logik 77
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengendarstellung in KNF
Klausel: Menge von Literalen (Disjunktion).{A,B} stellt (A ∨ B) dar.
Formel in KNF: Menge von Klauseln (Konjunktion).{{A,B}, {¬A,B}} stellt ((A ∨ B) ∧ (¬A ∨ B)) dar.
Die leere Klausel ist äquivalent zu einer unerfüllbaren Formel (0).Die leere Formel ist äquivalent zu einer gültigen Formel (1).
Barbara König Logik 78
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Ablesen von DNF und KNF aus Wahrheitstafel
A B C F
0 0 0 10 0 1 00 1 0 00 1 1 01 0 0 11 0 1 01 1 0 01 1 1 1
DNF: Aus jeder Zeile mit Wahrheitswert 1wird eine Konjunktion, aus einer 0 in derSpalte A wird ¬A, aus einer 1 wird A
(¬A ∧ ¬B ∧ ¬C )
∨ (A ∧ ¬B ∧ ¬C ) ∨ (A ∧ B ∧ C )
KNF: Aus jeder Zeile mit Wahrheitswert 0wird eine Disjunktion, aus einer 0 in derSpalte A wird A, aus einer 1 wird ¬A
(A ∨ B ∨ ¬C ) ∧ (A ∨ ¬B ∨ C )
∧ (A ∨ ¬B ∨ ¬C ) ∧ (¬A ∨ B ∨ ¬C )
∧ (¬A ∨ ¬B ∨ C )
Barbara König Logik 79
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Erfüllbarkeits-/Gültigkeitstests für DNF/KNF
Für Formeln in DNF gibt es einen einfachen Erfüllbarkeitstest.
Erfüllbarkeitstest für Formeln in DNFEine Formel in disjunktiver Normalform ist erfüllbar, genau dannwenn sie eine Konjunktion (L1 ∧ · · · ∧ Ln) enthält, in der jedesLiteral entweder nur positiv oder nur negativ vorkommt. Das heißt,es gibt keine atomare Formel A, die sowohl als A als auch als ¬A indieser Konjunktion vorkommt.
Beispiele:(A ∧ B ∧ ¬C ) ∨ (¬A ∧ ¬B) ∨ (B ∧ ¬B)ist erfüllbar, beispielsweise mit der Belegung A(A) = 1,A(B) = 1, A(C ) = 0.(A ∧ B ∧ ¬A) ∨ (¬A ∧ ¬B ∧ A ∧ B ∧ C ) ∨ (B ∧ ¬B)ist nicht erfüllbar (= unerfüllbar).
Barbara König Logik 80
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Erfüllbarkeits-/Gültigkeitstests für DNF/KNF
Für Formeln in KNF gibt es einen einfachen Gültigkeitstest.
Gültigkeitstest für Formeln in KNFEine Formel in konjunktiver Normalform ist gültig, genau dannwenn es in jeder vorkommenden Disjunktion (L1 ∨ · · · ∨ Ln) einLiteral gibt, das sowohl positiv als auch negativ vorkommt. Dasheißt, es gibt in jeder Disjunktion eine atomare Formel A, diesowohl als A als auch als ¬A vorkommt.
Beispiele:(A ∨ B ∨ ¬C ) ∧ (¬A ∨ ¬B) ∧ (B ∨ ¬B)ist nicht gültig, beispielsweise erhält man 0 bei Auswertungunter der Belegung A(A) = 0, A(B) = 0, A(C ) = 1.(A ∨ B ∨ ¬A) ∧ (¬A ∨ ¬B ∨ A ∨ B ∨ C ) ∧ (B ∨ ¬B)ist gültig.
Barbara König Logik 81
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Erfüllbarkeits-/Gültigkeitstests für DNF/KNF
Aufwand der Tests:Diese einfachen Erfüllbarkeits- bzw. Gültigkeitstests könnendurchgeführt werden, indem man einmal die Formel durchläuft.Das heißt, man benötigt nur lineare Zeit.Trotzdem erhält man dadurch keinen einfachenErfüllbarkeitstest für Formeln in KNF und keinen einfachenGültigkeitstest für Formeln in DNF.Dazu müsste man eine Formel in KNF erst in DNF umwandeln(oder umgekehrt), was exponentielle Zeit in Anspruch nehmenkann.
Barbara König Logik 82
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Erfüllbarkeits-/Gültigkeitstests für DNF/KNF
Das Problem, die Erfüllbarkeit einer beliebigen Formel (oder einerFormel in KNF) zu bestimmen ist auch als SAT-Problem(Satisfiability-Problem) bekannt.
SAT ist NP-vollständig ( “Berechenbarkeit und Komplexität”),was bedeutet, dass es (zur Zeit) keinen bekanntenPolynomzeit-Algorithmus für dieses Problem gibt. Ob ein solcherPolynomzeit-Algorithmus existiert, ist ein offenes Problem.
Es gibt jedoch einige Verfahren, die zumindest in vielen Fällen sehreffizient sind (z.B. limboole und das im folgenden besprocheneResolutionsverfahren).
Barbara König Logik 83
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Gültigkeits- und Erfüllbarkeitstests mit limboole
limboole – fmv.jku.at/limboole/
limboole ist ein Tool, mit dem Gültigkeits- undErfüllbarkeitstests für aussagenlogische Formeln durchgeführtwerden können.Wir werden in der Vorlesung dafür noch effiziente Verfahrenkennenlernen. (Allerdings verwendet limboole etwas andere,stärker optimierte, Verfahren.)Es gibt noch zahlreiche andere Tools dieser Art, dienormalerweise als SAT-Solver bezeichnet werden.Anders als andere Werkzeuge konvertiert limboole selbst dieEingabe in (konjunktive) Normalform.
Barbara König Logik 84
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Gültigkeits- und Erfüllbarkeitstests mit limboole
Eingabeformat für limboole
Aussagenlogik limboole↔ <->→ ->∨ |∧ &¬ !
limboole kann für eine Formel F sowohl überprüfen,ob sie gültig (valid) oder nicht gültig (invalid) ist als auchob sie erfüllbar (satisfiable) oder unerfüllbar (unsatisfiable) ist.
Bei einer nicht-gültigen Formel F wird eine Belegung A mitA(F ) = 0 ausgegeben, bei einer erfüllbaren Formel eine BelegungA mit A(F ) = 1.
Barbara König Logik 85
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Diagnose
Um zu zeigen, dass
F︷ ︸︸ ︷(AK ∨ BK ), (AK → BK ), ((BK ∧ RL)→ ¬AK ),RL
|= RL ∧ ¬AK ∧ BK︸ ︷︷ ︸G
gilt, überprüfen wir, ob F → G gültig ist. Diese Formel sieht inlimboole-Syntax folgendermaßen aus:
((AK | BK) & (AK -> BK) & ((BK & RL) -> !AK) & RL)-> (!AK & BK & RL)
Barbara König Logik 86
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Vergleich von Schaltkreisen
Aufgabe: Gegeben sind zwei Schaltkreise. Überprüfen Sie, ob dieseSchaltkreise äquivalent sind, in dem Sinne, dass sie bei gleicherEingabe die gleichen Ausgaben liefern.
Diese Überprüfung soll mit Hilfe von limboole durchgeführtwerden und nutzt die Tatsache, dass
F ≡ G gdw. F ↔ G gültig ist.
Barbara König Logik 87
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Vergleich von Schaltkreisen
Schaltkreis 1:
∨
∧
∧
∧
Nor
X1
Y1
X2
Y2
∨
Nor
Barbara König Logik 88
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Vergleich von Schaltkreisen
Schaltkreis 2:
∧
∧
∧
¬¬
¬
X1
Y1
X2
Y2∧
∨
Barbara König Logik 89
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Vergleich von Schaltkreisen
Formel S1 für Schaltkreis 1 (in limboole-Syntax)
(((X1 & Y1) | !(X1 | Y1)) & ((X2 & Y2) | !(X2 | Y2))
Formel S2 für Schaltkreis 1 (in limboole-Syntax)
(X1 & Y2 & X2 & Y1) | (X2 & Y2 & !X1 & !Y1) |(X1 & Y1 & !X2 & Y2) | (!X2 & !X1 & !Y1 & Y2)
Barbara König Logik 90
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Vergleich von Schaltkreisen
Mit Hilfe von limboole lässt sich feststellen, dass die FormelS1 ↔ S2 nicht gültig ist, das heißt die Schaltkreise sind nichtäquivalent.
Zusatzaufgabe: wie kann man mit Hilfe von limboole überprüfen,auf welchen Eingaben sich die beiden Schaltkreise unterscheiden?
Barbara König Logik 91
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Vollständigkeit von Operatormengen
Definition (Boolesche Funktionen)
Eine Funktion der Form b : {0, 1}n → {0, 1} heißt (n-stellige)Boolesche Funktion.
Eine Formel F mit atomaren Formeln aus der Menge {A1, . . . ,An}beschreibt eine n-stellige Boolesche Funktion bF wie folgt:
bF (x1, . . . , xn) = Ax1,...,xn(F ),
wobei Ax1,...,xn die Belegung ist, die Ai mit xi ∈ {0, 1} belegt.
Die n-stelligen Booleschen Funktionen entsprechen genau denWahrheitstafeln mit n Spalten für atomare Formeln und einerErgebnisspalte.
Barbara König Logik 92
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Vollständigkeit von Operatormengen
Daher gibt es genau 22n n-stellige Boolesche Funktionen bzw.Wahrheitstafeln mit n atomaren Formeln.
Aufgabe: Stellen Sie alle 16 Wahrheitstafeln mit zwei atomarenFormeln auf, d.h., bestimmen Sie alle zweistelligen BooleschenFunktionen. Versuchen Sie, jeder Wahrheitstafel den Operator oderdie Formel zuzuordnen, die sie beschreibt.
Barbara König Logik 93
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Vollständigkeit von Operatormengen
Definition (Vollständigkeit)
Eine Menge von Operatoren heißt vollständig, wenn man damit fürjede Boolesche Funktion eine entsprechende Formel erstellen kann,die diese Funktion beschreibt.
Die Operatormenge {¬,∨,∧} ist vollständig.Begründung: wie vorher beschrieben kann jede beliebigeWahrheitstafel in KNF bzw. DNF umgewandelt werden.Die Operatormenge {¬,∨} ist vollständig.Begründung: A ∧ B ≡ ¬(¬A ∨ ¬B).Die Operatormenge {¬,∧} ist vollständig.Die Operatormenge {¬,→} ist vollständig.Begründung: A ∨ B ≡ ¬A→ B .
Barbara König Logik 94
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Vollständigkeit von Operatormengen
Die Operatormenge {Nand} ist vollständig, wobei derOperator Nand wie folgt definiert ist: ANandB = ¬(A ∧ B).Begründung: ANandA = ¬(A ∧ A) ≡ ¬A und(ANandB)Nand (ANandB) ≡ A ∧ B .Die Operatormenge {Nor} ist vollständig, wobei der OperatorNor wie folgt definiert ist: ANorB = ¬(A ∨ B).
Barbara König Logik 95
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Vollständigkeit von Operatormengen
Die Operatormenge {∧,∨} ist nicht vollständig.Begründung: Die Formel ¬A kann nicht dargestellt werden.Falls eine Formel nur aus Operatoren der Form ∧ und ∨besteht und der Wahrheitswert 1 eingesetzt wird, so erhältman wieder 1. Das ist aber bei ¬A nicht der Fall.Die Operatormenge {→} ist nicht vollständig.Begründung: analog zu {∧,∨}Man erhält jedoch Vollständigkeit, wenn man auch dieKonstante 0 (“falsch”) zulässt. Dann gilt A→ 0 ≡ ¬A und ∨kann wie oben beschrieben mit Hilfe von ¬ und → dargestelltwerden.Die Operatormenge {¬,↔} ist nicht vollständig (ohneBegründung).
Barbara König Logik 96
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Endlichkeitssatz
Definition (Erfüllbarkeit einer Menge) – Wiederholung
Eine (möglicherweise unendliche) Menge M von aussagenlogischenFormeln heißt erfüllbar genau dann, wenn es eine Belegung A gibt,die für alle Formeln in M passend ist und für die gilt A(F ) = 1 füralle F ∈ M.
Endlichkeitssatz (compactness theorem)
Eine Menge M von Formeln ist erfüllbar genau dann, wenn jede derendlichen Teilmengen von M erfüllbar ist.
Barbara König Logik 97
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Endlichkeitssatz
Beweis (Skizze):
1. Schritt: Zerlegung von M in Mengen M1,M2,M3, . . . , wobei Mi
genau die Formeln von M enthält, die aus den atomaren FormelnA1, . . . ,Ai bestehen. Es gilt:
M1 ⊆ M2 ⊆ M3 ⊆ . . .M =
⋃∞i=1 Mi
Problem: Jede Menge Mi kann unendlich viele Formeln enthalten.(Beispielsweise könnte M1 die Formeln A1, ¬A1, ¬¬A1, ¬¬¬A1,. . . enthalten.)Da es jedoch höchstens 22i verschiedene i-stellige BoolescheFunktionen geben kann, kann man diese in endlich vieleÄquivalenzklassen zusammenfassen.
Barbara König Logik 98
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Endlichkeitssatz
2. Schritt: Wir zeigen nun, dass M erfüllbar ist, wenn jede endlicheTeilmenge von M (insbesondere jede Menge Mi ) erfüllbar ist. Sei Ai
ein Modell für Mi . Wir konstruieren ein Modell A von M wie folgt:1 Setze I := {1, 2, 3, . . . }2 Stufe n > 0 (Wahrheitswert für An wird festgelegt)
Falls es unendlich viele Indizes i ∈ I gibt mit Ai (An) = 1,dann setze A(An) = 1 und entferne aus I alle Indizes j ,für die Aj(An) = 0 gilt.Sonst: setze A(An) = 0 und entferne aus I alle Indizes j ,für die Aj(An) = 1 gilt.
3. Schritt: Zeige, dass A tatsächlich ein Modell für M ist.
Barbara König Logik 99
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Endlichkeitssatz
Bemerkungen zum Endlichkeitssatz:Der Beweis ist nicht-konstruktiv, er zeigt nur, dass es einModell A gibt, nicht wie man es erhält.Aussagen der Form “es gibt unendlich viele i ∈ I mit . . . ”können nicht in eine (mechanische) Konstruktion umgewandeltwerden.Korollar: Wenn M eine unerfüllbare Menge ist, dann ist bereitseine endliche Teilmenge von M unerfüllbar.Die Bedeutung des Endlichkeitssatzes liegt vor allem in seinenAnwendungsmöglichkeiten im Bereich der Prädikatenlogik(siehe 2. Kapitel der Vorlesung).
Barbara König Logik 100
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolution (Motivation)
Wir benötigen Algorithmen für Erfüllbarkeitstests, die zumindest invielen Fällen gutartiges Verhalten zeigen.
Dennoch ist im schlimmsten Fall (worst case) immer eineexponentielle Laufzeit zu erwarten.
Wir betrachten nun Resolution als Erfüllbarkeitstest unduntersuchen dann einige Fallstudien mit schlechtem bzw. gutemLaufzeitverhalten.
Barbara König Logik 101
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolution (Idee)
Wir betrachten im folgenden nur Formeln in KNF.
Es gilt (für Formeln F ,G und eine atomare Formel A):
(F ∨ A) ∧ (G ∨ ¬A) |= (F ∨ G )
Aus der Herleitung der leeren Disjunktion bzw. leeren Klausel (=unerfüllbare Formel 0) folgt Unerfüllbarkeit. (Korrektheit)(Siehe auch der Zusammenhang zwischen Folgerung undUnerfüllbarkeit: F unerfüllbar gdw. F |= 0.)
Zwei Fragen:Kann man aus einer unerfüllbaren Formel immer die leereKlausel herleiten? (Vollständigkeit)Gibt es eine Möglichkeit, die Herleitung kompakteraufzuschreiben?
Barbara König Logik 102
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolution (Idee)
Es gilt:
F |= G ⇐⇒ F ≡ F ∧ G
Daraus folgt:
(F ∨ A) ∧ (G ∨ ¬A) ≡ (F ∨ A) ∧ (G ∨ ¬A) ∧ (F ∨ G )
Das kann so interpretiert werden, dass man zu den bisherexistierenden Klauseln (F ∨ A), (G ∨ ¬A) die Klausel (F ∨ G )hinzufügt, ohne die Aussage der Formel zu verändern.Dies macht man so lange, bis man die leere Klausel erhält, odersich sicher sein kann, dass die leere Klausel nicht auftaucht.
Barbara König Logik 103
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Mengendarstellung der KNF
Klausel: Menge von Literalen (Disjunktion).{A,B} stellt (A ∨ B) dar.
Formel: Menge von Klauseln (Konjunktion).{{A,B}, {¬A,B}} stellt ((A ∨ B) ∧ (¬A ∨ B)) dar.
Die leere Klausel (= leere Disjunktion) ist äquivalent zu einerunerfüllbaren Formel. Diese wird auch mit � bezeichnet.
Die leere Formel (= leere Konjunktion) ist äquivalent zu einergültigen Formel.
Barbara König Logik 104
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Vorteile der Mengendarstellung
Man erhält automatisch:Kommutativität:(A ∨ B) ≡ (B ∨ A),beide dargestellt durch {A,B}Assoziativität:((A ∨ B) ∨ C ) ≡ (A ∨ (B ∨ C )),beide dargestellt durch {A,B,C}Idempotenz:(A ∨ A) ≡ A,beide dargestellt durch {A}
Barbara König Logik 105
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolvent (I)
Definition (Resolvent)
Seien K1, K2 und R Klauseln. Dann heißt R Resolvent von K1 undK2, falls es ein Literal L gibt mit L ∈ K1 und L ∈ K2 und R dieForm hat:
R = (K1 − {L}) ∪ (K2 − {L}).
Hierbei ist L definiert als
L =
{¬Ai falls L = Ai ,Ai falls L = ¬Ai
Barbara König Logik 106
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolvent (II)
Wir stellen diesen Sachverhalt durch folgendes Diagramm dar(Sprechweise: R wird aus K1, K2 nach L resolviert).
K1 K2
R
Ferner: falls K1 = {L} und K2 = {L}, so entsteht die leere Mengeals Resolvent. Diese wird mit dem speziellen Symbol � bezeichnet,das eine unerfüllbare Formel darstellt.
Barbara König Logik 107
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolutions-Lemma
Resolutions-LemmaSei F eine Formel in KNF, dargestellt als Klauselmenge. Ferner seiR ein Resolvent zweier Klauseln K1 und K2 in F . Dann sind F undF ∪ {R} äquivalent.
Beweis: Folgt direkt aus
(F1 ∨ A)︸ ︷︷ ︸K1
∧ (F2 ∨ ¬A)︸ ︷︷ ︸K2
≡ (F1 ∨ A)︸ ︷︷ ︸K1
∧ (F2 ∨ ¬A)︸ ︷︷ ︸K2
∧ (F1 ∨ F2)︸ ︷︷ ︸R
Barbara König Logik 108
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Definition von Res(F )
DefinitionSei F eine Klauselmenge. Dann ist Res(F ) definiert als
Res(F ) = F ∪ {R | R ist Resolvent zweier Klauseln in F}.
Außerdem setzen wir:
Res0(F ) = F
Resn+1(F ) = Res(Resn(F )) für n ≥ 0
und schließlich sei
Res∗(F ) =⋃
n≥0
Resn(F ).
Barbara König Logik 109
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anzahl der Resolventen
Angenommen, die Formel F enthält n atomare Formeln. Dann giltwelche Abschätzung für Res∗(F )?
A |Res∗(F )| ≤ 2n B |Res∗(F )| ≤ 4n
C |Res∗(F )| kann beliebig groß werden
Dabei bezeichnet |Res∗(F )| die Anzahl der Elemente in Res∗(F ).
Es gilt |Res∗(F )| ≤ 4n
4n ist eine obere Schranke für die Menge aller Klauseln (jedeatomare Formel kann auf vier verschieden Arten in einer Klauselvorkommen: gar nicht, nur positiv, nur negativ, positiv undnegativ).
Barbara König Logik 110
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anzahl der Resolventen
Was passiert, wenn alle Klauseln maximal zweielementig sind?Durch die Resolution von zweielementigen Klauseln können nurwieder maximal zweielementige Klauseln entstehen. (Das ist beidrei- und mehrelementigen Klauseln anders.)
Da es bei n verschiedenen atomaren Formeln nur(2n
2
)= 2n(2n−1)
2viele zweielementige und 2n viele einelementige Klauseln gibt,werden nach spätestens dieser polynomialen Anzahl von Schrittenkeine neuen Klauseln mehr abgeleitet.
Barbara König Logik 111
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolutionssatz
Wir zeigen nun die Korrektheit und Vollständigkeit der Resolution:
Resolutionssatz (der Aussagenlogik)
Eine Klauselmenge F ist unerfüllbar genau dann, wenn� ∈ Res∗(F ).
Diese Aussage beinhaltet zwei Teile:Wenn � ∈ Res∗(F ), dann ist F unerfüllbar.(Korrektheit, folgt unmittelbar aus dem Resolutionslemma)Wenn F unerfüllbar ist, dann � ∈ Res∗(F ).(Vollständigkeit, muss noch – per Induktion – bewiesenwerden)
Barbara König Logik 112
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Induktionsprinzip
Um die AussageFür jedes n ∈ {0, 1, 2, 3, . . .} gilt P(n).
zu zeigen, gehen wir im allgemeinen folgendermaßen vor:Wir zeigen, dass P(0) gilt. (Induktionsanfang)Wir zeigen, dass für jedes n gilt:Wenn P(n) gilt, dann gilt auch P(n + 1). (Induktionsschritt)
Dann kann man schließen, dass P(n) für jedes beliebige n gilt.
Barbara König Logik 113
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beweisidee (I)
Vollständigkeitsbeweis: Induktion über die Anzahl der atomarenFormeln.
Hier: Induktionsschritt mit n + 1 = 4
F = {{A1}, {¬A2,A4}, {¬A1,A2,A4}, {A3,¬A4}, {¬A1,¬A3,¬A4}}
Barbara König Logik 114
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beweisidee (I)
Vollständigkeitsbeweis: Induktion über die Anzahl der atomarenFormeln.
Hier: Induktionsschritt mit n + 1 = 4
F = {{A1}, {¬A2,A4}, {¬A1,A2,A4}, {A3,¬A4}, {¬A1,¬A3,¬A4}}
F0 = {{A1}, {¬A2}, {¬A1,A2}} A4 wird mit 0 belegt
Barbara König Logik 114
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beweisidee (I)
Vollständigkeitsbeweis: Induktion über die Anzahl der atomarenFormeln.
Hier: Induktionsschritt mit n + 1 = 4
A4 wird mit 0 belegt
A4 wird mit 1 belegt
F = {{A1}, {¬A2,A4}, {¬A1,A2,A4}, {A3,¬A4}, {¬A1,¬A3,¬A4}}
F0 = {{A1}, {¬A2}, {¬A1,A2}}F1 = {{A1}, {A3}, {¬A1,¬A3}}
Barbara König Logik 114
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beweisidee (II)
{¬A2} {¬A1,A2} {¬A1,¬A3}{A1} {A3}
{¬A1} {¬A1}
F0 F1
Barbara König Logik 115
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beweisidee (II)
{A1}F0 F1
{¬A2,A4} {¬A1,A2,A4} {¬A1,¬A3,¬A4}{A3,¬A4}
{¬A1,¬A4}{¬A1,A4}
{A4} {¬A4}
Barbara König Logik 115
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beweisidee (II)
{A1}F0 F1
{¬A2,A4} {¬A1,A2,A4} {¬A1,¬A3,¬A4}{A3,¬A4}
{¬A1,¬A4}{¬A1,A4}
{A4} {¬A4}
Barbara König Logik 115
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Deduktion
Definition (Deduktion)
Eine Deduktion (oder Herleitung oder Beweis) der leeren Klauselaus einer Klauselmenge F ist eine Folge von K1,K2, . . . ,Km vonKlauseln mit folgenden Eigenschaften:
Km ist die leere Klausel und für jedes i = 1, . . . ,m gilt, dassKi entweder Element von F ist oder aus gewissen KlauselnKa,Kb mit a, b < i resolviert werden kann.
Eine Klauselmenge ist unerfüllbar genau dann, wenn eine Deduktionder leeren Klausel existiert.Es ist also nicht notwendig, ganz Res∗(F ) zu berechnen, sondern eskönnen geeignete Such-Heuristiken verwendet werden.
Barbara König Logik 116
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Resolutionskalkül
Mit dem Begriff Kalkül bezeichnet man eine Menge vonsyntaktischen Umformungsregeln, mit denen man semantischeEigenschaften herleiten kann.
Syntaktische Umformungsregeln: Resolution, Stopp beiErreichen der leeren KlauselSemantische Eigenschaft: Unerfüllbarkeit
Wünschenswerte Eigenschaften eines Kalküls:Korrektheit: Wenn die leere Klausel aus F abgeleitet werdenkann, dann ist F unerfüllbar.Vollständigkeit: Wenn F unerfüllbar ist, dann ist die leereKlausel aus F ableitbar.
Barbara König Logik 117
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel mit otter
Wir wollen zeigen, dass
((AK∨BK )∧(AK → BK )∧(BK∧RL→ ¬AK )∧RL)→ (¬AK∧BK )
gültig ist. Das ist genau dann der Fall, wenn
(AK ∨BK )∧(¬AK ∨BK )∧(¬BK ∨¬RL∨¬AK )∧RL∧(AK ∨¬BK )
unerfüllbar ist. (Wegen: F → G gültig gdw. F ∧ ¬G unerfüllbar.)
Barbara König Logik 118
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel mit otter
Wir verwenden otter – einen Theorembeweiser basierend aufResolution.
otter – http://www.cs.unm.edu/˜mccune/otter/
Mit Hilfe von otter kann man Resolutionsbeweisedurchführen.otter ist eigentlich für die Prädikatenlogik gedacht, für dieAussagenlogik ist im allgemeinen ein aussagenlogischerSAT-Solver (wie limboole) angebracht.otter ist inzwischen zu prover9 weiterentwickelt worden, wirverwenden in der Vorlesung jedoch trotzdem otter, weil manin der Ausgabe sehr schön die Resolutionsbeweisenachvollziehen kann.
Barbara König Logik 119
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel mit otter
Eingabesyntax (Beispielformel)
set(prolog_style_variables).set(binary_res).clear(unit_deletion).clear(factor).list(sos).ak | bk. % (ak | bk) in limboole-Syntax-ak | bk. % (!ak | bk)-bk | -rl | -ak. % (!bk | !rl | !ak)rl. % rlak | -bk. % (ak | !bk)end_of_list.
Die Optionen zu Beginn stellen sicher, dass die in der Vorlesungeingeführte Art der Resolution verwendet wird.
Barbara König Logik 120
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel mit otter
Textuelle Ausgabe von otter---------------- PROOF ----------------1 [] ak|bk.2 [] -ak|bk.3 [] -bk| -rl| -ak.4 [] rl.5 [] ak| -bk.6 [binary,2.1,1.1] bk.7 [binary,5.2,6.1] ak.8 [binary,3.1,6.1] -rl| -ak.11 [binary,8.1,4.1] -ak.12 [binary,11.1,7.1] $F.------------ end of proof -------------
Barbara König Logik 121
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel mit otter
Ausgabe von otter – visuell mit GraphViz aufbereitet
Barbara König Logik 122
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel: Pigeonhole-Prinzip
Wir betrachten nun eine Formel, bei der viele Erfüllbarkeitstester(SAT-Solver) ein schlechtes Verhalten zeigen.
Pigeonhole-Prinzip/Dirichletsches Schubfachprinzip
Wenn N + 1 Tauben in N Schlägen sitzen, dann gibt es inmindestens einem Schlag zwei (oder mehr) Tauben.
Wir verwenden zur Formalisierung folgende atomare Formeln: Ti ,j
mit i ∈ {1, . . . ,N + 1}, j ∈ {1, . . . ,N}.A(Ti ,j) = 1 bedeutet dabei, dass die i-te Taube im j-tenSchlag sitzt.
Barbara König Logik 123
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel: Pigeonhole-Prinzip
Wir formalisieren zunächst: “N + 1 Tauben sitzen in N Schlägen”.Jede Taube sitzt in mindestens einem Schlag:
F1 =∧
i∈{1,...,N+1}
∨
j∈{1,...,N}Ti ,j
Keine Taube sitzt in zwei Schlägen:
F2 =∧
i∈{1,...,N+1}
∧
j1,j2∈{1,...,N}, j1 6=j2
(¬Ti ,j1 ∨ ¬Ti ,j2)
In einem Schlag sitzen (mindestens) zwei Tauben:
G =∨
i1,i2∈{1,...,N+1}, i1 6=i2
∨
j∈{1,...,N}(Ti1,j ∧ Ti2,j)
Barbara König Logik 124
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Beispiel: Pigeonhole-Prinzip
Der gesamte aussagenlogische Ausdruck lautet:
F1 ∧ F2 → G .
Er ist gültig genau dann, wenn F1 ∧ F2 ∧ ¬G unerfüllbar ist.Dabei ist F1∧F2∧¬G schon “beinahe” in konjunktiver Normalform.
Mit Hilfe eines Programms kann man Formeln für jedes N erzeugenund mit Hilfe von limboole überprüfen. Für diese Art von Formelnzeigt limboole ein relativ schlechtes Laufzeitverhalten, bereits abN = 20 dauert der Test sehr lange.
Barbara König Logik 125
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Sudoku
Beispiel: ein Sudoku-Solver, basierend auf Erfüllbarkeitstests
Sudoku-RegelnEin Sudoku-Feld ist ein Schach-brett mit 9 Zeilen und 9 Spalten.Es ist außerdem unterteilt in 9Regionen, bestehend aus 3 × 3Feldern.
Barbara König Logik 126
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Sudoku
Beispiel: ein Sudoku-Solver, basierend auf Erfüllbarkeitstests
Sudoku-RegelnZu Beginn sind einige dieser Fel-der mit Zahlen aus der Menge{1, . . . , 9} gefüllt.
5 3
6
9 8
7
1 9 5
6
3
1
6
5
97
82
2
3
6
8
8
4
7
6
4 1 9
8
Barbara König Logik 126
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Sudoku
Beispiel: ein Sudoku-Solver, basierend auf Erfüllbarkeitstests
Sudoku-RegelnDie Aufgabe besteht nun darin,das Feld vollständig auszufüllen,so dass in jeder Zeile, in jederSpalte und in jeder Region jedeZahl zwischen 1 und 9 genau ein-mal vorkommt.
5 3
6
9 8
7
1 9 5
6
3
1
6
5
97
82
2
3
6
8
8
4
7
6
4 1 9
8
4 6 8 9 1 2
7 2 3 4 8
1 3 4 2 5 7
5 9 7 1 4 2
2 6 5 7 9
1 3 9 4 8 5
9 1 5 3 7 4
2 8 7 6 3
3 4 5 2 6 1
Barbara König Logik 126
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Sudoku
Wir verwenden folgende atomare Formeln, um ein Sudoku zubeschreiben: Si ,j ,k mit i , j , k ∈ {1, . . . , 9}.
A(Si ,j ,k) = 1 bedeutet dabei, dass sich auf Feld (i , j) die Zahlk befindet.
Mit Hilfe dieser 9 · 9 · 9 = 729 atomaren Formeln lassen sich nun dieSudoku-Spielregeln mit Hilfe der Aussagenlogik formalisieren.
Barbara König Logik 127
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Sudoku
Auf jedem Feld befindet sich eine Zahl:∧
i ,j∈{1,...,9}
∨
k∈{1,...,9}Si ,j ,k
Auf keinem Feld befinden sich zwei Zahlen:∧
i ,j∈{1,...,9}
∧
k1,k2∈{1,...,9}, k1 6=k2
(¬Si ,j ,k1 ∨ ¬Si ,j ,k2)
In keiner Zeile, Spalte, Region kommt eine Zahl doppelt vor:für Zeile 1 lautet die Formel wie folgt
∧
j1,j2∈{1,...,9}, j1 6=j2
∧
k∈{1,...,9}(¬S1,j1,k ∨ ¬S1,j2,k)
(Für die restlichen Zeilen und für die Spalten und Regionenergeben sich analoge Formeln).
Barbara König Logik 128
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
Anwendung: Sudoku
Für die Erzeugung dieser Formel als limboole-Formel bietet es sichan, ein Programm zu schreiben, das die (sehr große) Formel in eineDatei schreibt. Die Datei besteht aus ca. 220.000 Zeichen.Anschließend muss nur noch die Situation in einem bestimmtenSudoku-Rätsel dargestellt werden, wie z.B. für das obige Beispiel:
S115 & S123 & S157 & S216 & S241 & S259 & S265 &S329 & S338 & S386 & S418 & S456 & S493 & S514 &S548 & S563 & S591 & S617 & S652 & S696 & S726 &S772 & S788 & S844 & S851 & S869 & S895 & S958 &S987 & S999
Die entstehende Formel ist erfüllbar und limboole gibt (trotz derGröße der Formel) ohne erkennbare Zeitverzögerung die Lösung aus.
Barbara König Logik 129
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
51 4
7 8 6
6 3 9
4 2 3
1 7
6 4 5
9 3 4
1 8 7
7 2 8
Barbara König Logik 130
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenResolution
1 2
3 8 5
9
4
75
1
5
2
4
1
9
7 3
Barbara König Logik 131
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Prädikatenlogik
Wir beschäftigen uns nun im folgenden mit der Prädikatenlogik, diegegenüber der Aussagenlogik folgendes erlaubt:
Man kann über ein beliebiges Universum (= Grundmenge) unddessen Elemente Aussagen machen.Man kann quantifizieren: “für alle x gilt . . . ”; “es gibt ein x , sodass . . . ”Es gibt mehrstellige Prädikatsymbole (interpretiert alsRelationen) und mehrstellige Funktionssymbole (interpretiertals Funktionen).
Der Aufbau dieses Kapitels ist ähnlich wie bei der Aussagenlogik:wir beginnen mit Grundbegriffen (Syntax, Semantik, Gültigkeit,Erfüllbarkeit), Äquivalenz und Normalformen, und beschäftigen unsdann mit der Resolution.
Barbara König Logik 132
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Syntax der Prädikatenlogik: Variablen, Terme
Definition (Syntax der Prädikatenlogik)
Eine Variable hat die Form xi mit i = 1, 2, 3 . . ..Ein Prädikatensymbol hat die Form Pk
i und einFunktionssymbol hat die Form f ki mit i = 1, 2, 3 . . . undk = 0, 1, 2 . . .. Hierbei heißt i jeweils der Unterscheidungsindexund k die Stelligkeit (oder Stellenzahl).Wir definieren nun die Terme durch einen induktiven Prozess:
1 Jede Variable ist ein Term.2 Falls f ein Funktionssymbol mit der Stelligkeit k ist, und
falls t1, . . . , tk Terme sind, so ist auch f (t1, . . . , tk) einTerm.
Barbara König Logik 133
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Syntax der Prädikatenlogik: Variablen, Terme
Bemerkungen zur Syntax der Prädikatenlogik:Es sind auch Funktionssymbole der Stelligkeit 0eingeschlossen, und in diesem Fall fallen die Klammern weg,d.h., statt c() schreiben wir nur c .Nullstellige Funktionssymbole heißen auchKonstanten(-symbole).Genauso gibt es nullstellige Prädikatsymbole der Form P()bzw. einfach nur P .
Barbara König Logik 134
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Syntax der Prädikatenlogik: Variablen, Terme
Weitere Bemerkungen:Für Variablen schreiben wir auch x , y , z , u, v ,w , . . .
Für Prädikatsymbole schreiben wir auch P,Q,R, S , . . . (dieStelligkeit ergibt sich dann aus dem Kontext).Für Funktionssymbole schreiben wir auch f , g , h, . . . (dieStelligkeit ergibt sich dann ebenfalls aus dem Kontext).Für Konstanten(-symbole) schreiben wir auch a, b, c , d , . . .
Barbara König Logik 135
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Syntax der Prädikatenlogik: Formeln
Nun können wir (wiederum induktiv) definieren, was Formeln (derPrädikatenlogik) sind.
1 Falls P ein Prädikatsymbol der Stelligkeit k ist, und fallst1, . . . , tk Terme sind, dann ist P(t1, . . . , tk) eine Formel.
2 Für jede Formel F ist auch ¬F eine Formel.3 Für alle Formeln F und G sind auch (F ∧ G ) und (F ∨ G )
Formeln.4 Falls x eine Variable ist und F eine Formel, so sind auch ∃xF
und ∀xF Formeln. Das Symbol ∃ wird Existenzquantor und ∀Allquantor genannt.
Barbara König Logik 136
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Syntax der Prädikatenlogik: Formeln
Bemerkungen:Atomare Formeln nennen wir genau diejenigen, die die FormP(t1, . . . , tn) haben (gemäß (1)). Falls F eine Formel ist undF als Teil einer Formel G auftritt, so heißt F Teilformel von G .Quantoren binden stärker als alle anderen Operatoren, d.h.,Formeln werden folgendermaßen geklammert:
∀xP(x) ∧ Q(y) entspricht (∀xP(x)) ∧ Q(y)
P(x) ∨ ∃yQ(y) ∨ R(z) entspricht P(x) ∨ (∃yQ(y)) ∨ R(z)
Barbara König Logik 137
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Freie und gebundene Variablen
Definition (Freie und gebundene Variable)
Alle Vorkommen von Variablen in einer Formel werden in freie undgebundene Vorkommen unterteilt. Dabei heißt ein Vorkommen derVariablen x in der Formel F gebunden, falls F eine Formel derForm ∃xG oder ∀xG enthält und x in G vorkommt. Andernfallsheißt dieses Vorkommen von x frei.
Eine Formel ohne Vorkommen einer freien Variablen heißtgeschlossen oder eine Aussage.
Barbara König Logik 138
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Freie und gebundene Variablen
Beispiele für freie und gebundene Variable:∀xP(x): in dieser Formel kommt x gebunden vor.∀xQ(x , y): in dieser Formel kommt x gebunden und y frei vor.(∀xP(x)) ∧ R(x): in dieser Formel hat x sowohl eingebundenes als auch ein freies Vorkommen.∀x((∀xP(x)) ∧ R(x)): in dieser Formel ist das ersteVorkommen von x unter dem inneren und das zweiteVorkommen unter dem äußeren Quantor gebunden.
Definition (Matrix)
Die Matrix einer Formel F ist diejenige Formel, die man aus Ferhält, indem jedes Vorkommen von ∃ bzw. ∀, samt derdahinterstehenden Variablen gestrichen wird. Symbolischbezeichnen wir die Matrix der Formel F mit F ∗.
Barbara König Logik 139
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zur Prädikatenlogik
NF: Keine Formel F: Formel, aber nicht Aussage A: Aussage
NF F A∀∃P(x)∀xP(a)∀x∃y(Q(x , y) ∨ R(x , y))
∀xQ(x , x)→ ∃xQ(x , y)
∀xP(x) ∨ ∀xQ(x , x)
∀P(x)P(x)→ ∃x
Barbara König Logik 140
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zur Prädikatenlogik
NF: Keine Formel F: Formel, aber nicht Aussage A: Aussage
NF F A∀x¬∀yQ(x , y) ∧ R(x , y)
∃z(Q(z , x) ∨ R(y , z))→ ∃y(R(x , y) ∧ Q(x , z))
∃x(¬P(x) ∨ P(a))
P(x)→ ∃xP(x)∃x∀y((P(y)→ Q(x , y)) ∨ ¬P(x))
Barbara König Logik 141
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Definition (Struktur)
Eine Struktur ist ein Paar A = (UA, IA), wobei UA eine beliebigeaber nicht-leere Menge ist, die die Grundmenge von A (oder derGrundbereich, der Individuenbereich, das Universum) genannt wird.Ferner ist IA eine Abbildung, die
jedem k-stelligen Prädikatensymbol P (im Definitionsbereichvon IA) eine k-stellige Relation über UA zuordnet,jedem k-stelligen Funktionssymbol f (im Definitionsbereichvon IA) eine k-stellige Funktion auf UA zuordnet,jeder Variablen x (im Definitionsbereich von IA) ein Elementder Grundmenge UA zuordnet.
Barbara König Logik 142
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Bemerkungen zu Strukturen:Eine Struktur ist das analoge Konzept zu Belegungen in derAussagenlogik.Die den Funktionssymbolen zugeordneten Funktionen könnenfolgendermaßen dargestellt werden: sei f ein n-stelligesFunktionssymbol, dann schreiben wir f A = IA(f ) mit
f A : UnA → UA
(a1, . . . , an) 7→ f A(a1, . . . , an),
beispielsweise die einstellige Nachfolgerfunktion auf dennatürlichen Zahlen (UA = N0 = {0, 1, 2, 3, 4, . . . }):
f A : N0 → N0
n 7→ n + 1
Barbara König Logik 143
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Die den Prädikatsymbolen zugeordneten Relationen könnenfolgendermaßen dargestellt werden: sei P ein n-stelligesPrädikatsymbol, dann schreiben wir PA = IA(P) mit
PA ⊆ UnA = UA × · · · × UA︸ ︷︷ ︸
n-mal
PA = {(a1, . . . , an) | a1, . . . , an ∈ UA und . . . }
beispielsweise die zweistellige ≤-Relation auf den natürlichenZahlen:
PA ⊆ N0 × N0
PA = {(n,m) | n,m ∈ N0 und n ≤ m}
Barbara König Logik 144
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Definition (Passende Struktur)
Sei F eine Formel und A = (UA, IA) eine Struktur. A heißt zu Fpassend, falls IA für alle in F vorkommenden Prädikatsymbole,Funktionssymbole und freien Variablen definiert ist.
Der Definitionsbereich der Abbildung IA ist also eineTeilmenge von {Pk
i , fki , xi | i = 1, 2, 3, . . . und k = 0, 1, 2, . . .}
(in der alle Prädikatsymbole, Funktionssymbole und freienVariablen von F enthalten sind) undder Wertebereich (bzw. Bildbereich) von IA ist die Menge allerRelationen und Funktionen auf UA, sowie der Elemente vonUA.
Wir schreiben abkürzend statt IA(P) einfach PA, statt IA(f )einfach f A und statt IA(x) einfach xA.
Barbara König Logik 145
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Definition (Wert eines Terms)
Sei F eine Formel und A eine zu F passende Struktur. Für jedenTerm t, den man aus den Bestandteilen von F bilden kann (alsoaus den freien Variablen und Funktionssymbolen), definieren wirnun den Wert von t in der Struktur A, den wir mit A(t)bezeichnen. Es gilt A(t) ∈ UA. Die Definition ist wieder induktiv.
1 Falls t eine Variable ist (also t = x), so ist A(t) = xA.
2 Falls t die Form t = f (t1, . . . , tk) hat, wobei t1, . . . , tk Termeund f ein k-stelliges Funktionssymbol ist, so istA(t) = f A(A(t1), . . . ,A(tk)).
Fall (2) schließt auch die Möglichkeit ein, dass f nullstellig ist, d.h.,t = a für eine Konstante a. In diesem Fall gilt A(t) = aA.
Barbara König Logik 146
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Auf analoge Weise definieren wir (induktiv) den (Wahrheits-)Werteiner Formel F unter der Struktur A, wobei wir ebenfalls dieBezeichnung A(F ) verwenden. Es gilt A(F ) ∈ {0, 1}.
Definition (Wahrheitswert einer Formel)
Falls F die Form F = P(t1, . . . , tk) hat mit den Terment1, . . . , tk und k-stelligem Prädikatsymbol P , so ist
A(F ) ={
1, falls (A(t1), . . . ,A(tk)) ∈ PA
0, sonst
Falls F die Form F = ¬G hat, so ist
A(F ) ={
1, falls A(G ) = 00, sonst
Barbara König Logik 147
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Falls F die Form F = (G ∧ H) hat, so ist
A(F ) ={
1, falls A(G ) = 1 und A(H) = 10, sonst
Falls F die Form F = (G ∨ H) hat, so ist
A(F ) ={
1, falls A(G ) = 1 oder A(H) = 10, sonst
Barbara König Logik 148
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semantik der Prädikatenlogik: Strukturen
Falls F die Form F = ∀xG hat, so ist
A(F ) ={
1, falls für alle d ∈ UA gilt: A[x/d ](G ) = 10, sonst
Falls F die Form F = ∃xG hat, so ist
A(F ) ={
1, falls es ein d ∈ UA gibt mit: A[x/d ](G ) = 10, sonst
Für d ∈ UA steht A[x/d ] für diejenige Struktur A′, die überall mitA identisch ist, bis auf die Definition von xA
′. Wir definieren
xA′= d , unabhängig davon, ob IA auf x definiert ist oder nicht.
Barbara König Logik 149
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Modell, Gültigkeit, Erfüllbarkeit
Definition (Modell)
Falls für eine Formel F und eine zu F passende Struktur A giltA(F ) = 1, so schreiben wir wieder A |= F . Sprechweise: F gilt inA oder A ist Modell für F .
Gültigkeit, Erfüllbarkeit, UnerfüllbarkeitFalls jede zu F passende Struktur ein Modell für F ist, so schreibenwir |= F , andernfalls 6|= F . Sprechweise: F ist (allgemein-)gültig.Falls es mindestens ein Modell für die Formel F gibt, so heißt Ferfüllbar, andernfalls unerfüllbar.
Barbara König Logik 150
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Erfüllbarkeit und Gültigkeit
Folgende Formeln sind erfüllbar, aber nicht gültig. Finden Siejeweils eine Struktur, die ein Modell für die Formel ist, und eineStruktur, die kein Modell für die Formel ist.
1 F = ∀xP(x)2 G = ∀x∃yQ(x , f (y))
Barbara König Logik 151
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Erfüllbarkeit und Gültigkeit
Modell A für F = ∀xP(x):
Universum UA = N0
PA = N0(das ist die einzige mögliche Interpretation von P , die zueinem Modell führt)
Struktur, die kein Modell für F = ∀xP(x) ist:
Universum UB = N0
PB = {n | n ∈ N0, n gerade}
Barbara König Logik 152
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Erfüllbarkeit und Gültigkeit
Modell A für G = ∀x∃yQ(x , f (y))
Universum UA = N0
QA = {(n,m) | n,m ∈ N0, n < m}f A : N0 → N0 mit f A(n) = n + 1
Struktur, die kein Modell für G = ∀x∃yQ(x , f (y)) ist:
Universum UB = N0
QB = {(n,m) | n,m ∈ N0, n < m}f B : N0 → N0 mit f B(n) = 1
Bemerkung: diese Strukturen sind natürlich keineswegs die einzigenBeispiele für Modelle bzw. Nicht-Modelle von F , G .
Barbara König Logik 153
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Erfüllbarkeit und Gültigkeit
G: Gültig E: Erfüllbar U: Unerfüllbar
G E U∀xP(a)∃x(¬P(x) ∨ P(a))
P(a)→ ∃xP(x)∀xP(x)→ ∃xP(x)∀xP(x) ∧ ¬∀yP(y)∀xP(x)→ ∀xP(f (x))
Barbara König Logik 154
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Prädikatenlogik mit Gleichheit
Bei Prädikatenlogik mit Gleichheit sind Formeln genauso aufgebaut,wie bei herkömmlicher Prädikatenlogik, mit dem Unterschied, dasses ein spezielles Prädikat = gibt, das in Infix-Notation verwendetwird. Das heißt, zur Definition der Syntax wird folgender Satzhinzugefügt:
Falls t1, t2 Terme sind, dann ist (t1 = t2) eine Formel.Außerdem steht (t1 6= t2) für ¬(t1 = t2).
Und die Definition des Wahrheitswert einer Formel wirdfolgendermaßen ergänzt:
Falls F die Form F = (t1 = t2) hat mit den Termen t1, t2, soist
A(F ) ={
1, falls A(t1) = A(t2)0, sonst
Barbara König Logik 155
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Erfüllbarkeit und Gültigkeit
G: Gültig E: Erfüllbar U: Unerfüllbar
G E U∃x∃y∃z(x 6= y ∧ y 6= z ∧ x 6= z)
∀x∀y(x = y → f (x) = f (y))
∀x∀y(f (x) = f (y)→ x = y)
∃x∃y∃z(f (x) = y ∧ f (x) = z ∧ y 6= z)
Barbara König Logik 156
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Tarski’s World
Tarski’s WorldTarski’s World ist eine Lehrsoftware für Prädikatenlogik,entworfen von Jon Barwise und John Etchemendy.Dabei werden die Formeln auf einem Schachbrett evaluiert, aufdem sich Tetraeder, Würfel und Dodekaeder in drei Größen(small, medium, large) befinden können.Gegenüber der allgemeinen Prädikatenlogik gibt es sowohlEinschränkungen an die Syntax von Formeln als auch an diezulässigen Strukturen.Ob eine Formel für eine bestimmte Welt gilt (oder nicht), kannin einem Spiel gegen den Rechner intuitiv veranschaulichtwerden.
Barbara König Logik 157
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Tarski’s World – Screenshot
Barbara König Logik 158
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Tarski’s World
Einschränkungen an die Syntax – zulässige Konstanten undPrädikatsymbole:
Zulässige Konstanten: a, b, c , d , e, f
Zulässige Prädikatsymbole (Auswahl):Einstellig:Tet,Cube,Dodec, Small ,Medium, LargeZweistellig:Smaller , Larger ,BackOf ,FrontOf , LeftOf ,RightOfDreistellig: Between
Neben den Konstanten kommen in den Formeln bei Tarski’s Worldkeine weiteren Funktionssymbole vor.
Variablen, aussagenlogische Operatoren und Quantoren könnenbeliebig benutzt werden. Außerdem ist das Prädikat Gleichheit (=)erlaubt.
Barbara König Logik 159
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Tarski’s World
Einschränkungen an die Semantik – zulässige Strukturen:Universen bestehen immer aus Mengen von Körpern auf demSchachbrett.Die Interpretation der Prädikatsymbole ist durch die Größe undArt der Körper und durch ihre Positionierung auf demSchachbrett festgelegt.Beispielsweise gilt:
Tet(a) bedeutet, dass a ein Tetraeder ist.Smaller(a, b) bedeutet, dass a kleiner als b ist.LeftOf (c , d) sagt aus, dass sich c links von d befindet.Between(a, b, c) sagt aus, dass sich a zwischen b und cbefindet.
Barbara König Logik 160
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Tarski’s World
Daraus folgt: Nicht jede Formel, die in jeder Tarski’s World gilt, isteine im prädikatenlogischen Sinne gültige Formel.
Beispiel: ∀x(Small(x) ∨Medium(x) ∨ Large(x))
Barbara König Logik 161
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Folgerung und Äquivalenz
Definition (Folgerung)
Eine Formel G heißt eine Folgerung der Formeln F1, . . . ,Fk falls fürjede Struktur, die sowohl zu F1, . . . ,Fk als auch zu G passend ist,gilt:
Wenn A Modell von {F1, . . . ,Fk} ist, dann ist A auchModell von G .
Wir schreiben F1, . . . ,Fk |= G , falls G eine Folgerung vonF1, . . . ,Fk ist.
Definition (Äquivalenz)
Zwei Formeln F , G heißen (semantisch) äquivalent, falls für alleStrukturen A, die sowohl für F als auch für G passend sind, giltA(F ) = A(G ). Hierfür schreiben wir F ≡ G .
Barbara König Logik 162
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Folgerung und Äquivalenz
1 F1 = ∀xP(x) ∨ ∀xQ(x)
2 F2 = ∀x(P(x) ∨ Q(x))
3 F3 = ∀xP(x) ∨ ∀yQ(y)
J NF1 |= F2
F2 |= F3
F3 |= F1
Barbara König Logik 163
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Folgerung und Äquivalenz
1 F1 = ∃y∀xP(x , y)2 F2 = ∀x∃yP(x , y)
J NF1 |= F2
F2 |= F1
Barbara König Logik 164
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe zu Folgerung und Äquivalenz
J N∀x∀yF ≡ ∀y∀xF∀x∃yF ≡ ∃x∀yF∀x∃yF ≡ ∃y∀xF∃x∃yF ≡ ∃y∃xF∀xF ∨ ∀xG ≡ ∀x(F ∨ G )
∀xF ∧ ∀xG ≡ ∀x(F ∧ G )
∃xF ∨ ∃xG ≡ ∃x(F ∨ G )
∃xF ∧ ∃xG ≡ ∃x(F ∧ G )
Barbara König Logik 165
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Äquivalenzen
Satz (Äquivalenz von prädikatenlogischen Formeln)
Seien F und G beliebige Formeln. Dann gilt:1 ¬∀xF ≡ ∃x¬F¬∃xF ≡ ∀x¬F
2 Falls x in G nicht frei vorkommt, gilt:∀xF ∧ G ≡ ∀x(F ∧ G )∀xF ∨ G ≡ ∀x(F ∨ G )∃xF ∧ G ≡ ∃x(F ∧ G )∃xF ∨ G ≡ ∃x(F ∨ G )
3 ∀xF ∧ ∀xG ≡ ∀x(F ∧ G )∃xF ∨ ∃xG ≡ ∃x(F ∨ G )
4 ∀x∀yF ≡ ∀y∀xF∃x∃yF ≡ ∃y∃xF
Barbara König Logik 166
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Äquivalenzen
Bemerkung: alle Äquivalenzgesetze der Aussagenlogik behaltenweiterhin ihre Gültigkeit.
Beispiel:
∀x¬(P(x) ∧ ¬P(x)) ≡ ∀x(¬P(x) ∨ P(x))
(nach deMorgan)
Barbara König Logik 167
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Substitution
Definition (Substitution)
Sei F eine Formel, x eine Variable und t ein Term. Dann bezeichnetF [x/t] diejenige Formel, die man aus F erhält, wenn man jedesfreie Vorkommen der Variablen x in F durch t ersetzt. Durch [x/t]wird eine Substitution beschrieben.
Dabei geht man davon aus, dass durch die Substitution keineVariable in t gebunden wird.
Beispiele für Substitutionen:(P(x) ∨ Q(f (x)) ∨ R(y)
)[x/g(y)] =
P(g(y)) ∨ Q(f (g(y))) ∨ R(y)(∀xP(x) ∨ Q(x)
)[x/g(y)] = ∀xP(x) ∨ Q(g(y))
Barbara König Logik 168
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Substitution
Unterscheidung zwischen F [x/t] und A[x/d ]:Bei F [x/t] wird eine syntaktische Ersetzung innerhalb derFormel F vorgenommen.Bei A[x/d ] wird eine Struktur verändert, d.h., diese Ersetzungbezieht sich auf die Semantik.
Der Zusammenhang zwischen beiden Notationen ist wie folgt:
ÜberführungslemmaFür jede Formel F , jede Variable x und jeden Term t, der keine inF gebundene Variable enthält, gilt:
A(F [x/t]) = A[x/A(t)](F ).
Barbara König Logik 169
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Bereinigte Formeln
Definition (Bereinigte Formel)
Eine Formel heißt bereinigt, sofern es keine Variable gibt, die in derFormel sowohl gebunden als auch frei vorkommt, und sofern hinterallen vorkommenden Quantoren verschiedene Variablen stehen.
Lemma (Gebundene Umbenennung)
Sei y eine Variable, die in F nicht vorkommt. Dann gilt:∃xF ≡ ∃y(F [x/y ])∀xF ≡ ∀y(F [x/y ])
LemmaZu jeder Formel F gibt es eine äquivalente Formel in bereinigterForm.
Barbara König Logik 170
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Pränexform
Definition (Pränexform)
Eine Formel heißt pränex oder in Pränexform, falls sie folgendeBauart hat
Q1y1Q2y2 . . .QnynF ,
wobei Qi ∈ {∃, ∀}, n ≥ 0, und die yi (paarweise verschiedene)Variablen sind. Es kommt ferner kein Quantor in F vor.
SatzFür jede Formel gibt es eine äquivalente (und bereinigte) Formel inPränexform.
Barbara König Logik 171
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Pränexform
Verfahren zur Bestimmung der Pränexform:
Gegeben: eine prädikatenlogische Formel F .
1 Erstelle durch gebundene Umbenennung eine bereinigteFormel, die zu F äquivalent ist.
2 Schieben alle Negationen mit Hilfe der Gesetze ¬∀xF ≡ ∃x¬Fund ¬∃xF ≡ ∀x¬F hinter die Quantoren.
3 Ziehe alle Quantoren nach vorne unter Verwendung folgenderGesetze (Annahme: x kommt nicht frei in G vor):
(∀xF ∧ G ) ≡ ∀x(F ∧ G ) (∀xF ∨ G ) ≡ ∀x(F ∨ G )
(∃xF ∧ G ) ≡ ∃x(F ∧ G ) (∃xF ∨ G ) ≡ ∃x(F ∨ G )
(Für diese Umformung ist es unbedingt notwendig, dass Fzuvor bereinigt wurde.)
Barbara König Logik 172
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Pränexform
Beispiel: Formen Sie die folgende Formel in Pränexform um.
F = (∀x∃y P(x , g(y , f (x))) ∨ ¬Q(z)) ∨ ¬∀x R(x , y)
Barbara König Logik 173
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Skolemform
Wir definieren nun noch die Skolemform, in der keineExistenzquantoren mehr enthalten sind.
Definition (Skolemform)
Eine Formel ist in Skolemform, falls sie folgende Bauart hat
∀y1∀y2 . . . ∀ynF ,
wobei n ≥ 0, und die yi (paarweise verschiedene) Variablen sind. Eskommt ferner kein Quantor in F vor.
Barbara König Logik 174
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Skolemform
Für jede Formel F in bereinigter Pränexform (BPF) definieren wirihre Skolemform(-el) als das Resultat der Anwendung des folgendenAlgorithmus auf F :
while F enthält einen Existenzquantor dobegin
F habe die Form F = ∀y1∀y2 . . . ∀yn∃z G für eineFormel G in BPF und n ≥ 0 (der Allquantorblock kannauch leer sein);
Sei f ein neues bisher in F nicht vorkommendesn-stelliges Funktionssymbol;
F := ∀y1∀y2 . . . ∀ynG [z/f (y1, y2, . . . , yn)];(der Existenzquantor in F wird entfernt und jedesVorkommen von z in G durch f (y1, y2, . . . , yn) ersetzt)
end
Barbara König Logik 175
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Skolemform
SatzFür jede Formel F in bereinigter Pränexform gilt: F ist erfüllbargenau dann, wenn die Skolemform von F erfüllbar ist.
Bemerkung: die Umformung in die Skolemform erhält nur dieErfüllbarkeit von Formeln, nicht jedoch deren Gültigkeit! Man sagtdaher, dass die Formel F und ihre Skolemformerfüllbarkeitsäquivalent sind. Sie sind im allgemeinen jedoch nichtäquivalent.
Barbara König Logik 176
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Skolemform
Beispiel 1: Formen Sie folgende Formel in Skolemform um.
F = ∃x∀y∃z∀u∃vP(x , y , z , u, v)
Barbara König Logik 177
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Skolemform
Beispiel 2: Gegeben sei die Formel
F = ∀x∃y P(x , y)
Bestimmen Sie zunächst die Skolemform F ′ von F .Geben Sie ein Modell von F an und erweitern Sie es zu einemModell von F ′.
Barbara König Logik 178
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Klauselform
Definition (Klauselform)
Eine Aussage heißt in Klauselform, falls sie die Bauart hat
∀y1∀y2 . . . ∀yn F ,
wobei F keine Quantoren enthält und in KNF (konjunktiverNormalform) ist.
Eine Aussage in Klauselform kann als Menge von Klauselndargestellt werden.
Beispiel: ∀x∀y((P(x , y) ∨ Q(x)) ∧ R(y)) ist in Klauselform undwird dargestellt als:
{{P(x , y),Q(x)}, {R(y)}}
Barbara König Logik 179
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Klauselform
Verfahren zur Bestimmung der Klauselform:
Gegeben: eine prädikatenlogische Formel F (mit eventuellenVorkommen von freien Variablen).
1 Bereinige F durch systematisches Umbenennen dergebundenen Variablen. Es entsteht eine zu F äquivalenteFormel F1.
2 Seien y1, y2, . . . , yn die in F bzw. F1 vorkommenden freienVariablen. Ersetze F1 durch F2 = ∃y1∃y2 . . . ∃ynF1. Dann istF2 erfüllbarkeitsäquivalent zu F1 und F und enthält keinefreien Variablen mehr.
3 Stelle eine zu F2 äquivalente (und damit zu Ferfüllbarkeitsäquivalente) Aussage F3 in Pränexform her.
Barbara König Logik 180
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Klauselform
4 Eliminiere die vorkommenden Existenzquantoren durchÜbergang zur Skolemform von F3. Diese sei F4 und ist dannerfüllbarkeitsäquivalent zu F3 und damit auch zu F .
5 Forme die Matrix von F4 um in KNF, wodurch man dieKlauselform erhält (und schreibe diese Formel F5 dann alsKlauselmenge auf).
Barbara König Logik 181
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Klauselform
Welche dieser Formel sind bereinigt, in Pränexform, in Skolemform,in Klauselform?
B P S K∀x(Tet(x) ∨ Cube(x) ∨ Dodec(x))∃x∃y(Cube(y) ∨ BackOf(x , y))∀x(¬FrontOf(x , x) ∧ ¬BackOf(x , x))¬∃xCube(x) ↔ ∀x¬Cube(x)∀x(Cube(x) → Small(x)) → ∀y(¬Cube(y) → ¬Small(y))(Cube(a) ∧ ∀xSmall(x)) → Small(a)∃x(Larger(a, x) ∧ Larger(x , b)) → Larger(a, b)
Barbara König Logik 182
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Klauselform
Beispiel: Formen Sie die folgenden Formeln in Klauselform um:
F1 = ∀xP(x)→ ∀xP(f (x))F2 = (∀x∃y P(x , g(y , f (x))) ∨ ∀z¬Q(z)) ∧ ¬∀x R(x , x)
Barbara König Logik 183
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Universum
Motivation: Um die Erfüllbarkeit/Unerfüllbarkeit einerprädikatenlogischen Formel zu testen, müsste man ungeheuer vieleStrukturen durchprobieren.
Wir zeigen im folgenden, dass es reicht nur ganz bestimmteStrukturen, sogenannte Herbrand-Strukturen—benannt nach demLogiker Jacques Herbrand—zu testen.Diese können immer noch ein unendlich großes Universum habenund unendlich viele sein, sind aber dennoch wesentlichüberschaubarer.Darauf aufbauend kann dann ein automatisches Verfahrenentwickelt werden, das mit Hilfe von Resolution die Unerfüllbarkeiteiner prädikatenlogischen Formel überprüft.
Barbara König Logik 184
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Universum
Definition (Herbrand-Universum)
Das Herbrand-Universum D(F ) einer geschlossenen Formel F inSkolemform ist die Menge aller variablenfreie Terme, die aus denBestandteilen von F gebildet werden können. Falls in F keineKonstante vorkommt, wählen wir zunächst eine beliebige Konstante,zum Beispiel a, und bilden dann die variablenfreien Terme.
D(F ) wird wie folgt induktiv definiert:1 Alle in F vorkommenden Konstanten sind in D(F ). Falls F
keine Konstante enthält, so ist a in D(F ).2 Für jedes in F vorkommende n-stellige Funktionssymbol f und
Terme t1, . . . , tn in D(F ) ist der Term f (t1, . . . , tn) in D(F ).
Barbara König Logik 185
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Universum
Beispiel: Bestimmen Sie die Herbrand-Universen zu folgendenFormeln
F1 = ∀x P(f (x), g(a))F2 = ∀x∀y Q(h(x , y))
F3 = ∀x P(x)
Barbara König Logik 186
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Strukturen
Definition (Herbrand-Struktur)
Sei F eine Aussage in Skolemform. Dann heißt jede zu F passendeStruktur A = (UA, IA) eine Herbrand-Struktur für F , fallsfolgendes gilt:
1 UA = D(F ),2 für jedes in F vorkommende n-stellige Funktionssymbol f und
t1, t2, . . . , tn ∈ D(F ) ist f A(t1, t2, . . . , tn) = f (t1, t2, . . . , tn).
Idee: Jeder variablenfreie Term t wird “durch sich selbst”interpretiert, d.h., A(t) = t. (Vermischung von Syntax undSemantik.)
Barbara König Logik 187
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Strukturen
Für eine Herbrand-Struktur A vereinfacht sich dasÜberführungslemma:
Lemma (Überführungslemma für Herbrand-Strukturen)
Sei A eine Herbrand-Struktur. Dann gilt für jede Formel F , jedeVariable x und jeden variablenfreien Term t:
A(F [x/t]) = A[x/t](F ).
Barbara König Logik 188
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Der fundamentale Satz der Prädikatenlogik
SatzSei F eine Aussage in Skolemform. F ist genau dann erfüllbar,wenn F ein Herbrand-Modell besitzt.
Idee: Man muss zeigen, dass eine erfüllbare Aussage F inSkolemform ein Herbrand-Modell besitzt.Da F erfüllbar ist, hat F ein (beliebiges) Modell A. Um einHerbrand-Modell B für F zu erhalten, werden die Prädikatsymbolewie folgt interpretiert: für ein n-stelliges Prädikatsymbol P undt1, . . . , tn ∈ D(F ) gilt
(t1, . . . , tn) ∈ PB genau dann, wenn (A(t1), . . . ,A(tn)) ∈ PA.
(Wenn eine Konstante a ∈ D(F ) nicht in F vorkommt, dann wähltman eine beliebige Interpretation aA.)
Barbara König Logik 189
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Der fundamentale Satz der Prädikatenlogik
Beispiel zum vorherigen Satz: Gegeben sei die Formel
F = ∀x P(x , f (x))
Aufgaben:Bestimmen Sie ein beliebiges Modell A von F .Anschließend definieren Sie ein Herbrand-Modell B von F ,dessen Relation PB analog zu PA definiert ist. (So wie imBeweis zum vorherigen Satz beschrieben.)
Barbara König Logik 190
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Expansion
Definition (Herbrand-Expansion)
Sei F = ∀y1∀y2 . . . ∀ynF ∗ eine Aussage in Skolemform. Dann istE (F ), die Herbrand-Expansion von F , definiert als
E (F ) = {F ∗[y1/t1][y2/t2] . . . [yn/tn] | t1, t2, . . . , tn ∈ D(F )}
Die Formeln in E (F ) entstehen also, indem die Terme in D(F ),dem Herbrand-Universum von F , in jeder möglichen Weise für dieVariablen in F ∗ substituiert werden.
Bemerkung: Da das Herbrand-Universum D(F ) abzählbar ist, istauch die Menge E (F ) abzählbar.
Barbara König Logik 191
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Expansion
Wiederholung: Abzählbarkeit
Definition (Abzählbarkeit)
Eine Menge M heißt abzählbar, wenn es eine surjektive Abbildungf : N0 → M gibt. Das heißt es gibt eine (nicht notwendigerweisekonstruktive) Aufzählung f (0), f (1), f (2), . . . aller Elemente vonM, in der jedes Element von M mindestens einmal vorkommt.
Bemerkungen:Beispiele für abzählbare Mengen sind N0, Q (die Menge derrationalen Zahlen bzw. Brüche) und die Menge aller Terme,die aus einer endlichen Menge von Funktionssymbolen gebildetwerden. (Daher: ein Herbrand-Universum D(F ) ist immerabzählbar.)Die Menge R der reellen Zahlen ist nicht abzählbar.
Barbara König Logik 192
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Expansion
Beispiel: Bestimme die Herbrand-Expansion der Formel
∀x∀y P(x , y , f (y)).
Barbara König Logik 193
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Herbrand-Expansion
Idee: Behandle die Formeln in der Herbrand-Expansion wieaussagenlogische Formeln. D.h., betrachte jedes auftauchendePrädikat P(t1, . . . , tn) wie eine atomare Formel A.
Beispiel:E (F ) = {F1,F2, . . . }.
Sei beispielsweise
F1 = (P(f (a), f (b))︸ ︷︷ ︸A
∨Q(g(a, b))︸ ︷︷ ︸B
∨P(a, b)︸ ︷︷ ︸C
) ∧ P(f (a), f (b))︸ ︷︷ ︸A
.
Dies entspricht (A ∨ B ∨ C ) ∧ A.
Eine Formel in der Herbrand-Expansion ist erfüllbar, genau dann,wenn sie im aussagenlogischen Sinne erfüllbar ist.
Barbara König Logik 194
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Satz von Gödel-Herbrand-Skolem
Satz (Gödel-Herbrand-Skolem)
Für jede Aussage F in Skolemform gilt: F ist erfüllbar genau dann,wenn die Formelmenge E (F ) (im aussagenlogischen Sinn) erfüllbarist.
Beweis: Es genügt zu zeigen, dass F ein Herbrand-Modell besitztgenau dann, wenn E (F ) erfüllbar ist.Die Formel F habe die Form ∀y1∀y2 . . . ∀ynF ∗. Mit Hilfe desÜberführungslemmas kann man zeigen:
Barbara König Logik 195
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Satz von Gödel-Herbrand-Skolem
A ist ein Herbrand-Modell für Fgdw. für alle t1, t2, . . . , tn ∈ D(F ) gilt:
A[y1/t1][y2/t2]...[yn/tn](F∗) = 1
gdw. für alle t1, t2, . . . , tn ∈ D(F ) gilt:
A(F ∗[y1/t1][y2/t2] . . . [yn/tn]) = 1
gdw. für alle G ∈ E (F ) gilt A(G ) = 1gdw. A ist ein Modell für E (F )
Barbara König Logik 196
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Satz von Herbrand
Satz (Herbrand)
Eine Aussage F in Skolemform ist unerfüllbar genau dann, wenn eseine endliche Teilmenge von E (F ) gibt, die (im aussagenlogischenSinn) unerfüllbar ist.
Beweis: Ummittelbare Folge des Satzes von Gödel-Herbrand-Skolemund des Endlichkeitssatzes. Endlichkeitssatz
Barbara König Logik 197
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Algorithmus von Gilmore
Sei F eine prädikatenlogische Aussage in Skolemform und sei{F1,F2,F3, . . . } eine Aufzählung von E (F ).
Algorithmus von GilmoreEingabe: F
n := 0;repeatn := n + 1;until (F1 ∧ F2 ∧ . . . ∧ Fn) ist unerfüllbar;Gib “unerfüllbar” aus und stoppe.
Barbara König Logik 198
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Algorithmus von Gilmore
Bemerkungen zum Algorithmus von Gilmore:Man wählt eine beliebige unendliche Aufzählung F1,F2,F3, . . .aller Formeln in E (F ).Dabei muss nur darauf geachtet werden, dass jede Formelirgendwann in dieser Aufzählung vorkommt. Das ist möglich,da E (F ) abzählbar ist.Es dürfen Formeln mehrfach vorkommen. Das ist insbesondereimmer dann so, wenn E (F ) endlich ist.Wenn alle Formeln in einer endlichen Menge E (F ) abgearbeitetsind und noch nicht “unerfüllbar” ausgegeben wurde, dannkann der Algorithmus auch stoppen und “erfüllbar” ausgeben.
Barbara König Logik 199
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Algorithmus von Gilmore
Beispiel: Zeigen Sie mit Hilfe des Algorithmus von Gilmore, dassfolgende Formeln
F = ∀x (P(f (x)) ∧ ¬P(x))G = ∀x∀y (¬P(f (f (x))) ∧ P(f (y)))
unerfüllbar sind.
Barbara König Logik 200
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Algorithmus von Gilmore
Aus dem Satz von Herbrand folgt:Falls die Formel F unerfüllbar ist, so stoppt der Algorithmusvon Gilmore nach endlicher Zeit und gibt unerfüllbar aus.Falls der Algorithmus von Gilmore unerfüllbar ausgibt, so ist Ftatsächlich unerfüllbar.
Wenn F jedoch erfüllbar ist, so gibt es keine Garantie dafür, dassder Algorithmus jemals terminiert.
Es kann auch gezeigt werden, dass es tatsächlich keinenAlgorithmus gibt, der das Unerfüllbarkeitsproblem derPrädikatenlogik löst und immer mit der korrekten Antwort(unerfüllbar bzw. erfüllbar) terminiert.
Barbara König Logik 201
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Algorithmus von Gilmore
Semi-Entscheidbarkeit (informell)
Sei M ⊆ X eine Menge (auch Sprache oder Problem genannt). DieMenge M heißt semi-entscheidbar, wenn es einen Algorithmus Agibt, der
ein Element x ∈ X als Eingabe nimmt undgenau dann, wenn x ∈ M gilt, terminiert und “x ist in Menthalten” zurückgibt.
Der Algorithmus A muss jedoch nicht terminieren, wenn x 6∈ Mgilt. Falls A auch in diesem Fall terminiert und “x ist nicht in Menthalten” zurückgibt, so heißt M entscheidbar.
Bemerkung: die Begriffe Entscheidbarkeit undSemi-Entscheidbarkeit werden detailliert in der Vorlesung“Berechenbarkeit und Komplexität” besprochen.
Barbara König Logik 202
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semi-Entscheidbarkeitssätze
Satz (Semi-Entscheidbarkeit)
Folgende Probleme sind semi-entscheidbar, jedoch nichtentscheidbar:(a) Das Unerfüllbarkeitsproblem für prädikatenlogische Formeln.(b) Das Gültigkeitsproblem für prädikatenlogische Formeln.(c) Das Folgerungsproblem für prädikatenlogische Formeln.(d) Das Äquivalenzproblem für prädikatenlogische Formeln.
Barbara König Logik 203
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Semi-Entscheidbarkeitssätze
Beweis:(a) Das Problem ist nicht entscheidbar (ohne Beweis). Der
Algorithmus von Gilmore kann es jedoch “semi-entscheiden”.(b) F gültig gdw. ¬F unerfüllbar.(c) F |= G gdw. F → G gültig.(d) F ≡ G gdw. F ↔ G gültig.
Barbara König Logik 204
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Resolution in der Prädikatenlogik
Der Algorithmus von Gilmore funktioniert zwar, ist in der Praxisaber unbrauchbar, weil er zuviele Formeln erzeugt und nichtzielgerichtet arbeitet.
Daher ist unser Programm der nächsten Stunden:
Wie sieht Resolution in der Prädikatenlogik aus?
Barbara König Logik 205
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Wiederholung: Resolution in der Aussagenlogik
Resolutionsschritt:
{L1, . . . , Ln,A} {L′1, . . . , L′m,¬A}
{L1, . . . , Ln, L′1, . . . , L
′m}
Mini-Beispiel:
{¬A,B} {A} {¬B}
{B}
�
Eine Klauselmenge ist unerfüllbar genau dann, wenn durchResolution die leere Klausel abgeleitet werden kann.
Barbara König Logik 206
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Anpassung des Algorithmus von Gilmore
Algorithmus von Gilmore:Sei F eine prädikatenlogische Aussage in Skolemform und sei{F1,F2,F3, . . .} eine Aufzählung von E (F ).
Eingabe: F
n := 0;repeat n := n + 1;until (F1 ∧ F2 ∧ . . . ∧ Fn) ist unerfüllbar;
(dies kann mit Mitteln der Aussagenlogik,beispielsweise Wahrheitstafeln, getestet werden)
Gib “unerfüllbar” aus und stoppe.
“Mittel der Aussagenlogik” wir verwenden Resolution für denUnerfüllbarkeitstest
Barbara König Logik 207
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Definition von Res(M) (Wiederholung)
DefinitionSei M eine Klauselmenge. Dann ist Res(M) definiert als
Res(M) = M ∪ {R | R ist Resolvent zweier Klauseln in M}.
Außerdem setzen wir:
Res0(M) = M
Resn+1(M) = Res(Resn(M)) für n ≥ 0
und schließlich sei
Res∗(M) =⋃
n≥0
Resn(M).
Barbara König Logik 208
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Grundresolutionsalgorithmus
Sei F1,F2, . . . weiterhin die Aufzählung der Herbrand-Expansion.
Grundresolutionsalgorithmus
Eingabe: eine Aussage F in Klauselform
i := 0;M := ∅;repeat
i := i + 1; M := M ∪ Fi ; M := Res∗(M)until � ∈ M
Gib “unerfüllbar” aus und stoppe.
Warum der Name Grundresolution? Im Gegensatz zu späterenVerfahren werden Terme ohne Variable (= Grundterme)substituiert, um die Formeln der Herbrand-Expansion zu erhalten.
Barbara König Logik 209
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Grundresolutionssatz
Aus dem Grundresolutionsalgorithmus ergibt sich folgender Satz:
GrundresolutionssatzEine Aussage in Klauselform F = ∀y1 . . . ∀ykF ∗ mit der Matrix F ∗
in KNF ist unerfüllbar genau dann, wenn es eine Folge vonKlauseln K1, . . . ,Kn gibt mit der Eigenschaft:
Kn ist die leere KlauselFür i = 1, . . . , n gilt:
entweder ist Ki eine Grundinstanz einer Klausel K ∈ F ∗,d.h. Ki = K [y1/t1] . . . [yk/tk ] mit ti ∈ D(F )oder Ki ist (aussagenlogischer) Resolvent zweierGrundinstanzen Ka,Kb mit a < i und b < i
Weglassen von Klauseln und Resolutionsschritten, die nicht zurHerleitung der leeren Klausel beitragen.
Barbara König Logik 210
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Grundresolutionsalgorithmus
Beispiel: Zeigen Sie mit Hilfe von Grundresolution, dass folgendeFormel in Klauselform unerfüllbar ist.
{{P(f (x)),Q(x)}, {¬P(f (g(y)))}, {¬Q(g(f (a)))}}
Barbara König Logik 211
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Prädikatenlogische Resolution
Bei der Grundresolution kann man unnötigerweise in Sackgassenlaufen.
Beispiel:
{P(f (x)),Q(x)}
[x/g(a)]
{¬P(f (g(y)))}[y/a]
{¬Q(g(f (a)))}
{Q(g(a))}
?
Besser wäre gewesen, die Variable x durch g(f (a)) anstatt durchg(a) zu ersetzen. Aber woher kann man das vorher wissen?
Barbara König Logik 212
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Prädikatenlogische Resolution
Idee: Variablen nur noch so weit “wie nötig” durch Terme ersetzen.Statt Grundtermen Terme mit Variablen verwenden.
{P(f (x)),Q(x)}
[x/g(y)]
{¬P(f (g(y)))}[]
{¬Q(g(f (a)))}
[]{Q(g(y))}
[y/f (a)]
�
Barbara König Logik 213
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Wiederholung: Substitutionen
Eine Substitution sub ist eine Abbildung von Variablen auf Terme.F sub: Anwendung der Substitution sub auf die Formel Ft sub: Anwendung der Substitution sub auf den Term t
Eine Substitution kann auch als Folge von Ersetzungen beschriebenwerden:
[x/f (z)] [y/g(a, z)] [z/h(w)]
entspricht folgender entflochtener Substitution:
[x/f (h(w)), y/g(a, h(w)), z/h(w)].
Ersetzungen werden von links nach rechts durchgeführt!
Verknüpfung von Substitutionen: sub1sub2 (zuerst wird sub1angewandt, anschließend sub2).
Barbara König Logik 214
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Unifikator/Allgemeinster Unifikator
Definition (Unifikation)
Gegeben sei eine Menge L = {L1, . . . , Lk} von Literalen. EineSubstitution sub heißt Unifikator von L, falls
L1sub = L2sub = · · · = Lksub
Das ist gleichbedeutend mit |Lsub| = 1, wobeiLsub = {L1sub, . . . , Lksub}.
Ein Unifikator sub von L heißt allgemeinster Unifikator von L, fallsfür jeden Unifikator sub′ von L gilt, dass es eine Substitution s gibtmit sub′ = sub s.
Barbara König Logik 215
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Unifikator/Allgemeinster Unifikator
Beispiele: Bestimmen Sie die allgemeinsten Unifikatoren folgenderMengen (falls sie existieren):
{P(x),P(f (y))}{P(x),Q(y)}{Q(x , f (x)),Q(y , g(y))}{P(x),P(f (x))}{Q(x , f (y)),Q(g(z), f (x))}{Q(x , f (y)),Q(g(y), f (x))}{Q(x , f (y)),Q(f (y), z),Q(z , f (x))}
Barbara König Logik 216
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Unifikator/Allgemeinster Unifikator
Bemerkungen:Eine Menge von Literalen kann mehrere allgemeinsteUnifikatoren haben.Beispielsweise sind sowohl [y/f (x)] als auch [x/z ][y/f (z)]allgemeinste Unifikatoren von {P(f (x)),P(y)}.Alle allgemeinsten Unifikatoren kann man jedoch durcheinfache Variablenumbenennung ineinander umformen.Eine Menge L von (mehr als zwei) Literalen kann unterUmständen nicht unifizierbar sein, auch wenn alle Paare vonLiteralen unifizierbar sind.Beispiel: {Q(x , f (y)),Q(f (y), z),Q(z , f (x))}
Barbara König Logik 217
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Unifikationsalgorithmus
Unifikationsalgorithmus
Eingabe: eine Literalmenge L 6= ∅sub := []; (leere Substitution)while |Lsub| > 1 do
Suche die erste Position, an der sich zwei Literale L1, L2aus Lsub unterscheidenif keines der beiden Zeichen ist eine Variablethen stoppe mit “nicht unifizierbar”else Sei x die Variable und t der Term im anderen Literal
(möglicherweise auch eine Variable)if x kommt in t vorthen stoppe mit “nicht unifizierbar”else sub := sub [x/t]
Ausgabe: subBarbara König Logik 218
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Unifikationsalgorithmus
Beispiel: Wende den Unifikationsalgorithmus auf folgendeLiteralmenge an
L = {¬P(f (z , g(a, y)), h(z)),¬P(f (f (u, v),w), h(f (a, b)))}
Bemerkung: hier sind a, b Konstanten und y , z , u, v ,w Variablen
Barbara König Logik 219
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Korrektheit des Unifikationsalgorithmus
Satz (Korrektheit des Unifikationsalgorithmus)
Der Unifikationsalgorithmus terminiert immer und gibt beiEingabe einer nicht-unifizierbaren Literalmenge “nichtunifizierbar” aus.Wenn eine Menge L von Literalen unifizierbar ist, dann findetder Unifikationsalgorithmus immer den allgemeinstenUnifikator von L.
Das bedeutet unter anderem auch, dass jede unifizierbare Mengevon Literalen einen allgemeinsten Unifikator hat (Unifikationssatzvon Robinson).
Barbara König Logik 220
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Prädikatenlogische Resolution
Definition (Prädikatenlogischer Resolvent)
Eine Klausel R heißt prädikatenlogischer Resolvent zweier KlauselnK1,K2, wenn folgendes gilt:
Es gibt Substitutionen s1, s2, die Variablenumbenennungensind, so dass K1s1 und K2s2 keine gemeinsamen Variablenenthalten.Es gibt Literale L1, . . . , Lm aus K1s1 und Literale L′1, . . . , L
′n
aus K2s2, so dass L = {L1, . . . , Ln, L′1, . . . , L
′n} unifizierbar ist.
Sei sub der allgemeinste Unifikator von L.(L bezeichnet das negierte Literal L.)Es giltR = ((K1s1 − {L1, . . . , Lm}) ∪ (K2s2 − {L′1, . . . , L′n}))sub.
Barbara König Logik 221
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Prädikatenlogische Resolution
Schreibweise:Zu resolvierende Literale unterstreichen undSubstitutionen angeben
Beispiel: Klauseln {P(x),P(f (y)),Q(x , y)}, {¬P(f (g(x)))}
{P(x),P(f (y)),Q(x , y)}s1 = []
sub = [x/f (g(z)), y/g(z)]
{¬P(f (g(x)))}
s2=[x/z]
{Q(f (g(z)), g(z))}
Hinweis: Es gibt noch zwei weitere Möglichkeiten, einenprädikatenlogischen Resolutionsschritt mit diesen Klauselnauszuführen.
Barbara König Logik 222
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Aufgabe
Sind diese Klauseln resolvierbar?Wieviele mögliche Resolventen gibt es?
K1 K2 Möglichkeiten{P(x),Q(x , y)} {¬P(f (x))}{Q(g(x)),R(f (x))} {¬Q(f (x))}{P(x),P(f (x))} {¬P(y),Q(y , z)}
Barbara König Logik 223
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Prädikatenlogische Resolution
Beispiel: Leiten Sie aus folgender Klauselmenge die leere Klauselher (diesmal mit prädikatenlogischer Resolution anstattGrundresolution).
{{P(f (x)),Q(x)}, {¬P(f (g(y)))}, {¬Q(g(f (a)))}}
Barbara König Logik 224
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Korrektheit und Vollständigkeit
Zwei Fragen:Wenn man mit prädikatenlogischer Resolution aus einer FormelF die leere Klausel � ableiten kann, ist F dann unerfüllbar?(Korrektheit)Kann man für eine unerfüllbare Formel F immer durchprädikatenlogische Resolution die leere Klausel herleiten?(Vollständigkeit)
Obiges ist zwar bereits für die Grundresolution bekannt, aber nochnicht für die prädikatenlogische Resolution.
Barbara König Logik 225
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Lifting-Lemma
Lifting-Lemma
Seien K1,K2 zweiprädikatenlogische Klauseln undseien K ′1,K
′2 zwei Grundinstanzen
hiervon, die aussagenlogischresolvierbar sind und denResolventen R ′ ergeben.Dann gibt es einenprädikatenlogischen Resolventen Rvon K1,K2, so dass R ′ eineGrundinstanz von R ist.
K1
��
K2
��
K ′1 R
��
K ′2
R ′
—: Resolution→: Substitution
Barbara König Logik 226
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiel zum Lifting-Lemma
{P(f (x)),Q(x)}[x/g(a)]��
{¬P(f (g(y)))}[y/a]��
{P(f (g(a))),Q(g(a))} {Q(g(y))}[y/a]��
{¬P(f (g(a)))}
{Q(g(a))}
Barbara König Logik 227
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Resolutionssatz
Resolutionssatz der PrädikatenlogikSei F eine Aussage in Skolemform mit einer Matrix F ∗ in KNF.Dann gilt: F ist unerfüllbar genau dann, wenn � ∈ Res∗(F ∗).(Dabei bezeichnet Res die Bildung aller möglichenprädikatenlogischen Resolventen.)
Für den Beweis des Resolutionssatzes benötigen wir noch denBegriff des Allabschlusses . . .
Barbara König Logik 228
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Resolutionssatz
Für eine Formel H mit freien Variablen x1, . . . , xn bezeichnen wirmit
∀H = ∀x1∀x2 . . . ∀xnHihren Allabschluss.
Sei F eine Aussage in Skolemform und sei F ∗ deren Matrix inKNF, so gilt:
F ≡ ∀F ∗ ≡∧
K∈F∗∀K
Beispiel:
F ∗ = P(x , y) ∧ ¬Q(y , x)
F ≡ ∀x∀y(P(x , y) ∧ ¬Q(y , x)) ≡ ∀x∀yP(x , y) ∧ ∀x∀y(¬Q(y , x))
Barbara König Logik 229
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Resolutionssatz
Beweisskizze (Resolutionssatz):Korrektheit: Falls R ein Resolvent von Klauseln K1,K2 ist,dann kann man zeigen, dass ∀K1 ∧ ∀K2 |= ∀R .Die weitere Argumentation ist analog zur Aussagenlogik: wenndie leere Klausel (eine unerfüllbare Formel) aus F folgt, dannist F selbst unerfüllbar.Vollständigkeit: Wenn F unerfüllbar ist, dann gibt es einenGrundresolutionsbeweis, bei dem die leere Klausel abgeleitetwird. Mit Hilfe des Lifting-Lemmas kann dieser Beweis alsprädikatenlogischer Resolutionsbeweis “nachgebaut” werden,wobei ebenfalls die leere Klausel entsteht.
Barbara König Logik 230
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Verfeinerung der Resolution (Ausblick)
Probleme bei der prädikatenlogischen Resolution:Zu viele WahlmöglichkeitenImmer noch zu viele SackgassenKombinatorische Explosion des Suchraums
Lösungsansätze:Strategien und Heuristiken: Verbieten bestimmterResolutionsschritte, Suchraum wird dadurch eingeschränkt
Vorsicht: Die Vollständigkeit darf dadurch nicht verloren gehen!
Barbara König Logik 231
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele
Ist die Klauselmenge
{{P(f (x))}, {¬P(f (x)),Q(f (x), x)}, {¬Q(f (a), f (f (a)))},{¬P(x),Q(x , f (x))}}
unerfüllbar?
Barbara König Logik 232
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele
Wir betrachten folgende Klauselmenge (Beispiel aus dem Buch vonSchöning):
F = {{¬P(x),Q(x),R(x , f (x))}, {¬P(x),Q(x),S(f (x))}, {T (a)},{P(a)}, {¬R(a, x),T (x)}, {¬T (x),¬Q(x)}, {¬T (x),¬S(x)}}
und zeigen ihre Unerfüllbarkeit mit Hilfe desResolutionstheorembeweisers otter (siehe auch die Vorstellung vonotter im Kapitel “Aussagenlogik”).
Barbara König Logik 233
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele
Wir betrachten folgende prädikatenlogische Formel:
F = ∀x(P(x)→ P(f (x)))
Ist diese Formel gültig, erfüllbar oder unerfüllbar?Was passiert, wenn sie als Eingabe für einenResolutionstheorembeweiser (wie beispielsweise otter)verwendet wird?
Diese Formel ist erfüllbar: otter leitet immer neue Klauseln abund terminiert nicht.
Barbara König Logik 234
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele
Das Affe-Banane-Problem (Teil 1)
(A1) Ein Tier, das Arme hat und nahe bei einem Ding ist,kann das Ding erreichen.
(A2) Ein Tier auf einem hohen Gegenstand, der unter denBananen steht, ist nahe bei den Bananen.
(A3) Wenn ein Tier in einem Raum einen Gegenstand zueinem Ding schiebt, die beide im Raum sind, dann istdas Ding nahe am Boden oder der Gegenstand istunter dem Ding.
(A4) Wenn ein Tier einen Gegenstand ersteigt, ist es aufdem Gegenstand.
(A5) Der Affe ist ein Tier, das Arme hat.
Barbara König Logik 235
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele
Das Affe-Banane-Problem (Teil 2)
(A6) Der Stuhl ist ein hoher Gegenstand.(A7) Die Bananen sind ein Ding.(A8) Der Affe, die Bananen und der Stuhl sind im Raum.(A9) Der Affe kann den Stuhl unter die Bananen schieben.(A10) Die Bananen sind nicht nahe am Boden.(A11) Der Affe kann den Stuhl ersteigen.(S?) Kann der Affe die Bananen erreichen?
Barbara König Logik 236
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele
Schema für die Lösung solcher Probleme:Seien A1, . . . ,An die Axiome oder Voraussetzungen undS die Schlussfolgerung.Um zu zeigen, dass
A1 ∧ · · · ∧ An → S
gültig ist, zeigen wir, dass
A1 ∧ · · · ∧ An ∧ ¬S
unerfüllbar ist.
Barbara König Logik 237
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Anwendungen
Anwendungen der prädikatenlogischen ResolutionTheorembeweiser: Beweis von Sätzen aus der MathematikVerifikation: Beweis der Korrektheit von ProgrammenSchlussfolgerung in ExpertensystemenPlanungssystemeLogik-Programmierung (PROLOG) siehe nächstes Kapitel
Bemerkung: Neben Resolution gibt es noch weitere Methoden, dieUnerfüllbarkeit prädikatenlogischer Formeln zu zeigen,beispielsweise mit Hilfe von Tableau-Beweisen.
Barbara König Logik 238
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Logik-Programmierung
Wir betrachten sogenannte Hornklauseln, bei denen höchstens einLiteral positiv ist (analog zu den aussagenlogischen Hornformeln).
Das führt zu einfacheren Resolutionsbeweisen, die im wesentlichendie Form von Ketten haben. Die dabei entstehenden Substitutionenkann man aufsammeln und als Lösung präsentieren.
Auf dieser Idee basieren Logik-Programmiersprachen, wiebeispielsweise PROLOG.
Barbara König Logik 239
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Logik-Programmierung
Beispiel: wir betrachten folgende Formalisierung der Addition
F = ∀x A(x , null , x) ∧∀x∀y∀z (A(x , y , z)→ A(x , s(y), s(z)))
Dabei ist A ein dreistelliges Prädikatsymbol mit der Bedeutung:A(x , y , z) genau dann, wenn x + y = z .
Außerdem ist s eine einstellige Funktion, die dieNachfolgerfunktion (successor function) darstellen soll. Einenatürliche Zahl n soll so dargestellt werden:
sn(null) = s(s(. . . (s(︸ ︷︷ ︸n mal
null)) . . . ))
Des weiteren soll die Konstante null die 0 repräsentieren.Barbara König Logik 240
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Logik-Programmierung
Wir wollen nun überprüfen, ob die Formel
G = ∃u A(s(s(s(null))), s(s(null)), u)
aus dieser Formel folgt. D.h., gibt es ein u für das gilt 3+ 2 = u?
Wir negieren und skolemisieren die Formel F → G und erhaltenfolgende Klauselmenge:
{{A(x , null , x)}, {¬A(x , y , z),A(x , s(y), s(z))},{¬A(s(s(s(null))), s(s(null)), u)}}
Dabei heißt die aus G entstandene Klausel Zielklausel.
Barbara König Logik 241
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Logik-Programmierung
Bemerkungen:Bei der Resolution dieser Klauseln reicht es aus, immer mitmindestens einer Klausel zu resolvieren, die nur aus negativenLiteralen besteht. Wir beginnen die Resolution also mit derZielklausel.Dabei entstehen als Resolventen wiederum nur Klauseln, dienur aus negativen Literalen bestehen.
Barbara König Logik 242
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Logik-Programmierung
{¬A(s(s(s(null))), s(s(null)), u)}
s1=[]
{¬A(x , y , z),A(x , s(y), s(z))}s2 = []
sub1 = [u/s(z), x/s(s(s(null))), y/s(null)]
{¬A(s(s(s(null))), s(null), z)}
s1=[]
{¬A(x , y , z),A(x , s(y), s(z))}s2 = [z/z ′]
sub2 = [z/s(z ′), x/s(s(s(null))), y/null ]
{¬A(s(s(s(null))), null , z ′)}
s1=[]
{A(x , null , x)}s2 = []
sub3 = [z ′/s(s(s(null))), x/s(s(s(null)))]
�
Barbara König Logik 243
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Motivation: Logik-Programmierung
Wir sammeln alle Substitutionen auf, wenden sie auf u an underhalten:
u sub1 sub2 sub3 = s(z) sub2 sub3
= s(s(z ′)) sub3
= s(s(s(s(s(null)))))
Das heißt, die leere Klausel kann abgeleitet werden, wenn man udurch s5(null) ersetzt. Das ist aber genau das Ergebnis derAddition 3+ 2.
Diesen Prozess nennt man auch Antwortgenerierung.
Barbara König Logik 244
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Hornklauseln
Definition (Hornklauselprogramm, Teil 1)
Ein Hornklauselprogramm oder Logikprogramm ist eineKlauselmenge, in der jede Klausel höchstens ein positives Literalenthält. Die Klauseln werden folgendermaßen klassifiziert:Tatsachenklauseln: Klauseln der Form {P} mit einem positiven
Literal P .PROLOG-Schreibweise: P.
Prozedurklauseln: Klauseln der Form {P,¬Q1, . . . ,¬Qk}, dieFolgerungen darstellen.PROLOG-Schreibweise: P :−Q1, . . . ,Qk (:− stehtfür ←)
Barbara König Logik 245
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Hornklauseln
Definition (Hornklauselprogramm, Teil 2)
Tatsachen- und Prozedurklauseln nennt man auchProgrammklauseln. Sie stellen das eigentliche Logikprogramm dar.
Logikprogramme werden aufgerufen durch sogenannte Zielklauseln:Zielklausel: eine Klausel der Form {¬Q1, . . . ,¬Qk}, entspricht
dem negierten BerechnungszielPROLOG-Schreibweise: ?− Q1, . . . ,Qk
Barbara König Logik 246
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
SLD-Resolution
Folgende Form der Resolution funktioniert speziell für Hornklauseln:
Definition (SLD-Resolution)
Eine SLD-Resolutionsherleitungder leeren Klausel hat die rechtsabgebildete Form, wobei G dieZielklausel ist, G1,G2, . . . nur ausnegativen Literalen bestehen undK1, . . . ,Kn Programmklauselnsind.
G K1
G1 K2
G2
... Kn
�
Die Abkürzung SLD steht für “ linear resolution with selectionfunction for definite clauses”
Barbara König Logik 247
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
SLD-Resolution
Satz (Vollständigkeit der SLD-Resolution)
Sei F mit Zielklausel G ein unerfüllbares Hornklauselprogramm.Dann gibt es für F eine SLD-Resolutionsherleitung der leerenKlausel.
Barbara König Logik 248
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Deklarative Programmiersprache PROLOG
Die Idee der Ermittlung eines Rechenergebnisses führt zur Definitioneiner Programmiersprache basierend auf Hornklauselprogrammen:PROLOG (entwickelt Anfang der siebziger Jahre).
Dabei beschreiben die Programmklauseln das eigentlich Programmund die Zielklausel die zu bearbeitenden Anfrage.
PROLOG ist, genau wie funktionale Programmiersprachen, einedeklarative Programmiersprache. Das heißt, es wird nicht so sehrbeschrieben, wie etwas berechnet wird, sondern was berechnetwerden soll.
Barbara König Logik 249
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Deklarative Programmiersprache PROLOG
ImperativZustandsorientiert: Zustand eines Programms besteht ausProgrammzähler und Belegung der Variablen (+ Stack, Heap)Programm besteht aus Befehlen, die diesen Zustand transformieren.Sprachen: FORTRAN, ALGOL, Pascal, Ada, C, Java
DeklarativBeschreibung einer Lösung durch Bedingungen, ohne genau zuspezifizieren, wie diese Lösung berechnet werden soll.Sprachen: Logik-Programmiersprachen: PROLOG;funktionale Sprachen: ML, OCaml, Haskell, Scheme, Lisp
Barbara König Logik 250
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Deklarative Programmiersprache PROLOG
Beispiel: Hausbau
Hausbau (imperativ): Hebe zunächst den Keller aus. Baue danneine Süd-, Ost-, West- und Nordwand. Setzeanschließend ein Dach auf die Wände.
Hausbau (deklarativ): Ein Haus besteht aus einem Keller, der vonvier Wänden umgeben ist, auf denen sich das Dachbefindet.
Barbara König Logik 251
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Deklarative Programmiersprache PROLOG
Syntax von PROLOG:Variablen werden mit Grossbuchstaben geschrieben:X, Y, Z, . . .Prädikat- und Funktionssymbole werden mit Kleinbuchstabendargestellt.Außerdem werden Programm- und Zielklauseln wie obenbeschrieben notiert.
Barbara König Logik 252
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Deklarative Programmiersprache PROLOG
PROLOG-Interpreter: wir verwenden GNU Prolog(http://www.gprolog.org/)
Wichtige Kommandos:
Aufruf> gprolog
Datei laden (z.B. eltern.pl)
| ?- [eltern].compiling eltern.pl for byte code...eltern.pl compiled, 36 lines read -
3874 bytes written, 11 ms
(1 ms) yes
Barbara König Logik 253
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Deklarative Programmiersprache PROLOG
Zielklausel eingeben| ?- onkel(X,christine).
X = boris ?
Mit ; werden weitere Antwortsubstitutionen gesucht.
Barbara König Logik 254
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
Beispiel: VerwandtschaftsbeziehungenNehmen Sie an, dass Verwandtschaftsbeziehungen wie “x istMutter von y ” und “x ist Vater von y ” definiert sind.Außerdem ist von jeder Person bekannt, ob sie männlich oderweiblich ist.Geben Sie Programmklauseln an, die abgeleiteteVerwandtschaftsbeziehungen wie “Elter”, “Grossmutter”,“Grossvater”, “Geschwister”, “Onkel” und “Tante” herleitenkönnen.
Barbara König Logik 255
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
Verwandtschaftsbeziehungenelter(X,Y) :- vater(X,Y).elter(X,Y) :- mutter(X,Y).
grossmutter(X,Y) :- mutter(X,Z),elter(Z,Y).grossvater(X,Y) :- vater(X,Z),elter(Z,Y).
geschwister(X,Y) :- elter(Z,X),elter(Z,Y),X\==Y.
onkel(X,Y) :- elter(Z,Y),geschwister(Z,X),maennlich(X).
tante(X,Y) :- elter(Z,Y),geschwister(Z,X),weiblich(X).
Barbara König Logik 256
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
Dadurch, dass PROLOG-Programme nicht aus konkretenHandlungsanweisungen bestehen, können ganz verschiedene Artenvon Anfragen an das gleiche Programm gestellt werden.Beispiel Addition:
add(X,null,X).add(X,s(Y),s(Z)) :- add(X,Y,Z).
?- add(s(s(s(null))),s(s(null)),X).X = s(s(s(s(s(null))))) ? ;
?- add(s(s(s(null))),Y,s(s(s(s(s(null)))))).Y = s(s(null)) ?
Bei der zweiten Anfrage wird eine Subtraktion durchgeführt.Barbara König Logik 257
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
PROLOG ist eine echte Programmiersprache, die auch Datentypenwie Zahlen, Listen, Strings, etc. beinhaltet. Wir sehen uns nun auchdiese Datentypen in Beispielprogrammen an.
Barbara König Logik 258
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
PROLOG beinhaltet vordefinierte Prädikate zur Manipulation vonListen. Damit können – ähnlich wie bei funktionalenProgrammiersprachen – rekursiv Operationen auf Listen definiertwerden.
Beispiele: Element hinten an eine Liste anhängen (attach) undListe umkehren (rev)
Listenverarbeitungattach([],Y,[Y]).attach([X | L],Y,[X | L1]) :- attach(L,Y,L1).
rev([],[]).rev([X | L],L1) :- rev(L,L2),attach(L2,X,L1).
Barbara König Logik 259
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
Wie bereits vorher angedeutet, kann man die definiertenOperatoren in “verschiedenen Richtungen” anwenden. Das istanders als bei den meisten anderen Programmiersprachen.
?- attach([a,b,c],d,Z).Z = [a,b,c,d]
?- attach([a,b,c],Y,[a,b,c,d]).Y = d
?- attach(X,d,[a,b,c,d]).X = [a,b,c]
Barbara König Logik 260
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
?- rev([a,b,c,d],Y).Y = [d,c,b,a]
?- rev(X,[a,b,c,d]).X = [d,c,b,a]
Barbara König Logik 261
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Beispiele für PROLOG-Programme
Alle Palindrome finden?- rev(X,X).X = []X = [_]X = [A,A]X = [A,_,A]X = [A,B,B,A]X = [A,B,_,B,A]...
Barbara König Logik 262
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Es gibt noch viele weitere Logiken, neben der Aussagenlogik undder Prädikatenlogik 1. Stufe.
Prädikatenlogik 2. Stufe
Quantifikation über Mengen (einstellige Prädikate) und Relationen(mehrstellige Prädikate) wird erlaubt.
Barbara König Logik 263
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Beispiel: Das Induktionsaxiom für die natürlichen Zahlen N0 ist nurin Prädikatenlogik 2. Stufe ausdrückbar:
Für jede Menge M von natürlichen Zahlen gilt: wenn M die 0enthält und für jede in M enthaltene Zahl n auch deren Nachfolgern + 1 in M enthalten ist, dann sind bereits alle natürlichen Zahlenin M enthalten.
∀M(0 ∈ M ∧ ∀n(n ∈ M → n + 1 ∈ M)→ ∀n(n ∈ M)
)
Barbara König Logik 264
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Weitere Bemerkungen zur Prädikatenlogik 2. Stufe:Das Unerfüllbarkeits- bzw. Gültigkeitsproblem für Logikenhöherer Stufe (insbesondere für die Prädikatenlogik 2. Stufe),ist nicht mehr semi-entscheidbar.Daraus folgt auch, dass solche Logiken höherer Stufe keinenKalkül (wie den Resolutionskalkül) haben können. Denn auseinem Kalkül, der es ermöglicht, alle wahren Formelnabzuleiten, kann man immer ein Semi-Entscheidungsverfahrengewinnen.Dennoch gibt es sogenannte Theorembeweiser (z.B. Isabelle,Coq), die die Erstellung von Beweisen in Logiken höherer Stufeunterstützen und teilweise automatisieren.
Barbara König Logik 265
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Die Nicht-Existenz eines solchen (vollständigen) Kalküls für dieArithmetik ist die Aussage des (Ersten) GödelschenUnvollständigkeitssatzes (1931). Für die Mathematik bedeutetdas: “Es gibt wahre Aussagen, die nicht beweisbar sind.”
Unterhaltsame Lektüre zu diesem Thema:Douglas R. Hofstadter: Gödel, Escher, Bach: An EternalGolden BraidIn deutscher Übersetzung: Douglas R. Hofstadter: Gödel,Escher, Bach: Ein endloses geflochtenes Band
Barbara König Logik 266
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
ModallogikenAnnahme, dass es mehrere mögliche Welten gibt. In manchendieser Welten können Aussagen wahr sein, in anderen nicht.
Beispiele für Aussagen der Modallogik:“Möglicherweise regnet es.”“Notwendigerweise sind alle Kreise rund.”
Barbara König Logik 267
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Für die Informatik besonders wichtig ist eine bestimmteModallogik, die sogennante Temporallogik:
TemporallogikHier werden die möglichen Welten als Momente im Ablauf der Zeitinterpretiert. Das heißt, man kann Aussagen über zeitliche Abfolgenmachen.
Beispiele für Aussagen der Temporallogik:“Irgendwann geschieht A.”“Das Ereignis B tritt unendlich oft ein.”
Die am häufigsten benutzten Temporallogiken sind: CTL(Computation Tree Logic), LTL (Linear Time Logic), modalerµ-Kalkül
Barbara König Logik 268
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Dreiwertige LogikenEnhalten neben den Wahrheitswerten 0, 1 auch den Wahrheitswert12 (= vielleicht).
Einsatz: in der Programmanalyse. Bei Approximation eines Systemdurch ein einfacheres System kann manchmal nicht mit Sicherheitgesagt werden, ob bestimmte Systemübergänge möglich oder nichtmöglich sind. Diesen wird dann der Wahrheitswert 1
2 zugeordnet.Auch für das Ergebnis einer Programmanalyse kann gelten:geforderte Eigenschaft gilt (1), gilt nicht (0) oder gilt vielleicht (1
2).
Barbara König Logik 269
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Die klassische Logik ist in folgendem Sinne monoton: wenn zu einerMenge von Axiomen ein weiteres hinzukommt, dann kann manimmer noch mindestens die gleichen Aussagen ableiten.
Monotonie: Aus F |= H folgt immer auch F ∧ G |= H.
Barbara König Logik 270
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Nicht-monotone LogikBei nicht-monotone Logiken kann diese Bedingung verletzt sein,d.h., durch zusätzliches Wissen kann eine Folgerung ungültigwerden.
Beispiel:Wir wissen, dass Tweety ein Vogel ist. Dann kann man darausfolgern, dass Tweety fliegen kann.Zusätzlich erfahren wir nun, dass Tweety ein Pinguin ist. Dannkann man diese Folgerung nicht mehr aufrechterhalten.
Einsatz: in Expertensystemen
Barbara König Logik 271
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Fuzzy LogicApproximiertes Schließen, eine Aussage kann nur zu einem gewissenProzentsatz “wahr” sein.
Einsatz: Haushaltsgeräte, Fehlerkorrektur
Barbara König Logik 272
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Intuitionistische LogikGrob: nur das, was man konstruieren kann, existiert.Widerspruchsbeweise sind nicht erlaubt.
Insbesondere: P ∨ ¬P (Satz vom ausgeschlossenen Dritten) istnicht automatisch eine gültige Formel.
Bemerkung: Dadurch wird die Logik zunächst schwächer undweniger Aussagen sind beweisbar. Die Forderung derKonstruierbarkeit kann aber für die Herleitung vonBerechnungsvorschriften verwendet werden.
Barbara König Logik 273
AussagenlogikPrädikatenlogik
Grundbegriffe, Äquivalenz und NormalformenHerbrandtheorie und ResolutionGrundlagen der Logik-Programmierung und Ausblick
Ausblick
Zuletzt noch eine Zusammenfassung der weiteren Anwendungen derLogik in der Informatik:
Modellierung und Spezifikation: Eindeutige Beschreibung vonkomplexen SystemenVerifikation: Beweisen, dass ein Programm das gewünschteVerhalten zeigtSchaltkreisentwurf: Schaltkreise lassen sich als logischeFormeln darstellen Entwurf und Optimierung von SchaltungenDatenbanken: Formulierung von Anfragen an Datenbanken Abfragesprache SQL (Structured query language)Künstliche Intelligenz: Schlussfolgerungen automatisieren,insbesondere in Expertensystemen
Barbara König Logik 274