| Lines 112 - 114 |
Lines 112 - 186 |
| ++++ 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 |
| |
|
| |
|
PraedikatenLogik
