Vorlesung
Dr. Harald Sack
Hasso-Plattner-Institut für Softwaresystemtechnik
Universität Potsdam
Wintersemester 2009/10
Semantic Web
Blog zur Vorlesung: http://sewe0910.blogspot.com/Die nichtkommerzielle Vervielfältigung, Verbreitung und Bearbeitung dieser Folien ist zulässig (Lizenzbestimmungen CC-BY-NC).
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
1. Einführung
2. Semantic Web BasisarchitekturDie Sprachen des Semantic Web - Teil 1
3. Wissensrepräsentation und LogikDie Sprachen des Semantic Web - Teil 2
4. Ontology Engineering
5. Semantic Web Applications
2
Semantic Web - Vorlesungsinhalt
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
Semantic Web Architektur3
URI / IRI
XML / XSDData Interchange: RDF
RDFS
Ontology: OWL Rule: RIF
Query:SPARQL
Proof
Unifying Logic
Cry
pto
Trust
Interface & Application
3. Wissensrepräsentation und Logik
Ontology-Level
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
45.01.2010 – Vorlesung Nr. 81 2 3 4 5 6 7 9 1110 12
13
3. Wissensrepräsentation und LogikDie Sprachen des Semantic Web - Teil 2
3.1.Ontologien in der Philosophie und der Informatik
3.2.Wiederholung Aussagenlogik und Prädikatenlogik
3.3.RDFS-Semantik
3.4.Beschreibungslogiken
3.5.OWL und OWL-Semantik
3.6.Regeln mit RIF/SWRL
14
Semantic Web - Vorlesungsinhalt
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
5
Beschreibungslogiken und OWL
3.4 Beschreibungslogiken
3.4.1 Motivation
3.4.2 Beschreibungslogiken Überblick
3.4.3 ALC - Syntax und Semantik
3.4.4 Inferenz und Reasoning
3.4.5 Tableaux-Verfahren
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
6
3. Wissensrepräsentationen3.4 Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
7
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.1 Motivation
Ontologien in der Informatik
An Ontology is aformal specification
of a shared
conceptualizationof a domain of interest
Tom Gruber, 1993
⇒ machine understandable
⇒ group of people/agents
⇒ about concepts⇒ between general description and individual use
...aber wozu braucht man in der Informatik überhaupt Ontologien?
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
8
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.1 Motivation
Ontologien und Kommunikation
Person 1 Person 2
Symbol
Concept
Thing
exchange of symbols„Golf“
conceptH1
conceptH2
agreement
M1 M2
Agent 1 Agent 2
exchangeof symbols
OntologyDescription
Semantics
Ontology agreement
specific domain,e.g. sports
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
9
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.1 Motivation
RDF und RDFS• Definition von Klassen,
Klassenhierarchien,Relationen,Individuen
• zur DefinitioneinfacherOntologiengeeignet
• für komplexereModellierungaber nicht geeignet
http://.../isbn/000651409X
WWW - Kommunikation, Internetworking,Webtechnologien
2004
a:titel
a:jahr
a:autor
a:verlag
Harald Sack
http://www.hpi.uni-potsdam.de/meinel/sack.html
a:name
a:homepage
Springer
Heidelberg
a:v_name
a:v_ort
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
10
Wir benötigen ein ausdruckstärkeresMittel zur Wissensrepräsentation
3.4 Beschreibungslogiken
3.4.1 Motivation
3.4.2 Beschreibungslogiken Überblick
3.4.3 ALC - Syntax und Semantik
3.4.4 Inferenz und Reasoning
3.4.5 Tableaux-Verfahren
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
11
3. Wissensrepräsentationen3.4 Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
12
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.2 Beschreibungslogiken Überblick
FOL als Semantic Web Sprache?•Warum nicht einfach FOL für Ontologien hernehmen?
•FOL kann alles
•….. Assembler auch
•FOL ist
•sehr ausdrucksstark
•deshalb unhandlich bei der Modellierung
•schlecht geeignet um Konsens bei der Modellierung zu finden
•Beweistheoretisch sehr komplex (semi-entscheidbar)
•FOL ist keine Markupsprache
Suche ein geeignetes Fragment von FOL
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
13
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.2 Beschreibungslogiken Überblick
Beschreibungslogiken (DLs)• engl.: description logics (DLs)
• Fragmente von FOL
• In DL werden mit Hilfe von Konstruktoren aus einfachen Beschreibungen (descriptions) komplexere Beschreibungen aufgebaut
• DLs unterscheiden sich durch die Menge der verwendeten Konstruktoren (Ausdrucksmächtigkeit)
• entwickelt aus „semantischen Netzwerken“
• meist entscheidbar
• vergleichsweise ausdrucksstark
• enge Verwandtschaft mit Modallogiken
• W3C Standard OWL DL basiert auf der Beschreibungslogik SHOIN(D)
Allgemeine DL Architektur
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
14
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.2 Beschreibungslogiken Überblick
Knowledge Base
TBox Terminological Knowledge Wissen über Konzepte einer Domäne (Klassen, Attribute, Eigenschaften,..)
Student: {x | Student(x)}nimmtTeilAn: {(x,y) | nimmtTeilAn(x,y)}
ABox Assertional Knowledge Wissen über Instanzen / Entitäten
Student(Christian)nimmtTeilAn(Christian, Semantic Web)
Infe
renc
e E
ngin
e
Inte
rface
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
15
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.2 Beschreibungslogiken Überblick
Allgemeiner DL Aufbau•DLs sind eine Familie logikbasierter Formalismen zur Wissensrepräsentation
•Spezielle Sprachen u.a. charakterisiert durch:• Konstruktoren für komplexe Konzepte und Rollen aus einfacheren Konzepten und Rollen
• Menge von Axiomen, um Fakten über Konzepte, Rollen und Individuen auszudrücken
•ALC (Attribute Language with Complement) ist die kleinste DL, die aussagenlogisch abgeschlossen ist
• Konjunktion, Disjunktion, Negation sind Klassenkonstruktoren,geschrieben ⊓, ⊔ , ¬
• Quantoren schränken Rollenbereiche ein:
Man ⊓ ∃hasChild.Female ⊓ ∃hasChild.Male ⊓ ∀hasChild.(Rich ⊔ Happy)
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
16
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.2 Beschreibungslogiken Überblick
Weitere DL Sprachmittel•Weitere Konstruktoren sind z.B.
•Number restrictions (Kardinalitätseinschränkungen) für Rollen:≥3 hasChild, ≤1 hasMother
•Qualified number restrictions (klassenspezifische Kardinalitätseinschränkungen) für Rollen:≥2 hasChild.Female, ≤1 hasParent.Male
•Nominals (definition by extension, Aufzählungsklassen): {Italy, France, Spain}
•Concrete domains (datatypes): hasAge.(≥21)
•Inverse roles: hasChild– ≡ hasParent
•Transitive roles: hasAncestor ⊑+ hasAncestor
•Role composition: hasParent.hasBrother(uncle)
3.4 Beschreibungslogiken
3.4.1 Motivation
3.4.2 Beschreibungslogiken Überblick
3.4.3 ALC - Syntax und Semantik
3.4.4 Inferenz und Reasoning
3.4.5 Tableaux-Verfahren
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
17
3. Wissensrepräsentationen3.4 Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
18
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC Grundbausteine•Grundbausteine:
•Klassen
•Rollen
• Individuen
•Student(Christian)Individuum Christian ist in Klasse Student
•nimmtTeilAn(Christian, VorlesungSemanticWeb)Christian nimmt an der Vorlesung SemanticWeb teil
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
19
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
Attributive Language with Complement - ALC• Atomare Typen
• Konzeptnamen A, B, ...
• Spezielle Konzepte
• ⊤ - Top (universelles Konzept)
• ⊥ - Bottom Konzept
• Rollennamen R,S, ...
• Konstruktoren
• Negation: ¬C
• Konjunktion: C ⊓ D
• Disjunktion: C ⊔ D
• Existenzquantor: ∃R.C
• Allquantor: ∀R.C
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
20
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC Grundbausteine•Klasseninklusion
•Professor ⊑ Fakultaetsmitglied
• jeder Professor ist ein Fakultätsmitglied
•entspricht (∀x)(Professor(x) → Fakultaetsmitglied(x))
•Klassenäquivalenz
•Professor ≡ Fakultaetsmitglied
•Die Fakultätsmitglieder sind genau die Professoren
•entspricht (∀x)(Professor(x) ↔ Fakultaetsmitglied(x))
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
21
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC komplexe Klassenbeziehungen•Konjunktion ⊓
•Disjunktion ⊔
•Negation ¬
(∀x)(Professor(x) → ((Person(x) Λ Universitaetsangehoeriger(x))
V (Person(x) Λ ¬Student(x)))
Professor ⊑ (Person ⊓ Unversitaetsangehoeriger) ⊔ (Person ⊓ ¬Student)
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
22
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC Quantoren auf Rollen•Strikte Bindung einer Klasse als Bildmenge (Range) einer Rolle
•Pruefung ⊑ ∀hatPruefer.Professor
•Eine Prüfung wird immer nur von einem Professor abgenommen
• (∀x)(Pruefung(x) → (∀y)(hatPruefer(x,y) → Professor(y)))
•Offene Bindung einer Klasse als Bildmenge einer Rolle
•Pruefung ⊑ ∃hatPruefer.Person
• Jede Prüfung hat mindestens einen Prüfer
• (∀x)(Pruefung(x) → (∃y)(hatPruefer(x,y) Λ Person(y)))
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
23
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC - formale Syntax•Folgende Syntaxregeln erzeugen Klassen in ALC, dabei ist A eine atomare Klasse, C und D komplexe Klassen und R eine Rolle:
•C,D ::= A | ⊤ | ┴ | ¬C | C ⊓ D | C ⊔ D | ∃R.C | ∀R.C
•Eine ALC TBox besteht aus Aussagen der Form C ⊑ D und C ≡ D, wobei C, D komplexe Klassen sind.
•Eine ALC ABox besteht aus Aussagen der Form C(a) und R(a,b), wobei C eine komplexe Klasse, R eine Rolle und a,b Individuen sind.
•Eine ALC-Wissensbasis besteht aus einer ABox und einer TBox.
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
24
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC - Semantik (Interpretationen)•wir definieren eine modelltheoretische Semantik für ALC (d.h. Folgerung wird über Interpretationen definiert)
•eine Interpretation I=(ΔI,.I) besteht aus
•einer Menge ΔI, genannt Domäne und
•einer Funktion .I, die abbildet von
• Individuennamen a auf Domänenelemente aI ∈ ΔI
•Klassennamen C auf Mengen von Domänenelementen CI ⊆ ΔI
•Rollennamen R auf Mengen von Paaren von Domänenelementen RI ⊆ ΔI × ΔI
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
25
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC - Semantik (Interpretationen)• schematisch:
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
26
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC - Semantik •wird auf komplexe Klassen erweitert:
•⊤I = ΔI
• (C ⊔ D)I = CI ∪ DI
• (¬C)I = ΔI \ CI
•∀R.C = { x | ∀(x,y) ∈ RI → y ∈ CI}
•∃R.C = { x | ∃(x,y) ∈ RI mit y ∈ CI}
•und auf Axiome:
•C(a) gilt, wenn aI ∈ CI
•R(a,b) gilt, wenn (aI,bI) ∈ RI
•C ⊑ D gilt, wenn CI ⊆ DI
•C ≡ D gilt, wenn CI = DI
•⊥I = ∅
• (C ⊓ D)I = CI ∩ DI
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
27
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC - alternative Semantik
•Übersetzung in die Prädikatenlogik mittels der Abbildung π
•ABox: π (C(a))=C(a)π (R(a,b))=R(a,b)
•TBox:rekursive Definition
•Dabei sind C,D komplexe Klassen, R eine Rolle und A eine atomare Klasse.
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
28
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
ALC - Wissensbasis •Terminologisches Wissen (TBox)Axiome, die die Struktur der zu modellierenden Domäne beschreiben (konzeptionelles Schema):
•Human ⊑ ∃parentOf.Human
•Orphan ≡ Human ⊓ ¬∃hasParent.Alive
•Assertionales Wissen (ABox)Axiome, die konkrete Situationen (Daten) beschreiben:
•Orphan(harrypotter)
•hasParent(harrypotter,jamespotter)
•Semantik und logische Konsequenzen klar, da übersetzbar nach FOL
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
29
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
Operator/Construktor Syntax SpracheSprache
Konjunktion A ⊓ B
FL
S*
Wertrestriktion ∀R.C FL
S*
Existenzquantor ∃R
FL
S*
Top ⊤
AL*
S*Bottom ⊥
AL*
S*Negation ¬A
AL*
S*
Disjunktion A ⊔ B AL*
S*
Existentielle Restriktion ∃R.C
AL*
S*
Zahlenrestriktion (≤nR) (≥nR)
AL*
S*
Menge von Individuen {a1,...,a2}
AL*
S*
Beziehungshierarchie R ⊑ S HH
inverse Beziehung R-1 II
Qualifizierte Zahlenrestriktion (≤nR.C) (≥nR.C) QQ
Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
30
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.3 ALC - Syntax und Semantik
Beschreibungslogiken •ALC: Attribute Language with Complement
• S: ALC + Rollentransitivität
•H: Subrollenbeziehung
•O: abgeschlossene Klassen
• I: inverse Rollen
•N: Zahlenrestriktionen ≤n R etc.
•Q: Qualifizierende Zahlenrestriktionen ≤n R.C etc.
• (D): Datentypen
•F: Funktionale Rollen
•OWL DL ist SHOIN(D)
•OWL Lite ist SHIF(D)
3.4 Beschreibungslogiken
3.4.1 Motivation
3.4.2 Beschreibungslogiken Überblick
3.4.3 ALC - Syntax und Semantik
3.4.4 Inferenz und Reasoning
3.4.5 Tableaux-Verfahren
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
31
3. Wissensrepräsentationen3.4 Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
32
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Open World vs Closed World Assumption• OWA: Open World Assumption
Die Existenz von weiteren Individuen ist möglich, sofern sie nicht explizit ausgeschlossen wird.
• CWA: Closed World AssumptionEs wird angenommen, dass die Wissensbasis alle Individuen enthält.
if we assume that we know everything about Bill then all of his children are male
child(Bill,Bob)Man(Bob)
are all childrenof Bill male?
? ⊨ ∀child.Man(Bill)
no idea sincewe do not knowall children of Bill
DL answersdon‘t know
PROLOG answersyes
≤ 1 child.⊤(Bill) ? ⊨ ∀child.Man(Bill) yesnow we knoweverything aboutBill‘s children
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
33
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Wichtige Inferenzprobleme I
• Globale Konsistenz der Wissensbasis KB ⊨ false?• ist Wissensbasis sinnvoll?
• Klassenkonsistenz C ≡ ┴ ?
• Muss Klasse C leer sein?
• Klasseninklusion (Subsumption) C ⊑ D?• Strukturierung der Wissensbasis
• Klassenäquivalenz C ≡ D?• Sind zwei Klassen eigentlich dieselbe?
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
34
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Wichtige Inferenzprobleme II
• Klassendisjunktheit C ⊓ D = ┴?• Sind zwei Klassen disjunkt?
• Klassenzugehörigkeit C(a)?• Ist Individuum a in der Klasse C?
• Instanzgenerierung (Retrieval) „alle x mit C(x) finden“
• Finde alle (bekannten!) Individuen zur Klasse C.
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
35
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Entscheidbarkeit und DLs
• Entscheidbarkeit: zu jedem Inferenzproblem gibt es einen immer terminierenden Algorithmus
• DLs sind Fragment von FOL, also könnten (im Prinzip) FOL-Inferenzalgorithmen (Resolution, Tableaux) verwendet werden.
• Diese terminieren aber nicht immer!
• Problem: Finde immer terminierende Algorithmen!
• Keine „naiven“ Lösungen in Sicht!
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
36
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Entscheidbarkeit und OWL DL
• Tableaux- und Resolutionsverfahren müssen für DLs abgewandelt werden
• Wir werden uns (zuerst) auf ALC beschränken
• Tableaux- und Resolutionsverfahren zeigen Unerfüllbarkeit einer Theorie
• Rückführung der Inferenzprobleme auf das Finden von Inkonsistenzen in der Wissensbasis, d.h. zeigen der Unerfüllbarkeit der Wissensbasis!
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
37
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Rückführung der Inferenz auf Erfüllbarkeit / Konsistenz I
• Klassenkonsistenz C ≡ ┴ gdw
• KB ⊔ {C(a)} unerfüllbar (a neu)
• Klasseninklusion (Subsumption) C ⊑ D gdw
• KB ⊔ {(C ⊓ ¬D)(a)} unerfüllbar (a neu)
• Klassenäquivalenz C ≡ D gdw• C ⊑ D und D ⊑ C
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
38
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.4 Inferenz und Reasoning
Rückführung der Inferenz auf Erfüllbarkeit / Konsistenz II
• Klassendisjunktheit C ⊓ D = ┴ gdw• KB ⊔ {(C ⊓ D)(a)} unerfüllbar (a neu)
• Klassenzugehörigkeit C(a) gdw• KB ⊔ {¬C(a)} unerfüllbar
• Instanzgenerierung (Retrieval) alle C(X) finden
• Prüfe Klassenzugehörigkeit für alle Individuen.
• Effiziente Implementation problematisch….
3.4 Beschreibungslogiken
3.4.1 Motivation
3.4.2 Beschreibungslogiken Überblick
3.4.3 ALC - Syntax und Semantik
3.4.4 Inferenz und Reasoning
3.4.5 Tableaux-Verfahren
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
39
3. Wissensrepräsentationen3.4 Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
40
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Verfahren in der Aussagenlogik (PL)• syntaktisches Verfahren zum Prüfen der Konsistenz logischer Ausdrücke
• Grundidee (ähnlich Resolution):
• Beweisverfahren, mit dem eine Formel dadurch bewiesen wird, dass ihre Negation als widersprüchlich abgeleitet wird (proof by refutation).
• Tableaux basieren auf einer Darstellung von Formeln in disjunktiver Normalform (Resolution: konjunktive Normalform)
• Konstruiere Baum, in dem jeder Knoten mit einer Formel markiert ist. Ein Pfad von der Wurzel zu einem Blatt stellt die Konjunktion aller Formeln der Knoten entlang des Pfads dar; eine Verzweigung stellt eine Disjunktion dar.
• Der Baum wird durch sukzessive Anwendung der Tableaux-Erweiterungsregeln aufgebaut.
• Ein Pfad in einem Tableaux ist abgeschlossen, wenn entlang des Pfads sowohl X wie ¬X für eine Formel X auftreten, oder wenn F auftritt (X muss nicht atomar sein.).
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
41
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Verfahren in der Aussagenlogik (PL)• Grundidee (Fortsetzung):
• Ein Tableaux heißt abgeschlossen, wenn alle seine Pfade abgeschlossen sind.
• Ein Tableaux-Beweis für eine Formel X ist ein abgeschlossenes Tableaux für ¬X.
• Die Auswahl der Regeln bei der Erweiterung eines Tableaus ist nichtdeterministisch.
• Für aussagenlogische Tableaux kann die Auswahl etwas eingeschränkt werden
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
42
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Erweiterungsregeln• für Aussagenlogik:
• für konjunktive Formeln (α-Regeln):
• für disjunktive Formeln (β-Regeln):
¬¬XX
¬WF
¬FW
α α1α2
X∧YXY
¬(X∨Y)¬X¬Y
¬(X⇒Y)X
¬Y
β β1 | β2
X∨YX | Y
¬(X∧Y)¬X | ¬Y
(X⇒Y)¬X | Y
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
43
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Beispiel(1):zu zeigen: ((q ∧ r) ⇒ (¬q ∨ r))
(1) ¬((q ∧ r) ⇒ (¬q ∨ r))
(2) α,1: (q ∧ r)
(3) α,1: ¬(¬q ∨ r)
(4) α,2: q
(5) α,2: r
(6) α,3: ¬ ¬q
(7) α,3: ¬r
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
44
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Beispiel(2):zu zeigen : (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r))
(10|β aus 9) ¬q | (11|β aus 9) r
(12|β aus 4) ¬p | (13|β aus 4) q
(1) ¬((p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r)))
(2|α aus 1) (p ⇒ (q ⇒ r))
(3|α aus 1) ¬((p ⇒ q) ⇒ (p ⇒ r))
(4|α aus 3) (p ⇒ q)
(5|α aus 3) ¬(p ⇒ r)
(6|α aus 5) p
(7|α aus 5) ¬r
(8|β aus 2) ¬p | (9|β aus 2) (q ⇒ r)
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
45
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Erweiterungsregeln für FOL• wie für Aussagenlogik - in den Regeln stehen X und Y dann für beliebige (prädikatenlogische) Formeln:
• Zusätzlich folgende Regeln für die Behandlung quantifizierter Formeln :
• für γ universell quantifizierte Formel, δ existenziell quantifizierte Formel, mit:
• t ist Grundterm (d.h. enthält keine in Φ gebundenen Variablen), c ist eine „neue“ Konstante
γ γ[t]
δ δ[c]
γ γ[t]
∀x.Φ Φ[x←t]
¬∃x.Φ ¬Φ[x←t]
δ δ[c]
∃x.Φ Φ[x←c]
¬∀x.Φ ¬Φ[x←c]
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
46
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Beispiel(3):zu zeigen: (∀x.P(x)∨Q(x)) ⇒ (∃x.P(x))∨(∀x.Q(x))
(9|β aus 8) P(c) | (10|β aus 8) Q(c)
(1) ¬((∀x.P(x)∨Q(x)) ⇒ (∃x.P(x))∨(∀x.Q(x)))
(2|α aus 1) (∀x.P(x)∨Q(x))
(3|α aus 1) ¬((∃x.P(x))∨(∀x.Q(x)))
(4|α aus 3) ¬(∃x.P(x))
(5|α aus 3) ¬(∀x.Q(x))
(6|δ aus 5) ¬Q(c)
(7|γ aus 4) ¬P(c)
(8|γ aus 2) P(c)∨Q(c)
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
47
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Transformation in Negationsnormalform•Gegeben eine Wissensbasis W.
•Ersetze C ≡ D durch C ⊑ D und D ⊑ C
•Ersetze C ⊑ D durch ¬C ⊔ D.
•Wende die NNF-Transformationen auf der nächsten Seite an
•Resultierende Wissensbasis: NNF(W)
•Negationsnormalform von W.
•Negation steht nur noch direkt vor atomaren Klassen
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
48
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Transformation in Negationsnormalform• NNF Transformationen
• W und NNF(W) sind logisch äquivalent.
NNF(C) = C, falls C atomar istNNF(¬C) = ¬C, falls C atomar istNNF(¬¬C) = NNF(C)NNF(C ⊔ D) = NNF(C) ⊔ NNF(D)NNF(C ⊓ D) = NNF(C) ⊓ NNF(D)NNF(¬(C ⊔ D)) = NNF(¬C) ⊓ NNF(¬D)NNF(¬(C ⊓ D)) = NNF(¬C) ⊔ NNF(¬D)NNF(∀R.C) = ∀ R.NNF(C)NNF(∃R.C) = ∃ R.NNF(C)NNF(¬∀R.C) = ∃R.NNF(¬C)NNF(¬∃R.C) = ∀R.NNF(¬C)
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
49
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Transformation in Negationsnormalform• Beispiel: P ⊑ (E ⊓ U) ⊔ ¬(¬E ⊔ D)
• In NNF: ¬P ⊔ (E ⊓ U) ⊔ (E ⊓ ¬D).
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
50
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Erweiterungsregeln für OWL DL
• Ist das resultierende Tableaux abgeschlossen, so ist die ursprüngliche Wissensbasis unerfüllbar.
• Man wählt dabei immer nur solche Elemente aus, die auch wirklich zu neuen Elementen im Tableaux führen. Ist dies nicht möglich, so terminiert der Algorithmus und die Wissensbasis ist erfüllbar.
Auswahl AktionC(a)∈W (ABox) Füge C(a) hinzu
R(a,b)∈W (ABox) Füge R(a,b) hinzu
C∈W (TBox) Füge C(a) für ein bekanntes Individuum a hinzu
(C⊓D)(a)∈A Füge C(a) und D(a) hinzu
(C⊔D)(a)∈A Splitte den Zweig. Füge zu (1) C(a) und zu (2) D(a) hinzu
(∃R.C)(a)∈A Füge R(a,b) und C(b) für neues Individuum b hinzu
(∀R.C)(a)∈A Falls R(a,b)∈A, dann füge C(b) hinzu
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
51
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Beispiel:• P … Professor
• E … Person
• U … Universitätsangehöriger
• D … Doktorand
• Wissensbasis: P ⊑ (E ⊓ U) ⊔ (E ⊓ ¬D)
• Ist P ⊑ E logische Konsequenz?
• Wissensbasis (mit Anfrage) in NNF:{¬P⊔ (E ⊓ U) ⊔ (E ⊓ ¬D), (P ⊓ ¬E)(a)}
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
52
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Beispiel (Fortsetzung):• TBox: ¬P ⊔ (E ⊓ U) ⊔ (E ⊓ ¬D)
• Tableaux:
(1) (P ⊓ ¬E)(a) (aus Wissensbasis)
(2|α aus 1) P(a)
(3|α aus 1) ¬E(a)
(4) (¬P ⊔ (E ⊓ U) ⊔ (E ⊓ ¬D))(a) (aus Wissensbasis)
(5) ¬P(a) | (6) ((E ⊓ U) ⊔ (E ⊓ ¬D))(a)
(7) (E ⊓ U)(a) | (8) (E ⊓ ¬D)(a)
(9) E(a) (10) E(a)
(11) U(a) (12) ¬D(a)
Die Wissensbasis ist unerfüllbar, d.h. P ⊑ E.
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
53
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
• Wissensbasis: ¬Person ⊔ ∃hasParent.Person
• abzuleiten: ¬Person(Bill)
Person(Bill)
(¬Person ⊔ ∃hasParent.Person)(Bill)
(¬Person ⊔ ∃hasParent.Person)(x1)
(¬Person ⊔ ∃hasParent.Person)(x2)
¬Person(Bill) ⊔∃hasParent.Person(Bill)
hasParent(Bill,x1)
Person(x1)∃
¬Person(x1) ∃hasParent.Person(x1) ⊔
hasParent(x1,x2)
Person(x2)∃
¬Person(x2) ∃hasParent.Person(x2) ⊔
Problem tritt bei Existenzquantoren aufbzw. bei OWL:minCardinality
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
54
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Idee des Blocking• wir hatten folgendes konstruiert:
• Idee: Wiederverwendung alter Knoten
Person∃hasParent.Person
Person∃hasParent.Person
Person∃hasParent.Person
hasParent hasParent hasParent
Person∃hasParent.Person
hasParent
Person∃hasParent.Person
Blocking
Korrektheit muss natürlichbewiesen werden...hasParent
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
55
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
• Wissensbasis: ¬Person ⊔ ∃hasParent.Person
• abzuleiten: ¬Person(Bill)
Person(Bill)
(¬Person ⊔ ∃hasParent.Person)(Bill)
¬Person(Bill)
hasParent(Bill,x1)
Person(x1)
⊔
∃
(¬Person ⊔ ∃hasParent.Person)(x1)
¬Person(x1) ∃hasParent.Person(x1)
∃hasParent.Person(Bill)
⊔
σ(Βill) = {Person, ¬Person ⊔ ∃hasParent.Person, ∃hasParent.Person}σ(x1) = { Person, ¬Person ⊔ ∃hasParent.Person, ∃hasParent.Person }σ(x1) ⊆ σ(Bill), so Bill blocks x1
Person∃hasParent.Person
hasParent
hasParent
Person∃hasParent.Person
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
56
3. Wissensrepräsentationen3.4 Beschreibungslogiken / 3.4.5 Tableaux-Verfahren
Tableaux Blocking Definition• Die Auswahl von (∃R.C)(a) im Tableauzweig A ist blockiert,
falls es ein Individuum b gibt, so dass {C | C(a) ∈ A} ⊆ {C | C(b) ∈ A} ist.
• Zwei Möglichkeiten der Terminierung:1.Abschluss des Tableaus.Dann Wissensbasis unerfüllbar.
2.Keine ungeblockte Auswahl führt zu Erweiterung.Dann Wissensbasis erfüllbar.
3.4 Beschreibungslogiken
3.4.1 Motivation
3.4.2 Beschreibungslogiken Überblick
3.4.3 ALC - Syntax und Semantik
3.4.4 Inferenz und Reasoning
3.4.5 Tableaux-Verfahren
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
57
3. Wissensrepräsentationen3.4 Beschreibungslogiken
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
585.01.2010 – Vorlesung Nr. 81 2 3 4 5 6 7 9 1110 12
13
3. Wissensrepräsentation und LogikDie Sprachen des Semantic Web - Teil 2
3.1.Ontologien in der Philosophie und der Informatik
3.2.Wiederholung Aussagenlogik und Prädikatenlogik
3.3.RDFS-Semantik
3.4.Beschreibungslogiken
3.5.OWL und OWL-Semantik
3.6.Regeln mit RIF/SWRL
14
Semantic Web - Vorlesungsinhalt
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
Semantic Web Architektur59
URI / IRI
XML / XSDData Interchange: RDF
RDFS
Ontology: OWL Rule: RIF
Query:SPARQL
Proof
Unifying Logic
Cry
pto
Trust
Interface & Application
Ontology-Level
3. Wissensrepräsentation und Logik
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
60
Semantic Web
OWL
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
61
Literatur
»P. Hitzler, M. Krötzsch, S. Rudolph, Y. Sure Semantic Web Grundlagen, Springer, 2008.
»F. Baader, D. McGuinness, D. Nardi, P. Patel-Schneider (eds.)The Description Logic Handbook - Theory, Implementation, and Application, 2001.(siehe online-Materialien)
3. Wissensrepräsentation und Logik
Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam
62
Literatur
•Bloghttp://sewe0910.blogspot.com/
•Materialien-Webseitehttp://www.hpi.uni-potsdam.de/meinel/teaching/lectures_classes/semanticweb_ws0910.html
•bibsonomy - Bookmarkshttp://www.bibsonomy.org/user/lysander07/sw0910_08
2. Semantic Web Basisarchitektur
Besten Dank auch an Pascal Hitzler, Sebastian Rudolph und Markus Krötzsch für die Vorlesungsunterlagen auf semantic-web-grundlagen.de