Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels...

72
Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens Wächter Projekt im Hauptstudium Wintersemester 2006/07 Carola Eschenbach Özgür Özçep

Transcript of Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels...

Page 1: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Reasoning Services: Tableau-Beweiser für Beschreibungslogiken– ein Zwischenbericht –

Niels Beuck Oliver GriesRoland Illig

Felix LindnerArved Solth

Jens Wächter

Projekt im HauptstudiumWintersemester 2006/07

Carola EschenbachÖzgür Özçep

Page 2: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

2

Gliederung

•Einleitung (Oliver)•Expressions und Prover (Jens)•Reasoning Services (Felix)•Optimierungen (Arved)•Dependency directed backtracking (Niels)•Testumgebung und Ergebnisse (Roland)

Page 3: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Oliver Gries

Einführung

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

Page 4: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

4

A ∩ (A→B) ∩ ¬B

A

(A→B)

¬B

¬A B

Tableau-Beweiser

•Verfahren zur Erkennung von logischen Widersprüchen•Eine Formel gilt nach dem Tableau-Verfahren als

unerfüllbar, wenn alle Zweige widersprüchlich sind

Page 5: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

5

Beschreibungslogiken

•DL (Description Logic)•sind ein (meist) entscheidbares Fragment der Prädikatenlogik•Sprache besteht aus Konzepten, Konstanten und Rollen

•Beispiele für die Ausdrucksmächtigkeit:

o „Alle Menschen sind Lebewesen.“o „Harry hat nur Töchter.“ o „Ein Stuhl ist ein Möbelstück mit vier Beinen.“

Beschreibungslogiken (Axiome)•C D⊆ Konzept C wird von Konzept D subsummiert•C ≡ D Äquivalenz von C und D•C(a) a ist Instanz von Konzept C•R(a, b) a steht mit b in Relation R

Page 6: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

6

TBox ABoxWoman ≡ Person ∩ FemaleMan ≡ Person ∩ ¬WomanMother ≡ Woman ∩ ∃hasChild.PersonFather ≡ Man ∩ ∃hasChild.PersonParent ≡ Mother ∪ FatherGrandmother ≡ Mother ∩ ∃hasChild.ParentWife ≡ Woman ∩ ∃hasHusband.ManMotherWithManyChildren ≡ Mother ∩ ≥3 hasChild

MotherWithoutDaughter ≡ Mother ∩

∀hasChild.¬Woman

MotherWithoutDaughter(MARY)Father(PETER)hasChild(MARY, PETER)hasChild(MARY, PAUL)hasChild(PETER, HARRY)

example Inference:Grandmother(MARY).

Woman(MARY), Man(MARY) ergibt Inkonsistenz

Beschreibungslogiken:TBox, ABox und Inferenzen

Page 7: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

7

Reasoning-Services

TBox•Satisfiability – Ist ein Konzept erfüllbar ?•Subsumption – gilt C D für alle Belegungen ?⊆•Equivalence – gilt C ≡ D für alle Belegungen ?•Disjointness – sind C und D disjunkt ?•Classification – erstelle eine Taxonomie

(Subsumptionshierarchie) aller Konzepte

ABox + TBox•InstanceCheck – gilt C(a) ?•Retrieval – nenne alle Instanzen eines Konzeptes•Realization – nenne speziellste Konzepte einer

Instanz

Page 8: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

8

Inhalte des Projekts

Sprache•Wir haben die Sprache ALC gewählt. Sie enthält (im

Wesentlichen) die Konzeptkonstruktoren AND, OR, NOT, R.C ∃und R.C∀

Tableau-Beweiser•Unser Beweiser benutzt markierte Tableaux. Sie lassen sich

leichter implementieren, eine NNF muss nicht erstellt werden und es können auch nicht atomare Abschlüsse gefunden werden

Reasoning-Services•Wir haben den (TBox-)Satisfiability, Subsumption, Equivalence

und Disjointness-Service implementiert (InstanceCheck, Retrieval folgen)

Page 9: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

9

T ((∃R.A) ∩ (∃R.B) ∩ ¬(∃R.(A ∩ B))) (a)

T (∃R.A) (a)

T (∃R.B) (a)

T ¬(∃R.(A ∩ B)) (a)

T R(a,b), T A(b)

T R(a,c), T B(c)

F (∃R.(A ∩ B)) (a)

F (A ∩ B) (b), F (A ∩ B) (c)

F A(b) F B(b)

F A(c) F B(c)

Markiertes Tableau (Beispiel für die Sprache ALC)

Page 10: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

10

Phasen des Projektes

theoretische Grundlagen•Aufsatz von Ian Horrocks über (markierte) Tableaux•Kapitel 2 aus dem „Description Logics Handbook“

Erweiteurng des AL-Beweisers zu einem DL-Beweiser mit Reasoning-Services•Gruppe Parser•Gruppe Prover (Jens Wächter) •Gruppe Reasoning Services (Felix Lindner)

Optimierungen und Testumgebung•Optimierungen: Normalisierung der Konzepte, Semantic

Branching, Simplification (Arved Solth)•Dependancy Directed Backtracking-Optimierung (Niels Beuck)•Testumgebung mit ersten Ergebnissen (Roland Illig)

Page 11: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Jens Wächter

Prover und Expressions

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

Page 12: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

12

Expressions

•Frühe Grundsatzentscheidung : Orientierung an LISP •Eine Klasse, die alle Ausdrücke abdeckt statt individuelle

Klassen für jeden Ausdruck•Klasse ‚DLExpression‘ enthält Operator, Name,

Subkonzepte•Wir unterscheiden zwischen atomaren und nicht atomaren

Konzepten•Beispiel : (all R C) :

op = DLOperator.All

subexpressions[0] = R

subexpressions[1] = C

name = null

Page 13: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

13

Übersicht über den Prover

Prover

Expansionsregeln

Expansion

Tableau

Zweig

Eintrag

besitzt

benutzt

erstellt

erzeugt/

wird erzeugt

besteht aus

besteht aus

wird angewendet auf

für

Page 14: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

14

Tableau - Eintrag

•Ein Tableaueintrag(TEntry) besteht aus einem Ausdruck, einer Markierung und einer Konstante, auf die sich der Ausdruck bezieht

•T:(all R C)(x)•F:R(x, y)

Page 15: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

15

T:(and a b)(x)

T:a(x)

T:b(x)

Tableau-Zweig

•Das Tableau wird nicht als Baumstruktur sondern als Liste realisiert

•Der Tableauzweig(TBranch) unterteilt dabei die Liste der Einträge in Teillisten von expandierten, nicht expandierten und atomaren Einträgen

•Die Abschlussbedingungen von Zweigen werden ebenfalls in TBranch geprüft. Standard : atomarer Abschluss, optional : nicht atomarer

Page 16: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

16

T:(or a b)(x)

T:a(x)

T:(or a b)(x)

T:b(x)

aktiver Zweig

Tableau - Tableau

•reine Datenstruktur aus Zweigen und statistischen Daten•es gibt einen aktiven Zweig•aktueller Zweig lässt sich ersetzen durch Menge an neuen

Zweigen

Page 17: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

17

Prover

•Der Prover stellt den Reasoning Services Methoden zum Erfüllbarkeitstest bereit

•Der Prover steuert die Expansion der Tableaustruktur •Dazu benutzt er einen Satz an Expansionsregeln, die

priorisiert werden können•Ablauf des Beweisvorgangs : für aktuellen Tableauzweig

wird die Anwendbarkeit der Regeln für jeden Eintrag getestet. Wenn eine Regel auf einen Eintrag angewendet werden kann, dann wird eine Expansion erstellt und diese auf den aktuellen Tableauzweig angewendet.

•Mit dem resultierendem Zweig wird fortgefahren (Tiefensuche)

Page 18: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

18

T: (and (all R D) (some R C))(x)

T: (all R D)(x) (1)

T: (some R C)(x) (1)

T: R(x, y) (2)

T: C(y) (2)

T: D(y) (3)

T: (some R C)(x)

T: R(x, y)

T: C(y)

T: (all R D)(x)

T: R(x, y)

T: D(y)

Expansionsregeln

•In Expansionsregeln wird spezifiziert, wenn diese angewendet werden können

•Expansionsregeln erstellen Expansionen •Problem bei Regeln mit mehr als einer Vorbedingung

Page 19: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

19

Expansionen

•resultieren aus der Anwendung einer Expansionsregel auf einen Eintrag

•enthalten „Anleitung“ wie ein Zweig der Regel entsprechend umgeformt werden muss, bzw. neue Zweige erstellt werden müssen

•Anwendung von Expansion auf Zweig setzt Eintrag, auf den die Regel angewendet wurde, auf Liste von bereits expandierten Einträge

Page 20: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

20

T: (all R C)(x)

T: R(x, y)

T: C(y)

Sonderfall Allquantorexpansion

•Mehrere Vorbedingungen - Expansionsregel prüft, ob Eintrag der Form (all R C) ist

•Als Expansion wird ein „Muster“ erstellt, wie das Ergebnis aussehen könnte

•Für jede Relation, die ins Muster passt, wird bei Anwendung der Expansionsregel in resultierendem Zweig ein Konzept erstellt : test der anderen Vorbedingungen in Expansion

•Dieses Verfahren lässt sich bei Simplification nicht benutzen

Page 21: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Felix Lindner

Reasoning Services

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

Page 22: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

22

Reasoning Services

Page 23: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

23

Reasoning Services

Page 24: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

24

Reasoning Services

Page 25: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

25

Reasoning Services

Page 26: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

26

Reasoning Services

Page 27: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

27

Reasoning Services

Page 28: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

28

Reasoning Services

Vorverarbeitung•evtl. Normalisierung der beschreibungslogischen

Ausdrücke•evtl. T-Box Expansion

Page 29: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

29

Reasoning Services

Page 30: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

30

Bei Abschluss: unerfüllbar

Reasoning Services

Initiale Tableaus

Konzept-ErfüllbarkeitT C(a)

Mit TBox•Expansion der TBox Axiome

Ai ≡ Di' ,Di' enthält nur Basissymbole

•Ersetzung aller Vorkommen von

Ai in C durch Di'

TBox-ErfüllbarkeitAi ≡ Ci

CTBox ≡ (¬Ai C∪ i) ∩ (Ai ∪¬Ci) ∩...

T CTBox (a)

Page 31: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

31

Reasoning Services

Initiale Tableaus

Subsumption•Wird C von D subsumiert?•Rückführung auf

Unerfüllbarkeit

T C(a)

F D(a)

•Bei Abschluss gilt Sumbsumptionsbeziehung

Äquivalenz•Konzepte C und D äquivalent?•Rückführung auf Subsumption

• Subsumiert(C,D)

und • Subsumiert(D, C)

Page 32: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

32

Reasoning Services

Initiale Tableaus

Disjunktheit•Sind C und D disjunkt?•Rückführung auf Unerfüllbarkeit

T C(a)

T D(a)

•Bei Abschluss gilt Disjunktheit

Page 33: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

33

Reasoning Services

Page 34: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

34

Reasoning Services

Page 35: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Arved Solth

Optimierungen

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

Page 36: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

36

Optimierungen

• Semantic Branching

• Simplification

• Normalisierung

• Dependency Directed Backtracking

Page 37: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

37

Semantic Branching

• Syntactic Branching: jedes Disjunkt einer Verzweigung führt zu einem einzelnen Zweig

Page 38: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

38

Semantic Branching

• Syntactic Branching: jedes Disjunkt einer Verzweigung führt zu einem einzelnen Zweig

• Semantic Branching: ein Disjunkt D aus einer unexpandierten Verzweigung führt zu zwei disjunkten Zweigen mit T:D und F:D

Page 39: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

39

Semantic Branching

• Syntactic Branching: jedes Disjunkt einer Verzweigung führt zu einem einzelnen Zweig

• Semantic Branching: ein Disjunkt D aus einer unexpandierten Verzweigung führt zu zwei disjunkten Zweigen mit T:D und F:D

• Vorteil: die beiden Zweige sind strikt disjunkt und können dadurch mehrfaches, unnötiges und redundantes Expandieren von weiteren Formeln verhindern, wie es bei Syntactic Branching vorkommen kann

Page 40: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

40

Semantic Branching

• Beispiel: Formel (A ν B) (A ν ¬B) X, einmal mit Syntactic Branching und einmal mit Semantic Branching expandiert

Page 41: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

41

Semantic Branching

• Beispiel: Formel (A ν B) (A ν ¬B) X, einmal mit Syntactic Branching und einmal mit Semantic Branching expandiert

• Annahme: Formel X enthält aufwendig zu expandierende, evtl. wieder verzweigende Teilformeln

Page 42: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

42

Semantic Branching

• Beispiel: Formel (A ν B) (A ν ¬B) X, einmal mit Syntactic Branching und einmal mit Semantic Branching expandiert

• Annahme: Formel X enthält aufwendig zu expandierende, evtl. wieder verzweigende Teilformeln

• Ziel: erforderliche Anzahl von Expansionen der Teilformel X reduzieren und redundante Expansionen vermeiden

Page 43: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

43

Semantic Branching

Mit Syntactic Branching:T: (A ν B) (A ν ¬B) X

T: A T: B

T: A T: ¬B

F: B F: B

T: A T: ¬B

X

X

X

T: (A ν B)

T: (A ν ¬B)

T: X

X muss 3mal expandiert werden

Page 44: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

44

Semantic Branching

Mit Semantic Branching:T: (A ν B) (A ν ¬B) X

T: A T: ¬A

T: ¬B

T: A F: A

T: ¬B X

T: A F: A

T: B

T: (A ν B)

T: (A ν ¬B)

T: X

X muss nur 1mal expandiert werden!F: B

Page 45: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

45

Simplification

Page 46: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

46

Simplification

• Motivation: Versucht, Verzweigungen vor ihrer Expansion zu vereinfachen

Page 47: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

47

Simplification

• Motivation: Versucht, Verzweigungen vor ihrer Expansion zu vereinfachen

• Vorgehen: – suche nach Einträgen im aktuellen Zweig, deren Ausdrücke durch

Regelanwendungen zu Verzweigungen führen können;

Page 48: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

48

Simplification

• Motivation: Versucht, Verzweigungen vor ihrer Expansion zu vereinfachen

• Vorgehen: – suche nach Einträgen im aktuellen Zweig, deren Ausdrücke durch

Regelanwendungen zu Verzweigungen führen können;

– durchsuche nun den Zweig nach allen Teilausdrücken einer solchen Verzweigung;

Page 49: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

49

Simplification

• Motivation: Versucht, Verzweigungen vor ihrer Expansion zu vereinfachen

• Vorgehen: – suche nach Einträgen im aktuellen Zweig, deren Ausdrücke durch

Regelanwendungen zu Verzweigungen führen können;

– durchsuche nun den Zweig nach allen Teilausdrücken einer solchen Verzweigung;

– falls ein Teilausdruck gefunden wurde und sich nur durch sein Label von dem Teilausdruck der Verzweigung unterscheidet, wird er aus dieser gestrichen

Page 50: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

50

Simplification

• Vorteil: Durch streichen dieser Teilformeln können Verzweigungen vereinfacht oder sogar vermieden werden

Page 51: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

51

Simplification

• Vorteil: Durch streichen dieser Teilformeln können Verzweigungen vereinfacht oder sogar vermieden werden

• Besonderheit: Optimierung muss nicht nur auf die zu bearbeitende Verzweigung sondern auch auf alle anderen Einträge im aktuellen Zweig zugreifen ähnliche Problematik wie bei All-Quantor-Operatoren!

Page 52: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

52

Simplification

Ohne Simplification:T: (A ν B) ¬A

T: ¬A

T: (A ν B)

F: A

T: BT: A

Page 53: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

53

Simplification

Mit Simplification:T: (A ν B) ¬A

T: ¬A

T: (A ν B)

F: A

T: B

Page 54: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

54

Normalisierung und Unique Expressions

Page 55: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

55

Normalisierung und Unique Expressions

• Motivation: Minimiert den Vergleichsaufwand zwischen Ausdrücken der Sprache

Page 56: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

56

Normalisierung und Unique Expressions

• Motivation: Minimiert den Vergleichsaufwand zwischen Ausdrücken der Sprache

• Vorgehen: – Normalisierung bringt alle Ausdrücke durch eine Menge von

Umformungsregeln in eine Normalform,

Page 57: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

57

Normalisierung und Unique Expressions

• Motivation: Minimiert den Vergleichsaufwand zwischen Ausdrücken der Sprache

• Vorgehen: – Normalisierung bringt alle Ausdrücke durch eine Menge von

Umformungsregeln in eine Normalform,

– Unique Expressions speichert von jeder solchen Formel in Normalform nur eine Instanz;

Page 58: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

58

Normalisierung und Unique Expressions

• Motivation: Minimiert den Vergleichsaufwand zwischen Ausdrücken der Sprache

• Vorgehen: – Normalisierung bringt alle Ausdrücke durch eine Menge von

Umformungsregeln in eine Normalform,

– Unique Expressions speichert von jeder solchen Formel in Normalform nur eine Instanz;

– diese Instanzen von Ausdrücken werden verglichen und auf Inkonsistenzen überprüft

Page 59: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

59

Normalisierung und Unique Expressions

• Motivation: Minimiert den Vergleichsaufwand zwischen Ausdrücken der Sprache

• Vorgehen: – Normalisierung bringt alle Ausdrücke durch eine Menge von

Umformungsregeln in eine Normalform,

– Unique Expressions speichert von jeder solchen Formel in Normalform nur eine Instanz;

– diese Instanzen von Ausdrücken werden verglichen und auf Inkonsistenzen überprüft

• Vorteil: Redundanzen werden vermieden und Inkonsistenzen schnell erkannt

Page 60: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

60

Normalisierung und Unique Expressions

• Regeln zur lexikalischen Vereinfachung:

• Regeln zur Normalisierung:

1.

2.

3.

4.

5.

6.

7.

8.

9.

10.

11.

Page 61: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

61

Normalisierung und Unique Expressions

• Vor Normalisierung:

• a b c d (f ¬({(a ¬BOTTOM)}))

• Nach Normalisierung:

• (¬ TOP)

Page 62: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

62

Normalisierung und Unique Expressions

a b c d (f ¬({(a ¬BOTTOM)}))

Ablauf:

a b c d (f ¬({(a ¬ ¬TOP )}))5.

a b c d (f ¬({(a TOP )}))8.

a b c d (f ¬( {{a, TOP }}))9.

a b c d (f ¬( {{a}}))2.

a b c d (f ¬( {a}))11.

a b c d (f ¬a)11.

a b c d ({f,¬a}))9.

{a, b, c, d, {f,¬a}}9.

{a, b, c, d, f,¬a}10.

(¬TOP)4.

Regel:

Page 63: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Niels Beuck

Dependency Directed Backtracking

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

Page 64: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

64

(and (or..) (or..) (or..) ..)

Das Problem

•Verzweigende Expansionen erzeugen exponentiell viele Zweige•Welche Einträge zum Konflikt führen weiß man erst, wenn man

sie expandiert hat•Trägt eine Verzweigung nicht zum Konflikt bei, muss in jedem

ihrer Zweige der selbe Konflikt neu gefunden werden

Page 65: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

65

Lösung

•Überflüssige Zweige streichen!

•Springe zurück zur letzten Verzweigung, die zum Konflikt beigetragen hat (Backjumping)

Page 66: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

66

I

II

III

T- (or C D) (a)[0,II]

T- C (a)[0,II,III]

T- D (a)[0,II,III]

III

Ergänzungen im Tableau

Zweige erweitern um Verzweigungspunkte•Jeder Zweig kennt die Verzweigung, an der

er entstanden ist •Verzweigungspunkte haben eine

Ordnungsrelation

Einträge erweitern um Dependency-Sets•Jeder Eintrag erbt seine Abhängigkeiten

von dem Eintrag (bzw. den Einträgen) aus dem er entstanden ist.

•Geht ein Eintrag aus einer verzweigenden Expansion hervor, erhält er zusätzlich eine Abhängigkeit vom neuen Verzweigungspunkt.

Page 67: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

67

[0,I, II]

I

II

III

beachte: Verzweigungspunkte

der Zweige sind monoton fallend

0

T C(a)[0,I]

F C(a)[0, II]

Backjumping

•Konflikt gefunden: Abhängigkeit des Konflikts ist die Vereinigung der Abhängigkeiten aller beteiligten Einträge

•Zweige, deren Verzweigungspunkt nicht in dieser Menge ist, werden übersprungen.

Page 68: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

68

[0,I, II]I

II

III

0

[0, II]

Abhängigkeiten einer Verzweigung

•Weitere Abhängigkeiten eines Konflikts werden unter dem aktuellen Verzweigungspunkt vermerkt.

•Wird hierher zurückgesprungen, wird diese Menge mit der aktuellen vereinigt.

•Wird er übersprungen, wird sie verworfen

Page 69: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

Roland Illig

Testumgebung und erste Ergebnisse

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

Page 70: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

70

Testumgebung und erste Ergebnisse

Ziele•Testen, ob die Optimierungen was gebracht haben, und wenn ja, wie viel

•Vergleich der einzelnen Optimierungen•Wiederholbarkeit der Tests•Zuverlässige Messungen

Page 71: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

71

Umsetzung

Globale Optionen, um die Optimierungen zu steuern•dlexpression.normalising•dlexpansionrulebool.semanticbranching•dlexpansionrulebool.simplification•prover.use_ddb•prover.verbose

Meßpunkte, um die Ausführung zu kontrollieren•DLExpression.subExpressions•tableau.expand•tableau.constants

Einfache Zeitmessung

Page 72: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken – ein Zwischenbericht – Niels Beuck Oliver Gries Roland Illig Felix Lindner Arved Solth Jens.

72

Erste Ergebnisse

TODO