Vorlesung InformatikDr. rer. nat. Harald Sack
Institut für InformatikFriedrich Schiller Universität Jena
Wintersemester 2006/2007
Semantic Web
http://www.informatik.uni-jena.de/~sack/WS0607/semanticweb.htm
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 2
Semantic Web - Vorlesungsinhalt
1. Einführung2. Die Sprachen des Semantic Web3. Wissensrepräsentation4. Web of Trust5. Ontology Engineering6. Semantic Web Anwendungen
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 3
Semantic Web
3. Wissensrepräsentation3.1 Ontologien in der Philosophie und der Informatik3.2 Logik (Wiederholung)
3.2.1 Aussagenlogik (PL) und Prädikatenlogik (FOL)3.2.2 Modelltheoretische Semantik3.2.3 Normalformen3.2.4 Resolution3.2.5 Eigenschaften von PL / FOL
3.3 Beschreibungslogiken und OWL 3.4 SWRL3.5 Inferenzsysteme
27.11.2006 – Vorlesung Nr. 61 2 3 4 5 7 8 9 1110 12
13
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 4
3. Wissensrepräsentation3.2 Beschreibungslogiken
Semantic Web Architecture
URI Unicode
XML / XSD Namespaces
RDF
RDFSchema
Ontologies (OWL) Rules
Trust
Sig
natu
re
Enc
rypt
ion
SP
AR
QL
Logic Framework
Proof
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 5
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Logik – Grundlagennur knappe und informelle Wiederholung
siehe Grundstudiumsvorlesungen Info / DML
im Weiteren wird ein solides Verständnis der Grundlagen der Logik vorausgesetzt, daher bitte selbstständig wiederholen
siehe auchU. Schöning: Logik für Informatiker, Spektrum Akademischer Verlag, 5. Aufl. 2000.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 6
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Logik – GrundlagenSyntax: Zeichen ohne Bedeutung
definiert Regeln, wie zulässige Zeichenfolgen gebildet werden dürfen
Semantik: Bedeutung der Syntaxdefiniert Regeln, wie die Bedeutung von komplexenZeichenfolgen aus der Bedeutung von atomarenZeichenfolgen abgeleitet werden kann
If (i<0) then display (“negatives Guthaben!“)
Gebe die Meldung “negatives Guthaben!“ aus,wenn der Kontostand i unter 0 Euro sinkt.
Zuweisung vonBedeutung
Syntax
Bedeutung, z.B. ‘die reale Welt‘
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 7
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Was ist Semantik?Beispiel: Programmiersprachen
FUNCTION f(n:natural):natural;BEGIN
IF n=0 THEN f:=1ELSE f:=n*f(n-1);
END;
Berechnung der Fakultät
Syntax
Intendierte Semantik
n!n:f →formale Semantik
Verhalten des Programmsbei der Ausführung
Prozedurale Semantik
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 8
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Aussagenlogik
Prädikatssymbole/aussagenlogische Variablen, z.B. p, q, r, s, …„richtiges“ Formen von Formeln – im Zweifelsfall klammern:
((p ∧ ¬q) ∨ s) → ¬p(p ↔ ¬q) ↔ (q ∨ ¬p)
Präzedenzen: ¬ vor ∧,∨ vor →, ↔
„genau dann, wenn“Äquivalenz↔„wenn – dann“Implikation→
„oder“Disjunktion⋁„und“Konjunktion∧„nicht“Negation⌐
Intuitive BedeutungNameJunktor
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 9
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Aussagenlogik: Beispiele
nDie Straße wird nassrEs regnetgDie Sonne ist grün
ModellierungEinfache Aussagen
(r ∧ ⌐n) gWenn es regnet und die Straße nicht nass wird, dann ist die Sonne grün
r nWenn es regnet, dann wird die Straße nassModellierungZusammengesetzte Aussagen
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 10
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Prädikatenlogik erster Stufe (First Order Logic, FOL)
Junktoren wie in der AussagenlogikVariablen, z.B. X,Y,Z,…Konstantensymbole, z.B. a, b, c, …Funktionssymbole, z.B. f, g, h, … (mit Stelligkeit)Relations-/Prädikatssymbole, z.B. p, q, r, … (mit Stelligkeit)
(∀X)(∃Y) ((p(X)∨ ¬q(f(X),Y))→ r(X))
„für alle“Allquantor, Universalquantor
∀„es existiert“Existenzquantor∃
Intuitive BedeutungNameQuantor
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 11
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
FOL: Syntax
„richtiges“ Formen von Termen aus Variablen, Konstanten- und Funktionssymbolen:
f(X), g(a,f(Y)), s(a), .(H,T), x_location(Pixel)
„richtiges“ Formen von Atomen aus Relationssymbolen, deren Argumente Terme sind:
p(f(X)), q (s(a),g(a,f(Y))), add(a,s(a),s(a)), greater_than(x_location(Pixel),128)
„richtiges“ Formen von Formeln aus Atomen, Junktoren und Quantoren:
(∀Pixel) (greater_than(x_location(Pixel),128) → red(Pixel) )
Im Zweifelsfall klammern! Alle Variablen quantifizieren!
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 12
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
FOL: Beispiel Addition
(∀X)(∀Y)(∀Z)( add(a,X,X)∧ ( add(X,Y,Z) → add(s(X),Y,s(Z)) )
)
Intendierte Semantik:a … 0 (natürliche Zahl Null)s … Nachfolgerfunktion/Addition von Einsadd(x,y,z) … „z ist die Summe von x und y“
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 13
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
FOL: Beispiel Listen
(∀H)(∀T) ( list([]) ∧ (list(T) → list(.(H,T)) ))
Informell: [] … leere Liste.(H,T) … H ist Kopf, T Restlisteschreibe auch .(H,T) als [H|T]
(∀H)(∀T)( member(a,[a|T])∧ ( member(a,T) → member(a,[H|T]) )
)
Intendierte Semantik:member(x,liste) … “x ist Element von liste”
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 14
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
FOL: Beispiel Verwandtschaft
(∀X) ( parent(X) ↔ ( human(X) ∧ (∃Y) parent_of(X,Y) ))
(∀X) ( human(X) → (∃Y) parent_of(Y,X) )
(∀X) (orphan(X) ↔ (human(X) ∧¬(∃Y) (parent_of(Y,X)∧ alive(Y))))
(∀X)(∀Y)(∀Z)( uncle_of(X,Z) ↔ (brother_of(X,Y) ∧ parent_of(Y,Z)) )
Intendierte Semantik: klar!
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 15
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
FOL: Beispiel Pinguine
( (∀X)( penguin(X) → blackandwhite(X) )∧ (∃X)( oldTVshow(X) ∧ blackandwhite(X) )) → (∃X)( penguin(X) ∧ oldTVshow(X) )
Intendierte Semantik?
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 16
Semantic Web
3. Wissensrepräsentation3.1 Ontologien in der Philosophie und der Informatik3.2 Logik (Wiederholung)
3.2.1 Aussagenlogik (PL) und Prädikatenlogik (FOL)3.2.2 Modelltheoretische Semantik3.2.3 Normalformen3.2.4 Resolution3.2.5 Eigenschaften von PL / FOL
3.3 Beschreibungslogiken und OWL 3.4 SWRL3.5 Inferenzsysteme
27.11.2006 – Vorlesung Nr. 61 2 3 4 5 7 8 9 1110 12
13
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 17
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Aussagenlogik: Modelltheoretische Semantik
Interpretation I:Abbildung aller Prädikatssymbole nach {w,f}.
Ist F eine Formel und I eine Interpretation, dann ist I(F) ein Wahrheitswert, der aus F und I mittels Wahrheitstafeln ermittelt wird.
wwtwfww
fffwffw
fwfwwwf
wwwfwff
I(p↔q)I(p→q)I(p∧q)I(p⋁q)I(⌐p) I(q)I(p)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 18
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Aussagenlogik: Modelltheoretische Semantik
Wir schreiben I ⊨ F, wenn I(F)=w ist, und nennen dann die Interpretation I ein Modell der Formel F.
Zentrale Begriffe:allgemeingültig (Tautologie)erfüllbarwiderlegbarunerfüllbar
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 19
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Prädikatenlogik: Modelltheoretische Semantik
Struktur:Festlegung eines Grundbereichs D.Konstantensymbole werden auf Elemente von D abgebildet.Funktionssymbole auf Funktionen auf D.Relationssymbole auf Relationen über D.
Dann:Terme werden zu Elementen von D.Relationssymbole mit Argumenten werden wahr oder falsch.Entsprechende Behandlung der Junktoren/Quantoren.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 20
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Prädikatenlogik: Modelltheoretische SemantikBeispiel Addition
Modell I:Grundbereich: natürliche Zahlen NI(a) = 0I(s): n n+1l(add(k,m,n))=w genau dann, wenn k+m=n ist.
I ist Modell der Formel.
(∀X)(∀Y)(∀Z)( add(a,X,X)∧ ( add(X,Y,Z) → add(s(X),Y,s(Z)) )
)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 21
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Prädikatenlogik: Modelltheoretische SemantikBeispiel: Pinguine
( (∀X)( penguin(X) → blackandwhite(X) )∧ (∃X)( oldTVshow(X) ∧ blackandwhite(X) )) → (∃X)( penguin(X) ∧ oldTVshow(X) )
Interpretation I:Grundbereich: eine Menge M, die Elemente a,b,c enthält.… keine Konstanten- oder Funktionssymbole …Wir zeigen: Die Formel ist widerlegbar (d.h. sie ist nicht allgemeingültig):
Sind I(penguin)(a), I(blackandwhite)(a), I(oldTVshow)(b),I(blackandwhite)(b) wahr, I(oldTVshow)(a) jedoch falsch,
dann ist die Formel unter I falsch, d.h. I ⊭ F.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 22
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Der Begriff der logischen KonsequenzEine Theorie T ist eine Menge von Formeln.Eine Interpretation I ist ein Modell für T, wenn I ⊨ G für jede Formel G in T gilt.Eine Formel F ist eine logische Konsequenz aus T, wenn jedes Modell von T auch Modell von F ist.Wir schreiben dann T ⊨ F.
Zwei Formeln F,G heißen logisch (auch semantisch) äquivalent, wenn {F} ⊨ G und {G} ⊨ F gelten.Wir schreiben dann F ≡ G.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 23
DeMorgan‘sche Gesetze
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Logische Äquivalenz - Beispiele
F ∧ G ≡ G ∧ FF ∨ G ≡ G ∨ F
F → G ≡ ¬F ∨ GF ↔ G ≡ (F → G) ∧ (G → F)
¬(F ∧ G) ≡ ¬F ∨ ¬G¬(F ∨ G) ≡ ¬F ∧ ¬G
¬¬F ≡ F
F ∨ (G ∧ H) ≡ (F ∨ G) ∧ (F ∨ H)F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H)
¬(∀X) F ≡ (∃X) ¬F¬(∃X) F ≡ (∀X) ¬F
(∀X)(∀Y) F ≡ (∀Y)(∀X) F(∃X)(∃Y) F ≡ (∃Y)(∃X) F
(∀X) (F ∧ G) ≡ (∀X) F ∧ (∀X) G(∃X) (F ∨ G) ≡ (∃X) F ∨ (∃X) G
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 24
Semantic Web
3. Wissensrepräsentation3.1 Ontologien in der Philosophie und der Informatik3.2 Logik (Wiederholung)
3.2.1 Aussagenlogik (PL) und Prädikatenlogik (FOL)3.2.2 Modelltheoretische Semantik3.2.3 Normalformen3.2.4 Resolution3.2.5 Eigenschaften von PL / FOL
3.3 Beschreibungslogiken und OWL 3.4 SWRL3.5 Inferenzsysteme
27.11.2006 – Vorlesung Nr. 61 2 3 4 5 7 8 9 1110 12
13
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 25
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Normalformen
Zu jeder Formel gibt es unendlich viele logisch äquivalente Formeln.Für jede solche Äquivalenzklasse sucht man nun möglichst einfache Repräsentanten.
Diese Repräsentanten werden Normalformen genannt.
Einfaches Beispiel:schreibe ¬F statt ¬¬¬¬¬F
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 26
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Normalformen
Ziel: Umwandlung von Formeln in Klauselform.
Zwischenschritte:
1. Negationsnormalform• alle Negationen stehen ganz innen
2. Pränexnormalform• alle Quantoren stehen ganz vorne
3. Skolemisierte Pränexnormalform• Eliminierung der Existenzquantoren
4. konjunktive Normalform (CNF) = Klauselform• Darstellung als Konjunktion von Disjunktionen
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 27
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Negationsnormalform
Alle Negationszeichen werden durch Verwendung der folgenden Äquivalenzen nach innen gezogen:
F ↔ G ≡ (F → G)∧(G → F) ¬(F ∧ G) ≡ ¬F ∨ ¬GF → G ≡ ¬F ∨ G ¬(F ∨ G) ≡ ¬F ∧ ¬G
¬(∀X) F ≡ (∃X) ¬F ¬¬F ≡ F¬(∃X) F ≡ (∀X) ¬F
Ergebnis:Implikationen und Äquivalenzen fallen wegmehrfachen Negationen fallen wegalle Negationszeichen stehen direkt vor Atomen
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 28
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
NegationsnormalformBeispiel
( (∀X)( penguin(X) → blackandwhite(X) )∧ (∃X)( oldTVshow(X) ∧ blackandwhite(X) )) → (∃X)( penguin(X) ∧ oldTVshow(X) )wird zu¬( (∀X)( ¬penguin(X) ∨ blackandwhite(X) )∧ (∃X)( oldTVshow(X) ∧ blackandwhite(X) )) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) )und dann zu( (∃X)( penguin(X) ∧ ¬blackandwhite(X) )∨ (∀X)(¬oldTVshow(X) ∨ ¬blackandwhite(X) )) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) )
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 29
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Pränexnormalformerst Formel bereinigen (Quantoren binden verschiedene Variablen).
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) )∨ (∀X)( ¬oldTVshow(X) ∨ ¬blackandwhite(X) )) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) )
wird zu
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) )∨ (∀Y)( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) )) ∨ (∃Z)( penguin(Z) ∧ oldTVshow(Z) )
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 30
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
PränexnormalformDann aus der Negationsnormalform einfach alle Quantoren in derselben Reihenfolge nach vorne ziehen.
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) )∨ (∀Y)( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) )) ∨ (∃Z)( penguin(Z) ∧ oldTVshow(Z) )
wird zu
(∃X)(∀Y)(∃Z)( ( penguin(X) ∧ ¬blackandwhite(X) )∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )∨ ( penguin(Z) ∧ oldTVshow(Z) )
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 31
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Skolemnisierte Normalform“Existenzquantoren entfernen”
(∃X) (∀Y) (∃Z) ( ( penguin(X) ∧ ¬blackandwhite(X) )∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )∨ ( penguin(Z) ∧ oldTVshow(Z) )
wird zu …
(∀Y)( ( penguin(a) ∧ ¬blackandwhite(a) )∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )∨ ( penguin( f(Y) ) ∧ oldTVshow( f(Y) ) )
wobei a und f neue Symbole sind (sog. Skolemkonstanten bzw. –funktionen).
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 32
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Skolemnisierte NormalformVorgehensweise:
1. Entfernen der Existenzquantoren von links nach rechts.
2. Gibt es keinen Allquantor links des zu entfernenden Existenzquantors, so wird die entsprechende Variable durch ein neues Konstantensymbol ersetzt.
3. Gibt es n Allquantoren links des zu entfernenden Existenzquantors, so wird die entsprechende Variable durch ein neues Funktionssymbol mit Stelligkeit n ersetzt, dessen Argumente genau die Variablen der n Allquantoren sind.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 33
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Konjunktive Normalform (Klauselform)Es gibt nur noch Allquantoren, also lassen wir sie weg:
( penguin(a) ∧ ¬blackandwhite(a) )∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )∨ ( penguin(f(Y)) ∧ oldTVshow(f(Y))
Mit Hilfe semantischer Äquivalenzen wird die Formel nun als Konjunktion von Disjunktionen geschrieben.
F ∨ (G ∧ H) ≡ (F ∨ G) ∧ (F ∨ H)F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 34
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Konjunktive Normalform (Klauselform)
( (penguin(a) ∧ ¬blackandwhite(a) )∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )∨ ( penguin(f(Y)) ∧ oldTVshow(f(Y))
wird zu …….
( penguin(a)∨¬oldTVshow(Y)∨¬blackandwhite(Y)∨penguin(f(Y)))∧ ( penguin(a)∨¬oldTVshow(Y)∨¬blackandwhite(Y)∨oldTVshow(f(Y)))∧ ( ¬blackandwhite(a)∨oldTVshow(Y)∨¬blackandwhite(Y)∨penguin(f(Y)))∧ ( ¬blackandwhite(a)∨oldTVshow(Y)∨¬blackandwhite(Y)∨oldTVshow(f(Y)))
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 35
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Eigenschaften von Normalformen
Sei F eine Formel,G die Pränexnormalform von F,H die skolemisierte Pränexnormalform von G,K die Klauselform von H.
Dann ist F ≡ G und H ≡ K aber i.A. F ≢ K.
Es gilt jedoch:F ist unerfüllbar genau dann, wenn K unerfüllbar ist.(Grundlage des Resolutionsverfahrens)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 36
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Skolemnisierung ist keine Äquivalenztransformation
Die Formel (∃x) p(x) ∨ ¬(∃x) p(x) ist eine Tautologie.
Negationsnormalform: (∃x) p(x) ∨ (∀y) ¬p(y)Pränexnormalform: (∃x) (∀y) (p(x) ∨ ¬p(y))Skolemnormalform: (∀y) (p(a) ∨ ¬p(y))Äquivalent dazu: p(a) ∨ ¬(∃y) p(y)Die resultierende Formel ist keine Tautologie!
z.B. Interpretation I mitI(p(a)) = fI(p(b)) = w
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 37
Semantic Web
3. Wissensrepräsentation3.1 Ontologien in der Philosophie und der Informatik3.2 Logik (Wiederholung)
3.2.1 Aussagenlogik (PL) und Prädikatenlogik (FOL)3.2.2 Modelltheoretische Semantik3.2.3 Normalformen3.2.4 Resolution3.2.5 Eigenschaften von PL / FOL
3.3 Beschreibungslogiken und OWL 3.4 SWRL3.5 Inferenzsysteme
27.11.2006 – Vorlesung Nr. 61 2 3 4 5 7 8 9 1110 12
13
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 38
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution
{F1,…,Fn} hat F0 als logische Konsequenz{F1,…,Fn} ⊨ F0
F1 ∧… ∧ Fn → F0 ist allgemeingültig¬(F1 ∧… ∧ Fn → F0) ist unerfüllbar
G1 ∧ …∧ Gk ist unerfüllbar
Das Resolutionsverfahren erlaubt die Ableitung eines Widerspruchs aus G1 ∧ …∧ Gk.
Theorie
Transformation in Klauselform
Äqu
ival
ente
Aus
sage
n
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 39
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Aussagenlogik)
Ist (p1∨…∨pk∨p∨¬q1∨…∨¬ql)∧(r1∨…∨rm∨¬p∨¬s1∨…∨¬sn)wahr, dann:
Eines von p, ¬p muss falsch sein.
Also: Eines der anderen muss wahr sein. D.h.p1∨…∨pk∨¬q1∨…∨¬ql∨r1∨…∨rm∨¬s1∨…∨¬sn
muss wahr sein.
Ergo: Ist p1∨…∨pk∨¬q1∨…∨¬ql∨r1∨…∨rm∨¬s1∨…∨¬sn unerfüllbar,dann auch(p1∨…∨pk∨p∨¬q1∨…∨¬ql)∧(r1∨…∨rm∨¬p∨¬s1∨…∨¬sn)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 40
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Aussagenlogik)
(p1∨…∨pk∨p∨¬q1∨…∨¬ql) (r1∨…∨rm∨¬p∨¬s1∨…∨¬sn)
p1∨…∨pk∨¬q1∨…∨¬ql∨r1∨…∨rm∨¬s1∨…∨¬sn
Aus zwei Klauseln wird eine neue
Werden Klauseln resolviert, die nur noch aus je einem Atom bzw. negierten Atom bestehen, dann entsteht eine „leere Klausel“, bezeichnet mit ⊥.
K1 K2
K3
{K1,K 2} ⊨ K3Resolutionsschritt
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 41
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Aussagenlogik)
Vorgehensweise, um einen Widerspruch aus einer Menge M von Klauseln abzuleiten:
1. Wähle zwei Klauseln aus M und erzeuge aus ihnen eine neue Klausel K durch einen Resolutionsschritt.
2. Ist K =⊥ , dann ist ein Widerspruch gefunden.
3. Falls K ≠⊥ , füge K zur Menge M hinzu und gehe zu 1.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 42
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik)
In der Prädikatenlogik müssen bei der Resolution zusätzlich Variablenbindungen mit Hilfe von Substitutionen berücksichtigt werden
z.B.
(p(X,f(Y)) ∨ q( f(X),Y)) (¬p(a,Z) ∨ r(Z) )
(q( f(a),Y) ∨ r(f(Y))).
Resolution mit [X/a, Z/f(Y)] ergibt
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 43
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik) - Beispiel
Terminologisches Wissen (DL: TBox):(∀X) ( human(X) → (∃Y) parent_of(Y,X) )(∀X) ( orphan(X) ↔ (human(X) ∧ ¬(∃Y) (parent_of(Y,X) ∧ alive(Y)))
Wissen um Individuen (DL: ABox):orphan(harrypotter)parent_of(jamespotter,harrypotter)
Können wir folgern: ¬alive(jamespotter)?
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 44
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik) - Beispiel
Zu zeigen:
((∀X) ( human(X) → (∃Y) parent_of(Y,X) )∧ (∀X) (orphan(X) ↔ (human(X) ∧ ¬(∃Y) (parent_of(Y,X) ∧ alive(Y)))∧ orphan(harrypotter)∧ parent_of(jamespotter,harrypotter)) → ¬alive(jamespotter))
ist allgemeingültig.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 45
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik) - Beispiel
Zu zeigen:
¬((∀X) ( human(X) → (∃Y) parent_of(Y,X) )∧ (∀X) (orphan(X) ↔ (human(X) ∧ ¬(∃Y) (parent_of(Y,X) ∧ alive(Y)))∧ orphan(harrypotter)∧ parent_of(jamespotter,harrypotter)) → ¬alive(jamespotter))
ist unerfüllbar.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 46
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik) - Beispiel
Pränexnormalform:
(∀X)(∃Y)(∀X1)(∀Y1)(∀X2)(∃Y2)(( ¬human(X) ∨ parent_of(Y,X) ) ∧ (¬orphan(X1)∨ (human(X1) ∧ (¬parent_of(Y1,X1) ∨ ¬alive(Y1)))∧ (orphan(X2) ∨ (¬human(X2) ∨ (parent_of(Y2,X2) ∧ alive(Y2)))∧ orphan(harrypotter)∧ parent_of(jamespotter,harrypotter))∧ alive(jamespotter))
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 47
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik) - Beispiel
Klauselform:
( ¬human(X) ∨ parent_of(f(X),X) )∧ (¬orphan(X1) ∨ human(X1))∧ (¬orphan(X1) ∨ ¬parent_of(Y1,X1) ∨ ¬alive(Y1))∧ (orphan(X2) ∨ ¬human(X2) ∨parent_of(g(X,X1,Y1,X2),X2))∧ (orphan(X2) ∨ ¬human(X2) ∨ alive(g(X,X1,Y1,X2)))∧ orphan(harrypotter)∧ parent_of(jamespotter,harrypotter))∧ alive(jamespotter)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 48
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Resolution (Prädikatenlogik) - Beispiel
1. ( ¬human(X) ∨ parent_of(f(X),X) )2. ∧ (¬orphan(X1) ∨ human(X1))3. ∧ (¬orphan(X1) ∨ ¬parent_of(Y1,X1)
∨ ¬alive(Y1))4. ∧ (orphan(X2) ∨ ¬human(X2)
∨parent_of(g(X,X1,Y1,X2),X2))5. ∧ (orphan(X2) ∨ ¬human(X2)
∨ alive(g(X,X1,Y1,X2)))6. ∧ orphan(harrypotter)7. ∧ parent_of(jamespotter,harrypotter))8. ∧ alive(jamespotter)
9. .¬orphan(harrypotter)∨ ¬alive(jamespotter) (3,7)
10. ¬orphan(harrypotter) (8,9)11. ⊥ (6,10)
Wissen: Abgeleitete Klauseln:
(Tableauverfahren siehe Übung)
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 49
Semantic Web
3. Wissensrepräsentation3.1 Ontologien in der Philosophie und der Informatik3.2 Logik (Wiederholung)
3.2.1 Aussagenlogik (PL) und Prädikatenlogik (FOL)3.2.2 Modelltheoretische Semantik3.2.3 Normalformen3.2.4 Resolution3.2.5 Eigenschaften von PL / FOL
3.3 Beschreibungslogiken und OWL 3.4 SWRL3.5 Inferenzsysteme
27.11.2006 – Vorlesung Nr. 61 2 3 4 5 7 8 9 1110 12
13
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 50
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Eigenschaften der Prädikatenlogik
MonotonieBei Vergrößerung des Wissens gehen keine Schlussfolgerungen verloren.
KompaktheitFür jede Schlussfolgerung aus einer Theorie genügt eine endlicheTeilmenge der Theorie.
SemientscheidbarkeitAlle wahren Schlüsse lassen sich finden, wenn man lange genug sucht.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 51
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Eigenschaften der Aussagenlogik
Alle genannten Eigenschaften der Prädikatenlogik.
EntscheidbarkeitAlle wahren Schlüsse lassen sich finden, und alle falschen Schlüsse lassen sich widerlegen, wenn man lange genug sucht.
D.h. es gibt immer terminierende automatische Beweiser.
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 52
3. Wissensrepräsentation3.2 Beschreibungslogiken / 3.2.1 Logik – Grundlagen
Wichtige Fragmente der Prädikatenlogik
AussagenlogikDatalog (wie pures/reines Prolog, aber ohne Funktionssymbole)
entscheidbarDisjunktives Datalog (Klauseln ohne Funktionssymbole)
entscheidbarHornklauseln (pures/reines Prolog)
seminentscheidbarBeschreibungslogiken
entscheidbar (manche)z.B. OWL → nächster Teil der Vorlesung
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 53
Semantic Web
3. Wissensrepräsentation3.1 Ontologien in der Philosophie und der Informatik3.2 Logik (Wiederholung)
3.2.1 Aussagenlogik (PL) und Prädikatenlogik (FOL)3.2.2 Modelltheoretische Semantik3.2.3 Normalformen3.2.4 Resolution3.2.5 Eigenschaften von PL / FOL
3.3 Beschreibungslogiken und OWL 3.4 SWRL3.5 Inferenzsysteme
27.11.2006 – Vorlesung Nr. 61 2 3 4 5 7 8 9 1110 12
13
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 54
3. Wissensrepräsentation
Literatur
F. Baader, D. Calvanese, D. McGuinnessThe Description Logics HandbookCambridge University Press, 2003.
U. SchöningLogik für Informatiker,Spektrum Akademischer Verlag, 5.Aufl. 2000
Semantic WebDr. Harald Sack, Institut für Informatik, FSU Jena, Ernst-Abbe-Platz 2-4, D-07743 Jena, E-Mail: [email protected] 55
3. Wissensrepräsentation
Literatur
Materialien-Webseitehttp://www.informatik.uni-jena.de/~sack/WS0607/semanticweb-materialien.htm
bibsonomy - Bookmarkshttp://www.bibsonomy.org/user/lysander07