06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

66
Vorlesung Dr. Harald Sack Hasso-Plattner-Institut für Softwaresystemtechnik Universität Potsdam Wintersemester 2011/12 Semantic Web Technologien Blog zur Vorlesung: http://wwwsoup2011.blogspot.com/ Donnerstag, 15. Dezember 11

description

Folien zur Vorlesung 'Beschreibungslogiken' (Description Logics) der Vorlesungsreihe 'Semantic Web Technologien' am Hasso-Plattner-Institut Potsdam, 29.11.2011

Transcript of 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Page 1: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

VorlesungDr. Harald Sack

Hasso-Plattner-Institut für SoftwaresystemtechnikUniversität Potsdam

Wintersemester 2011/12

Semantic Web Technologien

Blog zur Vorlesung: http://wwwsoup2011.blogspot.com/

Donnerstag, 15. Dezember 11

Page 2: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

2

Semantic Web Technologien Wiederholung

Aussa

genlog

ik &

Prädi

katen

logik

Semantic Web Technologien Wiederholung

Donnerstag, 15. Dezember 11

Page 3: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

1. Einführung 2. Semantic Web Basisarchitektur

Die Sprachen des Semantic Web - Teil 1

3. Wissensrepräsentation und LogikDie Sprachen des Semantic Web - Teil 2

4. Semantic Web Anwendungen

3

Semantic Web Technologien Vorlesungsinhalt

Donnerstag, 15. Dezember 11

Page 4: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

3. Wissensrepräsentation und LogikDie Sprachen des Semantic Web - Teil 2

3.1.Exkurs: Ontologien in Philosophie und Informatik

3.2.Wiederholung: Aussagenlogik und Prädikatenlogik

3.3.Beschreibungslogiken (Description Logics)3.4.RDF(S)-Semantik3.5.OWL und OWL-Semantik3.6.OWL 2 und Regeln

Semantic Web Technologien Vorlesungsinhalt

4

Donnerstag, 15. Dezember 11

Page 5: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

5

Beschr

eibung

s-

logike

n

Donnerstag, 15. Dezember 11

Page 6: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

6

3. Wissensrepräsentation und Logik3.3 Beschreibungslogiken

3.3 Beschreibungslogiken3.3.1 Motivation3.3.2 Beschreibungslogiken Überblick3.3.3 ALC - Syntax und Semantik3.3.4 Inferenz und Reasoning3.3.5 Tableau-Verfahren

Donnerstag, 15. Dezember 11

Page 7: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität PotsdamTurmbau zu Babel, Pieter Brueghel, 1563

7

An Ontology is aformal specification

of a sharedconceptualization

of a domain of interest

Tom Gruber, 1993

⇒ machine understandable⇒ group of people/agents⇒ about concepts⇒ between general description and individual use

Ontologien in der Informatik

Donnerstag, 15. Dezember 11

Page 8: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Ontologien und Kommunikation

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

8

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

Donnerstag, 15. Dezember 11

Page 9: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

9

RDF und RDFS• Definition von Klassen,

Klassenhierarchien,Relationen,Individuen

• zur DefinitioneinfacherOntologiengeeignet

• für komplexereModellierungaber nicht geeignet

ISBN 0-00-651409-X

WWW

2004

a:titel

a:jahr

Springer

Heidelberg

a:verlagname

a:verlagort

a:verlag

Harald Sack

http://hpi-web.de/HaraldSack.html

a:autorname

a:autorhomepage

a:autor

Donnerstag, 15. Dezember 11

Page 10: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

10

Wir benötigen ein ausdrucksstärkeresMittel zur Wissensrepräsentation

Beschr

eibung

s-

logike

n

Donnerstag, 15. Dezember 11

Page 11: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

11

3.3 Beschreibungslogiken3.3.1 Motivation3.3.2 Beschreibungslogiken Überblick3.3.3 ALC - Syntax und Semantik3.3.4 Inferenz und Reasoning3.3.5 Tableau-Verfahren

Donnerstag, 15. Dezember 11

Page 12: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

12logic-basedformalisms

Wissensrepräsentation

non logic-based formalisms

• näher an der menschlichen Intuition

• daher einfacher zu verstehen

• besitzen meist keine konsistente Semantik

• Bsp.:• Semantic Networks• Frame-basierte

Repräsentationen• Regel-basierte

Repräsentationen

• komplexer und schwieriger zu verstehen

• basieren alle Grundlage der Prädikatenlogik

• konsistente Semantik• FOL Syntax• FOL Semantik• FOL Deduktionsregeln

• Bsp.:• Beschreibungslogiken

Donnerstag, 15. Dezember 11

Page 13: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

FOLVorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

13

FOL als Semantic Web Sprache?

•Warum nicht einfach FOL für Ontologien hernehmen?•FOL kann alles...

•vergleiche höhere Programmiersprachen und Assembler

•FOL ist•sehr ausdrucksstark•deshalb unhandlich bei der Modellierung•daher auch schlecht geeignet, um einen Konsens bei

der Modellierung zu finden•beweistheoretisch sehr komplex (semi-entscheidbar)

•FOL ist keine Markupsprache

Suche ein geeignetes Fragment von FOL

Donnerstag, 15. Dezember 11

Page 14: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

14 • 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)

• DLs entwickelten sich aus „semantischen Netzwerken“• DLs sind meist entscheidbar• DLs sind vergleichsweise ausdrucksstark• DLs besitzen enge Verwandtschaft mit Modallogiken

• W3C Standard OWL 1 DL basiert auf der Beschreibungslogik SHOIN(D)

Beschreibungslogiken (DLs)

Donnerstag, 15. Dezember 11

Page 15: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

15

Allgemeine DL Architektur

Knowledge Base

TBox Terminological Knowledge Wissen über Konzepte einer Domäne (Klassen, Attribute, Eigenschaften,..)

EuroBook ≣ Book ⨅ PublishedInEurope

ABox Assertional Knowledge Wissen über Instanzen / Entitäten

EuroBook(“Semantic Web Grundlagen“)

Infe

renc

e E

ngin

e

Inte

rface

Donnerstag, 15. Dezember 11

Page 16: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

16 •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 (deduktiv) abgeschlossen ist

•Konjunktion, Disjunktion, Negation sind Klassenkonstruktoren, geschrieben ⊓, ⊔ , ¬

•Quantoren schränken Rollenbereiche ein:

Man ⊓ ∃hasChild.Female ⊓ ∃hasChild.Male ⊓ ∀hasChild.(Rich ⊔ Happy)

Allgemeiner DL Aufbau

Donnerstag, 15. Dezember 11

Page 17: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

17

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)

Donnerstag, 15. Dezember 11

Page 18: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

18 3.3 Beschreibungslogiken3.3.1 Motivation3.3.2 Beschreibungslogiken Überblick3.3.3 ALC - Syntax und Semantik3.3.4 Inferenz und Reasoning3.3.5 Tableau-Verfahren

Donnerstag, 15. Dezember 11

Page 19: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

19

ALC Grundbausteine

•Grundbausteine:•Klassen•Rollen•Individuen

•Student(Christian)Individuum Christian ist in Klasse Student

•Vorlesung(SemanticWebTechnologien)Individuum SemanticWebTechnologien ist eine Vorlesung

•nimmtTeilAn(Christian, SemanticWebTechnologien)Christian nimmt an der Vorlesung „Semantic Web Technologien“ teil

Donnerstag, 15. Dezember 11

Page 20: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

20

ALC Grundbausteine

• 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

Donnerstag, 15. Dezember 11

Page 21: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

21

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))

Donnerstag, 15. Dezember 11

Page 22: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

22 •Konjunktion ⊓

•Disjunktion ⊔

•Negation ¬

(∀x)(Professor(x) → ((Person(x) Λ Universitaetsangehoeriger(x)) V (Person(x) Λ ¬Student(x)))

Professor ⊑ (Person ⊓ Unversitaetsangehoeriger) ⊔ (Person ⊓ ¬Student)

ALC - komplexe Klassenbeziehungen

Donnerstag, 15. Dezember 11

Page 23: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

23

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 (der eine Person ist)

•(∀x)(Pruefung(x) → (∃y)(hatPruefer(x,y) Λ Person(y)))

Donnerstag, 15. Dezember 11

Page 24: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

24

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.

Donnerstag, 15. Dezember 11

Page 25: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

25

ALC - Semantik (Interpretation)•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 (Domäne) aus Individuen und•einer Interpretationsfunktion .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

Donnerstag, 15. Dezember 11

Page 26: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

26

ALC - Semantik (Interpretation)

Donnerstag, 15. Dezember 11

Page 27: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

27

ALC - Semantik (Interpretation)

•wird auf komplexe Klassen erweitert:

•⊤I = ΔI und ⊥I = ∅

•(C ⊔ D)I = CI ∪ DI und (C ⊓ D)I = CI ∩ DI

•(¬C)I = ΔI \ CI

•∀R.C = { a∈ΔI | (∀b∈ΔI) ( (a,b)∈RI → b∈CI )}

•∃R.C = { a∈ΔI | (∃b∈ΔI) ( (a,b)∈RI ∧ b∈CI )}

Donnerstag, 15. Dezember 11

Page 28: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

28

ALC - Semantik (Interpretation)

•...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

Donnerstag, 15. Dezember 11

Page 29: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

29

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.

Donnerstag, 15. Dezember 11

Page 30: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

30

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)

Donnerstag, 15. Dezember 11

Page 31: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

31

Beschreibungslogiken (Description Logics)

Operator/Construktor Syntax SpracheSprache

Konjunktion A ⊓ B

FLWertrestriktion ∀R.C FL

Existenzquantor ∃R

Top ⊤

Bottom ⊥

S*Negation ¬A

S*

Disjunktion A ⊔ B AL*

Existentielle Restriktion ∃R.C

Zahlenrestriktion (≤nR) (≥nR)

Menge von Individuen {a1,...,a2}

Beziehungshierarchie R ⊑ S HH

inverse Beziehung R-1 II

Qualifizierte Zahlenrestriktion (≤nR.C) (≥nR.C) QQ

Donnerstag, 15. Dezember 11

Page 32: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

32

Beschreibungslogiken (Description Logics)•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

•R: Rollenkonstruktoren

•OWL 1 DL ist SHOIN(D) / OWL 2 DL ist SHROIQ(D)

Donnerstag, 15. Dezember 11

Page 33: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

33 3.3 Beschreibungslogiken3.3.1 Motivation3.3.2 Beschreibungslogiken Überblick3.3.3 ALC - Syntax und Semantik3.3.4 Inferenz und Reasoning3.3.5 Tableau-Verfahren

Donnerstag, 15. Dezember 11

Page 34: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

34

Open World vs. Closed World Assumption

• OWA: Open World AssumptionDie 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

Donnerstag, 15. Dezember 11

Page 35: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

35

Inferenzprobleme und Beschreibungslogiken

• Sei D eine Terminologie (T-Box) und C und D Konzeptbeschreibungen in einer Sprache (Beschreibungslogik) L

• C ist erfüllbar bzgl. D genau dann, wenn es ein Modell I für D gibt, so dass gilt CI≠∅

anderenfalls ist C unerfüllbar bzgl. D

• C wird von D subsumiert bzgl. D, C ⊑D D bzw. D ⊨ C ⊑ D, genau dann, wenn für jedes Modell I von D gilt CI ⊆ DI

• C und D sind äquivalent bzgl. D, C ≣D D bzw. D ⊨ C ≣ D, genau dann, wenn für jedes Modell I von D gilt CI = DI

• C und D sind disjunkt bzgl. D, genau dann, wenn für jedes Modell I von D gilt CI ∩ DI = ∅

Donnerstag, 15. Dezember 11

Page 36: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

36

Inferenzprobleme und Beschreibungslogiken

• Sei D eine Terminologie (T-Box) und A eine Menge von Behauptungen (A-Box) in einer Sprache (Beschreibungslogik) L Sei α eine Behauptung, C eine Konzeptbeschreibung und a eine Konstante in L

• A ist konsistent bzgl. D genau dann, wenn es eine Interpretation I für L gibt, die gleichzeitig ein Modell für D und A ist

• a folgt aus A und D, A ∪ D ⊨ a, genau dann, für jede Interpretation I für L gilt, dass wenn I gleichzeitig ein Modell für D und A ist, das erfüllt I die Behauptung a

• a ist eine Instanz von C bzgl. D und A, genau dann, wenn A ∪ D ⊨ C(a)

Donnerstag, 15. Dezember 11

Page 37: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

37

Wichtige Inferenzprobleme (1)

• Globale (In)Konsistenz der Wissensbasis KB ⊨ ┴?

• ist Wissensbasis sinnvoll?

• Klassen(in)konsistenz C ≡ ┴ ?• Muss Klasse C leer sein?

• Klasseninklusion (Subsumption) C ⊑ D?• Strukturierung der Wissensbasis

• Klassenäquivalenz C ≡ D?• Sind zwei Klassen eigentlich dieselbe?

Donnerstag, 15. Dezember 11

Page 38: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

38

Wichtige Inferenzprobleme (2)

• Klassendisjunktheit C ⊓ D = ┴?• Sind zwei Klassen disjunkt?

• Klassenzugehörigkeit C(a)?• Ist Individuum a in der Klasse C enthalten?

• Instanzgenerierung (Retrieval) „alle x mit C(x) finden“• Finde alle (bekannten!) Individuen zur Klasse C.

Donnerstag, 15. Dezember 11

Page 39: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

39

Entscheidbarkeit und Beschreibungslogiken

• Entscheidbarkeit: zu jedem Inferenzproblem gibt es einen immer terminierenden Algorithmus• DLs sind Fragment von FOL, also könnten (im Prinzip)

FOL-Inferenzalgorithmen (Resolution, Tableau) verwendet werden.

• Diese terminieren aber nicht immer!

• Problem: Finde immer terminierende Algorithmen!• Keine „naiven“ Lösungen in Sicht!

Donnerstag, 15. Dezember 11

Page 40: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

40

Entscheidbarkeit und OWL DL

• FOL-Inferenzverfahren (Tableauverfahren und Resolution) müssen für DLs abgewandelt werden

• Wir werden uns auf ALC beschränken

• Tableau- 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!

Donnerstag, 15. Dezember 11

Page 41: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

41

Rückführung auf Unerfüllbarkeit (1)

(Reduction to Unsatisfiability)

• Klassen(in)konsistenz 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

Donnerstag, 15. Dezember 11

Page 42: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

42

Rückführung auf Unerfüllbarkeit (2)

• 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….

Donnerstag, 15. Dezember 11

Page 43: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

43 3.3 Beschreibungslogiken3.3.1 Motivation3.3.2 Beschreibungslogiken Überblick3.3.3 ALC - Syntax und Semantik3.3.4 Inferenz und Reasoning3.3.5 Tableau-Verfahren

Donnerstag, 15. Dezember 11

Page 44: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

44

Tableau 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).

•Tableau 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 Tableau-Erweiterungsregeln aufgebaut.

•Ein Pfad in einem Tableau 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.).

Donnerstag, 15. Dezember 11

Page 45: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

45

Tableau Verfahren in der Aussagenlogik (PL)

•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.

(q ∧ r) ∨ (p ∧ ¬ r) ∨ r

(q ∧ r) (p ∧ ¬ r) ∨ r

(p ∧ ¬ r) rq

r p

¬ r

Donnerstag, 15. Dezember 11

Page 46: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

46

Tableau Verfahren in der Aussagenlogik (PL)

•Grundidee (Fortsetzung):•Ein Tableau heißt abgeschlossen, wenn alle seine Pfade abgeschlossen sind.

•Ein Tableau-Beweis für eine Formel X ist ein abgeschlossenes Tableau für ¬X.

•Die Auswahl der Regeln bei der Erweiterung eines Tableaus ist nichtdeterministisch.

•Für aussagenlogische Tableau kann die Auswahl etwas eingeschränkt werden

Donnerstag, 15. Dezember 11

Page 47: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

•für Aussagenlogik:

•für konjunktive Formeln (α-Regeln):

•für disjunktive Formeln (β-Regeln):

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

47

Tableau Erweiterungsregeln

¬¬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

Donnerstag, 15. Dezember 11

Page 48: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

48

Tableauverfahren (PL) Beispiel (1):

zu zeigen: ((q ∧ r) ⇒ (¬q ∨ r))

(1) ¬((q ∧ r) ⇒ (¬q ∨ r)) = ¬(¬(q ∧ r) ∨ (¬q ∨ r)) = (q ∧ r) ∧ ¬(¬q ∨ r))

(2) α,1: (q ∧ r)

(3) α,1: ¬(¬q ∨ r) = q ∧ ¬r(4) α,2: q(5) α,2: r(6) α,3: q(7) α,3: ¬r

¬(X⇒Y)X

¬Y

α-Regel

Donnerstag, 15. Dezember 11

Page 49: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

49

Tableauverfahren (PL) Beispiel(2):

¬(X⇒Y)X

¬Y

α-Regel

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)

Donnerstag, 15. Dezember 11

Page 50: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

50

Tableauverfahren Erweiterung 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]

Donnerstag, 15. Dezember 11

Page 51: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

51zu 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)

γ γ[t]

∀x.Φ Φ[x←t]

¬∃x.Φ ¬Φ[x←t]

δ δ[c]

∃x.Φ Φ[x←c]

¬∀x.Φ ¬Φ[x←c]

Tableauverfahren (FOL) Beispiel(3):

Donnerstag, 15. Dezember 11

Page 52: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

52

Tableauverfahren für Beschreibungslogiken

•Transformation in Negationsnormalform notwendig

•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

Donnerstag, 15. Dezember 11

Page 53: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

53

Tableautransformation 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)

Donnerstag, 15. Dezember 11

Page 54: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

54

Tableautransformation in Negationsnormalform

• Beispiel: P ⊑ (E ⊓ U) ⊔ ¬(¬E ⊔ D)

• In NNF: ¬P ⊔ (E ⊓ U) ⊔ (E ⊓ ¬D).

Donnerstag, 15. Dezember 11

Page 55: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

55

Tableauerweiterungsregeln für DL

• Ist das resultierende Tableau 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 Tableau führen. Ist dies nicht möglich, so terminiert der Algorithmus und die Wissensbasis ist erfüllbar.

Auswahl Aktion

C(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

Donnerstag, 15. Dezember 11

Page 56: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

56

Tableauverfahren (DL) Beispiel(4):

• P … Professor• E … Person• U … Universitätsangehöriger• D … Doktorand

• Wissensbasis: P ⊑ (E ⊓ U) ⊔ (E ⊓ ¬D)• Ist P ⊑ E logische Konsequenz?

• Wissensbasis (mit [negierter] Anfrage) in NNF:{¬P⊔ (E ⊓ U) ⊔ (E ⊓ ¬D), (P ⊓ ¬E)(a)}

Donnerstag, 15. Dezember 11

Page 57: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

57

Tableauverfahren (DL) Beispiel(4):

• Wissensbasis: ¬P ⊔ (E ⊓ U) ⊔ (E ⊓ ¬D) (P ⊓ ¬E)(a)• Tableau:

(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)

Donnerstag, 15. Dezember 11

Page 58: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

58

Tableauverfahren (DL) Beispiel(5):

• 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

Donnerstag, 15. Dezember 11

Page 59: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

59

Idee des Blockings

• 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

Donnerstag, 15. Dezember 11

Page 60: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

60

Tableauverfahren (DL) mit Blocking

• 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

Donnerstag, 15. Dezember 11

Page 61: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

61 • Die Auswahl von (∃R.C)(a) im Tableauzweig A ist blockiert, falls es bereits 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 einer weiteren Erweiterung des Tableaus.Dann Wissensbasis erfüllbar.

Tableauverfahren (DL) mit Blocking

Donnerstag, 15. Dezember 11

Page 62: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

62

3. Wissensrepräsentation und Logik3.3 Beschreibungslogiken

3.3 Beschreibungslogiken3.3.1 Motivation3.3.2 Beschreibungslogiken Überblick3.3.3 ALC - Syntax und Semantik3.3.4 Inferenz und Reasoning3.3.5 Tableau-Verfahren

Donnerstag, 15. Dezember 11

Page 63: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

3. Wissensrepräsentation und LogikDie Sprachen des Semantic Web - Teil 2

3.1.Exkurs: Ontologien in Philosophie und Informatik

3.2.Wiederholung: Aussagenlogik und Prädikatenlogik

3.3.Beschreibungslogiken (Description Logics)3.4.RDF(S)-Semantik3.5.OWL und OWL-Semantik3.6.OWL 2 und Regeln

Semantic Web Technologien Vorlesungsinhalt

63

Donnerstag, 15. Dezember 11

Page 64: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

Formal

e Sema

ntik

für RD

F(S)

Rembrandt van Rijn, Die Anatomie des Dr. Tulp, 1632

64

die nächste Vorlesung....

Donnerstag, 15. Dezember 11

Page 66: 06 Beschreibungslogiken - Semantic Web Technologien WS 2011/12

Materialien

□Bloghttp://wwwsoup2011.blogspot.com/

□Webseitehttp://www.hpi.uni-potsdam.de/studium/lehrangebot/veranstaltung/semantic_web_technologien.html

□bibsonomy - Bookmarkshttp://www.bibsonomy.org/user/lysander07/swt1112_06

Vorlesung Semantic Web, Dr. Harald Sack, Hasso-Plattner-Institut, Universität Potsdam

66

3. Wissensrepräsentation und Logik3.3 Beschreibungslogiken

Donnerstag, 15. Dezember 11