Lines 112 - 114 |
Lines 112 - 309 |
++++ Beispiel |
++++ Beispiel |
|
|
[brother] { ( Charles, Edward), ( Charles, Andrew) , (Edward, Andrew) } teilmenge_von U x U |
[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 |