FrontPage > TuWienMitschriften > WissensbasierteSysteme > PraedikatenLogik

++ PrädikatenLogik

(Folien: Logik und Inferenz 2)

Prädikatenlogik PL1 - Signaturen

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)

* Menge von Funktionssymbolen
* Menge von Prädikatensymbolen
* jedes Symbol hat Stelligkeit

+++ Funktionssymbole

mit Stelligkeit 0: Konstanten
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

* A, B, C, John
* morning_star, evening_star
* father_of(John), age(John)
* father_of(father_of(John))
* distance(morning_star, evening_star)

Konvention: Dinge mit Großbuchstaben sind Konstanten


+++ PL1: Prädikatensymbole:

* mit Stelligkeit 0, 1, 2, ...
* zum Aufbau atomarer Formeln


++++ Beispiele

* prime(3), blue(sky)
* mortal(Socrates), flight(RF75, Dortmund, Berlin)
* 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