| Lines 7 - 12 |
Lines 7 - 22 |
| Prädikatenlogik PL1 - Signaturen |
Prädikatenlogik PL1 - Signaturen |
| |
|
| PL1: Prädikaten Logik, 1. Stufe |
PL1: Prädikaten Logik, 1. Stufe |
| |
|
| |
|
| |
Die Grenzen der Aussagenlogik: |
| |
|
| |
* Hasen haben lange Ohren |
| |
* Max ist ein Hase |
| |
___________________ |
| |
Max hat lange Ohren |
| |
|
| |
Abbildung ist in der Aussagen Logik nicht möglich! Eigentlich: ALLE Hasen haben lange Ohren. Reichert man diese Aussagen um eine "innere Struktur" an, landet man bei der PraedikatenLogik. |
| |
|
| |
|
| +++ SIGMA=(Func, Pred) |
+++ SIGMA=(Func, Pred) |
| Lines 19 - 24 |
Lines 29 - 38 |
| |
|
| mit Stelligkeit 0: Konstanten |
mit Stelligkeit 0: Konstanten |
| mit Stelligkeit 1 und höher: Zum Aufbau von Termen |
mit Stelligkeit 1 und höher: Zum Aufbau von Termen |
| |
|
| |
In Prolog wird die Stelligkeit immer angegeben, h/2 != h/3 ! |
| |
|
| |
Das Unterscheidungsmerkmal Stelligkeit ist keine gute Idee. Zweimal der gleiche Funktionsname mit unterschiedlicher Stelligkeit und unterschiedlicher Funktion ist eine potentielle Fehlerquelle! |
| |
|
| |
|
| ++++ Beispiele |
++++ Beispiele |
| Lines 44 - 46 |
Lines 58 - 309 |
| * mortal(Socrates), flight(RF75, Dortmund, Berlin) |
* mortal(Socrates), flight(RF75, Dortmund, Berlin) |
| * grandfather(father_of(father_of(John)), John) |
* grandfather(father_of(father_of(John)), John) |
| |
|
| |
|
| |
+++ Prädikatenlogik: PL1-Signaturen |
| |
|
| |
PL1 Prädikatensymbole: |
| |
* mit Stelligkeit 0, 1, 2, ... |
| |
* zum Aufbau //atomarer Formeln//. |
| |
|
| |
Beispiele: |
| |
* prime(3) |
| |
* blue(sky) |
| |
* mortal(Sokrates) |
| |
* flight (RF75, Dortmund, Berlin) |
| |
* grandfather(father_of(father_of(John)), John) |
| |
|
| |
+++ Interpretation |
| |
|
| |
Interpretieren die Symbole SIGMA durch |
| |
* Objekte |
| |
* Eigenschaften |
| |
* Funktionen |
| |
* Relationen |
| |
* Fakten |
| |
|
| |
Das Universum U besteht aus: |
| |
|
| |
* F (- Func | (F): U x .... x U -> U |
| |
* P (- Prod | (P) teilmenge_von U x .... x U |
| |
|
| |
Domain (=Universum) ist //nie// leer! |
| |
|
| |
++++ Funktionssymbol mit Stelligkeit 0: |
| |
Element in U |
| |
|
| |
++++ Funktionssymbol mit Stelligkeit >= 1: |
| |
Funktion über U |
| |
|
| |
++++ Prädikatensymbol mit Stelligkeit 0: |
| |
Wahrheitswert |
| |
|
| |
++++ Prädikatensymbol mit Stelligkeit 1 |
| |
Teilmenge von U |
| |
|
| |
|
| |
++++ Beispiel |
| |
|
| |
[blue] [Menge aller blauen Elemente in U] |
| |
|
| |
++++ Prädikatensymbol mit Stelligkeit >1 |
| |
|
| |
Relation über U |
| |
|
| |
++++ Beispiel |
| |
|
| |
[brother] { ( Charles, Edward), ( Charles, Andrew) , (Edward, Andrew) } teilmenge_von U x U |
| |
|
| |
|
| |
+++ Terme |
| |
|
| |
V = Menge von Variablen |
| |
|
| |
Terme: rekursiv / induktiv definiert |
| |
|
| |
(1) x, falls x (- V |
| |
|
| |
* jede Variable ist ein Term |
| |
|
| |
(2) c, falls c (- Func und c hat Stelligkeit 0 |
| |
|
| |
* jede Konstante ist kein Term |
| |
|
| |
(3) f(t1, ..., tn) falls f (- Func mit Stelligkeit n>0 und t1, ..., tn Terme |
| |
|
| |
* Induktionsschritt. |
| |
|
| |
|
| |
+++ Variablenbelegung |
| |
|
| |
alpha: V -> U |
| |
|
| |
2 Parameter: |
| |
* Signatur |
| |
* Variablenmenge (Wert aus Domain, Interpretationsfrage) |
| |
|
| |
|
| |
+++ Termausweitung |
| |
|
| |
Termauswertung eines Terms t in einer Interpretation I unter einer Variablenbelegung: |
| |
|
| |
|[t]|_{ I,alpha } (- U |
| |
|
| |
ist definiert durch |
| |
|
| |
|[x]|_{ I, alpha } = alpha(x) |
| |
|
| |
|[f(t1, ..., tn) ]|_{ I, alpha } = f_I(|[t_1]|_t{I, alpha}, ..., |[t_n]|_{ I, alpha } |
| |
|
| |
Interpretation stark von Termdefinition abhängig! |
| |
|
| |
Für die Terme, Interpretation udn endlichen Term //terminiert// diese Auswertung (später mehr)! |
| |
|
| |
Gilt für allgemeine Formeln nicht (im Wesentlichen wegen alpha). |
| |
|
| |
I und alpha richtig wählen ist Herausforderung, der Rest ist sehr einfach. |
| |
|
| |
* atomare Formeln P(t1, ..., tn) |
| |
* komplexere Forlemn mit Junkoren (NOT, AND, OR, =>, <=>) |
| |
* quantifizierte Formeln mit Quantoren und Variablen. |
| |
|
| |
|
| |
FORALL xF "Für alle x gilt F" (Allquantor) |
| |
EXISTS xF "Es gibt ein x, sodass F gilt" (Existenz-Quantor) |
| |
|
| |
|
| |
* FORALL x Mensch (x) => sterblich (x) |
| |
* NOT NOT sterblich (Sokrates) .... Doppelnegationselimination |
| |
* EXISTS x Großvater (x, Sokrates) |
| |
* FORALL x Großvater(Vater_von((Mutter_von(x)), x) |
| |
* NOT prim (3) |
| |
* FORALL x EXISTS y prim(y) AND x < y .... Für jede Zahl x gibt es eine größere Primzahl. |
| |
|
| |
Somit gibt es unendlich viele Primzahlen. Prim ist hier als intendierte Semantik über natürliche Zahlen definiert. |
| |
|
| |
|
| |
+++ Erfüllungsrelation |
| |
|
| |
|[ P(t1, ..., tn ) ]| _ { I, alpha } = true gdw. |
| |
( |[t_1]|_{ I, alpha } .... |[ t_n ]| _ { I, alpha } ) (- P_I |
| |
|
| |
|[ FORALL x F ]| _ { I, alpha } = true gdw |[ F ]| _ {I, alpha}_{ x / alpha } = true für jedes alpha (- U |
| |
|
| |
|[ EXISTS x F ]| _ { I, alpha } = true gdw |[ F ]| _ {I, alpha}_{x / alpha } = true für mindestens ein alpha (- U |
| |
|
| |
Terminiert bei unentscheidlicher Domain möglicherweise nicht! (Unentscheidbarkeit der Prädikatenlogik). |
| |
|
| |
|
| |
+++ Semantische Äquivalenzen |
| |
|
| |
++++ "!DeMorgan für Quantoren" |
| |
|
| |
1.1 NOT FORALL x F equiv EXISTS x NOT F |
| |
1.2 NOT EXISTS x F equiv FORALL x NOT F |
| |
|
| |
|
| |
2.1 ( FORALL x F) AND ( FORALL x G ) equiv FORALL x ( F AND G ) |
| |
2.2 ( EXISTS x F) OR ( EXISTS x G ) equiv EXISTS x ( F OR G) |
| |
|
| |
|
| |
++++ Vertauschen gleicher Quantoren |
| |
|
| |
3.1 FORALL x FORALL y F equiv FORALL y FORALL x F |
| |
3.2 EXISTS x EXISTS y F equiv EXISTS y EXISTS x F |
| |
|
| |
|
| |
+++ Semantische Nicht-Äquivalenzen |
| |
|
| |
(hier war Prof. Egly zu schnell für mich...) |
| |
|
| |
+++ Delphin im Karpfenteich |
| |
|
| |
Delphin / Fisch / Teichbaden, usw. Dieses Beispiel haben wir ausgelassen. |
| |
|
| |
+++ Inferenz Beispiele |
| |
|
| |
Hasen haben lange Ohren |
| |
Max ist ein Hase |
| |
_________________ |
| |
? Max hat lange Ohren |
| |
|
| |
|
| |
FORALL x Hase(x) => hat_lange_Ohren(x) |
| |
Hase (Max) |
| |
_________________ |
| |
: ? |
| |
_________________ |
| |
hat_lange_Ohren(Max) |
| |
|
| |
|
| |
+++ Inferenzregeln |
| |
|
| |
++++ Modus ponems / tollens |
| |
|
| |
Siehe Aussagenlogik |
| |
|
| |
++++ AND Einführung |
| |
|
| |
F, G |
| |
____ |
| |
F AND G |
| |
|
| |
|
| |
++++ AND Elimination |
| |
|
| |
F AND G |
| |
______ |
| |
F |
| |
|
| |
|
| |
++++ FORALL Instantiierung |
| |
|
| |
**wichtig!** |
| |
|
| |
FORALL x F |
| |
________ |
| |
F [ x / t ] |
| |
|
| |
|
| |
++++ EXISTS Instantiierung |
| |
|
| |
EXISTS x F (für min. ein x bewiesen) |
| |
_______ |
| |
F [ x / C neu ] |
| |
|
| |
|
| |
(C neu muss neu rein!, siehe Sequentialkalkül: Eigenvariable. Sollte eigentlich Eigenkonstante heißen, jedoch bezeichnet selbst die englische Fachliteratur das Ding als Eigenvariable.) |
| |
|
| |
+++ Beispiele |
| |
|
| |
++++ FORALL Instantiierung |
| |
|
| |
FORALL x grandfrather(father_of(mother_of(x)), x) |
| |
________________________ |
| |
grandfather(((father_of(mother_of(John)), John) |
| |
|
| |
|
| |
++++ EXISTS Instantiierung |
| |
|
| |
(zu schnell!) |
| |
|
| |
+++ Kalkül |
| |
|
| |
Ein Kalkül k: |
| |
* ist eine Menge von Axiomen und Inferenzregeln F1, ..., Fn |- G |
| |
* liefert syntaktisches Gegenstück zur semantischen Folgerungsrelation |= |
| |
* ist korrekt gdw F |- G impliziert F |= G |
| |
* ist vollständig gdw F |= G impliziert F |- G |
| |
|
| |
Korrekt und Vollständig (unser Ziel): |
| |
** |= equiv |- |
| |
|
| |
Axiome sequentielles Kalkül: Aus Formel folgt Formel |
| |
|
| |
Alles semantisch Beweisbare müßte auch syntaktisch beweisbar sein (und umgekehrt) |
| |
|
| |
++++ Normalformeln |
| |
|
| |
Sollten wir mal gehört haben (184/2), sind aber nicht Teil des Stoffs. Umkehrfunktion / Resolution. |
| |
|
| |
|
| |
++ DescriptionLogics |
PraedikatenLogik
