Introduction To Description Logic

Automated Reasoning in Artificial Intelligence:Introduction to Description LogicSzymon Klarman(part of the content based on the tutorial by Stefan Schlobach)szymon.klarman@gmail.comVU University Amsterdam, 2009-2012

AR@AIIntroduction to Description LogicPlan for today Tableau algorithm for ALC with empty TBoxes Soundness, completeness, termination Reasoning w.r.t. non-empty TBoxesSzymon Klarman1 / 1

AR@AIIntroduction to Description LogicReasoning over DL knowledge basesThere are many different reasoning problems but we would stronglyprefer having one universal reasoner (generic problem solver).General strategy:1Choose one type of problems — ϕ — and design a reasoner forsolving it.2For any problem ψ, reduce ψ to ϕ, so that:answer to ψ? is YES answer to ϕ? is YES.3Solve ϕ using the reasoner and translate the answer adequately.Problem solver (DL reasoner):Tableau algorithm deciding consistency of the ABox w.r.t. the TBox.Szymon Klarman2 / 1

AR@AIIntroduction to Description LogicReasoning as model findingRecall that for K (T , A), we say that A is consistent w.r.t. T iffthere exists a model for A and T , i.e. an interpretation I ( I , ·I )satisfying all axioms in A and T .Note: this problem is also called deciding satisfiability of K.The most natural way of solving this problem is to. try to find amodel for A and T .Let’s try:Decide whether A is consistent w.r.t. T , where:T:A:Szymon KlarmanArtist created .Sculpture t painted .ArtworkPainting v Artwork u SculpturePainter v Artist u created .Paintingrembrandt : Painter(rembrandt, nightwatch) : created3 / 1

AR@AIIntroduction to Description LogicTableau algorithm: overviewTableau is a refutation proof system. It performs a search through thetree of possible models of the input. It succeeds (delivers a proof) iffthe input is inconsistent (there is no model).Input: ABox A: for now we assume T Procedure: Set A as the root of the tree. Apply tableau expansion rules to the formulas on the branches.(*) Rules add new assertions on a branch and/or create new branches. IF a branch contains a clash: {a : A, a : A} or {a : }THEN mark the branch as closed;ELSE continue expansion until no more rules apply.Output: IF all branches close RETURN: A is INCONSISTENT. IF there exists an open branch RETURN: A is CONSISTENT.Szymon Klarman4 / 1

AR@AIIntroduction to Description LogicNegation Normal FormTo reduce the number of tableau rules we can assume that all conceptsin the input appear in Negation Normal Form (NNF). A ( C) (C u D) (C t D) r.C r.C AC C t D C u D r. C r. CExample:NNF (A u r.((D u r.E) t C)) Szymon KlarmanA u r. ((D u r.E) t C)A u r.( (D u r.E) u C)A u r.(( D t r.E) u C)A u r.(( D t r. E) u C)5 / 1

AR@AIIntroduction to Description LogicTableau rulesA branch of a tableau is a set of ABox assertions. For any branch S,the following rules apply: u IF (a : C u D) S THEN S 0 : S {a : C, a : D} t IF (a : C t D) S THEN S 0 : S {a : C} or S 0 : S {a : D} IF (a : r.C) S THEN S 0 : S {(a, b) : r, b : C}where b is a ‘fresh’ individual name in S IF (a : r.C) S and (a, b) : r S THEN S 0 : S {b : C} IF {a : A, a : A} S or (a : ) S THEN mark the branch asCLOSEDNote: A rule should fire only once on a given match. The order in which the rules are applied is not determined in principle.We only assume “fairness”.Szymon Klarman6 / 1

AR@AIIntroduction to Description LogicExampleProblem:Is r.A u r.B subsumed by r.(A u B)?Reduction:Is ( r.A u r.B) u r.(A u B) unsatisfiable?Is A {a : r.A u r.B u r.(A u B)} inconsistent?Input:NNF (A) {a : r.A u r.B u r.( A t B)}Procedure:.compute a tableau proof for ASzymon Klarman7 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.Szymon Klarmana : r.A u r.B u r.( A t B)A8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)A( u : 1)( u : 1)( u : 1)8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.5.6.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:AA( u :( u :( u :( :( :1)1)1)2)2)8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.5.6.7.8.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:A(a, c) : rc:BA( u :( u :( u :( :( :( :( :1)1)1)2)2)3)3)8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.5.6.7.8.9.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:A(a, c) : rc:Bb : A t BA( u : 1)( u : 1)( u : 1)( : 2)( : 2)( : 3)( : 3)( : 4,5)8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.5.6.7.8.9.10.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:A(a, c) : rc:Bb : A t Bc : A t BA( u : 1)( u : 1)( u : 1)( : 2)( : 2)( : 3)( : 3)( : 4,5)( : 4,7)8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.5.6.7.8.9.10.11.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:A(a, c) : rc:Bb : A t Bc : A t Bb : A ( t : 9) (6, 11)12.b : BA( u : 1)( u : 1)( u : 1)( : 2)( : 2)( : 3)( : 3)( : 4,5)( : 4,7)( t : 9)8 / 1

AR@AIIntroduction to Description LogicExampleTableau proof:1.2.3.4.5.6.7.8.9.10.11.13.Szymon Klarmana : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:A(a, c) : rc:Bb : A t Bc : A t Bb : A ( t : 9) (6, 11)c : A ( t : 10)A( u : 1)( u : 1)( u : 1)( : 2)( : 2)( : 3)( : 3)( : 4,5)( : 4,7)12.b : B14.c : B ( t : 10) (8, 14)( t : 9)8 / 1

AR@AIIntroduction to Description LogicExample.there exists an open branch in the tableau, hence:Output:{a : r.A u r.B u r.( A t B)} is CONSISTENT( r.A u r.B) u ( r.(A u B)) is SATISFIABLE r.A u r.B is NOT SUBSUMED by r.(A u B)Can we be sure?Construct a canonical model I ( I , ·I ) of the ABox from the openbranch: use the individual names from the branch to define the domain, use the atomic assertions of the form a : A and (a, b) : r to definean interpretation of the vocabulary.Szymon Klarman9 / 1

AR@AIIntroduction to Description LogicExampleBrancha : r.A u r.B u r.( A t B)a : r.Aa : r.Ba : r.( A t B)(a, b) : rb:A(a, c) : rc:Bb : A t Bc : A t Bb : Bc : ACanonical model I {a, b, c}AI {b}B I {c}rI {(a, b), (a, c)}Clearly, I is a model of {a : r.A u r.B u r.( A t B)}.Szymon Klarman10 / 1

AR@AIIntroduction to Description LogicExercise: reasoningProblem: Is created.P ainting u created. subsumed by created.P ainting ?Szymon Klarman11 / 1

AR@AIIntroduction to Description LogicExercise: reasoningProblem: Is created.P ainting u created. subsumed by created.P ainting ?Input: {a : created.P ainting u created. u created. P ainting}Proof:1.2.3.4.5.6.7.8.a : created.P ainting u created. u created. P aintinga : created.P aintinga : created. a : created. P ainting(a, b) : createdb: b : P aintingb : P ainting (7, 8)A( u : 1)( u : 1)( u : 1)( : 3)( : 3)( : 2,5)( : 4,5)Output:Szymon Klarman11 / 1

AR@AIIntroduction to Description LogicExercise: reasoningProblem: Is created.P ainting u created. subsumed by created.P ainting ?Input: {a : created.P ainting u created. u created. P ainting}Proof:1.2.3.4.5.6.7.8.a : created.P ainting u created. u created. P aintinga : created.P aintinga : created. a : created. P ainting(a, b) : createdb: b : P aintingb : P ainting (7, 8)A( u : 1)( u : 1)( u : 1)( : 3)( : 3)( : 2,5)( : 4,5)Output: Yes, it is SUBSUMED.Szymon Klarman11 / 1

AR@AIIntroduction to Description LogicExercise: constructing canonical modelConstruct a canonical model for the following open branch:a : created.P aintinga : created. a : created. Sculpture(a, b) : createdb: b : P aintingb : SculptureSolution:Szymon Klarman12 / 1

AR@AIIntroduction to Description LogicExercise: constructing canonical modelConstruct a canonical model for the following open branch:a : created.P aintinga : created. a : created. Sculpture(a, b) : createdb: b : P aintingb : SculptureSolution: I {a, b} P ainting I {b} SculptureI createdI {(a, b)}Szymon Klarman12 / 1

AR@AIIntroduction to Description LogicCorrectnessThe key computational properties are given via three theorems: soundness: the algorithm proves only conclusions that are “really” true IF the tableau proof succeeds, i.e. it closes on some input, THENthe input is inconsistent IF the input is consistent THEN the tableau does not closeProof: show that the tableau rules preserve consistency, i.e.whenever the branch is consistent before an application of a rulethen after it, there must still exist at least one consistent branch. completeness: the algorithm can prove every true conclusion IF the input is inconsistent THEN the algorithm proves it, i.e. itcloses IF the algorithm does not close THEN the input is consistentProof: show that it is always possible to construct a model of theinput from an open branch.Szymon Klarman13 / 1

AR@AIIntroduction to Description LogicTermination termination: The algorithm always returns an answer after a finitenumber of inference steps.Proof: The size of the resulting tableau is bounded by the size of theinput (which is finite): applications of t and u result in strictly shorter formulas, for any a, the number of its successors generated by rule islimited by the number of assertions of type a : r.C, for any (a, b) : r, the number of possible applications of rule islimited by the number of assertions of type a : r.C. complexity: with empty TBoxes, the tableau algorithm isPSpace-complete.Szymon Klarman14 / 1

AR@AIIntroduction to Description LogicReasoning with non-empty TBoxesIn order to account for the TBox T , the tableau procedure has to beextended as follows:Input: Replace every C D T with C v D and D v C. Replace every C v D T with NNF ( C t D). Add T to the root of the tableau.Tableau rule: IF ( C) S and an individual a occurs in STHEN S 0 : S {a : C}Note: C indeed means that EVERY individual in any model must be C.Szymon Klarman15 / 1

AR@AIIntroduction to Description LogicExampleProblem: Is C satisfiable w.r.t. T {C v D, C v D} ?Tableau proof:1.2.3.Szymon Klarman C t D C t Da:CTTA16 / 1

AR@AIIntroduction to Description LogicExampleProblem: Is C satisfiable w.r.t. T {C v D, C v D} ?Tableau proof:1.2.3.4.5.Szymon Klarman C t D C t Da:Ca : C t Da : C t DTTA( : 1, 3)( : 2, 3)16 / 1

AR@AIIntroduction to Description LogicExampleProblem: Is C satisfiable w.r.t. T {C v D, C v D} ?Tableau proof:1.2.3.4.5.6.Szymon Klarman C t D C t Da:Ca : C t Da : C t Da : C ( t : 4) (1, 6)7.TTA( : 1, 3)( : 2, 3)a:D( t : 4)16 / 1

AR@AIIntroduction to Description LogicExampleProblem: Is C satisfiable w.r.t. T {C v D, C v D} ?Tableau proof:1.2.3.4.5. C t D C t Da:Ca : C t Da : C t Da : C ( t : 4) (1, 6)8. a : C ( t : 5) (1, 8)6.TTA( : 1, 3)( : 2, 3)7.9.a:D( t : 4)a : D ( t : 5) (7, 9)Output: C is UNSATISFIABLE w.r.t. TSzymon Klarman16 / 1

AR@AIIntroduction to Description LogicReasoning with non-empty TBoxes Soundness and completeness hold with small changes in proofs. The complexity is actually NExpTime-complete. Termination requires an additional supporting mechanism.Termination:Consider any input containing an axiom of the form: . . . r.C . . .A straightforward application of the rules and might lead toan infinite expansion of the tableau tree.Solution: Detect cycles and prevent further application of the rule.This is achieved by a special blocking rule.Szymon Klarman17 / 1

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.Szymon Klarman r.Ca:BTA18 / 1

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.3.Szymon Klarman r.Ca:Ba : r.CTA( : 1, 2)18 / 1

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.3.4.5.Szymon Klarman r.Ca:Ba : r.C(a, b) : rb:CTA( : 1, 2)( : 3)( : 3)18 / 1

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.3.4.5.6.Szymon Klarman r.Ca:Ba : r.C(a, b) : rb:Cb : r.CTA( : 1, 2)( : 3)( : 3)( : 1, 4)18 / 1