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

2

Gliederung

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

Oliver Gries

Einführung

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

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

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

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

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

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)

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)

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)

Jens Wächter

Prover und Expressions

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

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

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

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)

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

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

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)

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

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

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

Felix Lindner

Reasoning Services

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

22

Reasoning Services

23

Reasoning Services

24

Reasoning Services

25

Reasoning Services

26

Reasoning Services

27

Reasoning Services

28

Reasoning Services

Vorverarbeitung•evtl. Normalisierung der beschreibungslogischen

Ausdrücke•evtl. T-Box Expansion

29

Reasoning Services

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)

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)

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

33

Reasoning Services

34

Reasoning Services

Arved Solth

Optimierungen

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

36

Optimierungen

• Semantic Branching

• Simplification

• Normalisierung

• Dependency Directed Backtracking

37

Semantic Branching

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

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

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

40

Semantic Branching

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

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

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

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

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

45

Simplification

46

Simplification

• Motivation: Versucht, Verzweigungen vor ihrer Expansion zu vereinfachen

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;

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;

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

50

Simplification

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

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!

52

Simplification

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

T: ¬A

T: (A ν B)

F: A

T: BT: A

53

Simplification

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

T: ¬A

T: (A ν B)

F: A

T: B

54

Normalisierung und Unique Expressions

55

Normalisierung und Unique Expressions

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

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,

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;

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

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

60

Normalisierung und Unique Expressions

• Regeln zur lexikalischen Vereinfachung:

• Regeln zur Normalisierung:

1.

2.

3.

4.

5.

6.

7.

8.

9.

10.

11.

61

Normalisierung und Unique Expressions

• Vor Normalisierung:

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

• Nach Normalisierung:

• (¬ TOP)

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:

Niels Beuck

Dependency Directed Backtracking

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

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

65

Lösung

•Überflüssige Zweige streichen!

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

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.

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.

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

Roland Illig

Testumgebung und erste Ergebnisse

Reasoning-Services: Tableau-Beweiser für Beschreibungslogiken

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

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

72

Erste Ergebnisse

TODO