# Introduction To Description Logic

2y ago
57 Views
377.62 KB
42 Pages
Last View : 1m ago
Transcription

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

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.3.4.5.6.7.8.Szymon Klarman r.Ca:Ba : r.C(a, b) : rb:Cb : r.C(b, c) : rc:CTA( : 1, 2)( : 3)( : 3)( : 1, 4)( : 6)( : 6)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.7.8.9.10.Szymon Klarman r.Ca:Ba : r.C(a, b) : rb:Cb : r.C(b, c) : rc:Cc : r.C.TA( : 1, 2)( : 3)( : 3)( : 1, 4)( : 6)( : 6)( : 1, 7)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.7.8.9.10. r.Ca:Ba : r.C(a, b) : rb:Cb : r.C(b, c) : rc:Cc : r.C.TA( : 1, 2)( : 3)( : 3)( : 1, 4)( : 6)( : 6)( : 1, 7) B IF b is a (possibly indirect) successor of a in S and it is the case that:{C b : C S} {D a : D S}THEN mark b as BLOCKED by a in S and do not apply to bSzymon Klarman18 / 1

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.3.4.5.6.7.8.9. r.Ca:Ba : r.C(a, b) : rb:Cb : r.C(b, c) : rc:Cc : r.CTA( : 1, 2)( : 3)( : 3)( : 1, 4)( : 6)( : 6)( : 1, 7)La {B, r.C}Lb {C, r.C}Lc {C, r.C}c is BLOCKED by b do not expand this anymore! B IF b is a (possibly indirect) successor of a in S and it is the case that:{C b : C S} {D a : D S}THEN mark b as BLOCKED by a in S and do not apply to bSzymon Klarman18 / 1

AR@AIIntroduction to Description LogicBlocking exampleProblem: Is B satisfiable w.r.t. T { r.C} ?Tableau proof:1.2.3.4.5.6.7.8.9. r.Ca:Ba : r.C(a, b) : rb:Cb : r.C(b, c) : rc:Cc : r.CTA( : 1, 2)( : 3)( : 3)( : 1, 4)( : 6)( : 6)( : 1, 7)La {B, r.C}Lb {C, r.C}Lc {C, r.C}c is BLOCKED by b do not expand this anymore!Output: C is SATISFIABLE w.r.t. TWarning: to ensure completeness, the blocking rule can be applied ONLYwhen no other rules (apart from ) apply anymore on the branch.Szymon Klarman18 / 1

AR@AIIntroduction to Description LogicData structures for tableauxPractical implementations of the tableau algorithm for DLs often usedifferent data structures — closer to DL models. An open branch isrepresented as a labeled graph, where:nodesindividualsnode labelsconceptsedgesrole relationshipsedge labelsrole namesExample:1.2.3.4.5.6.a : r.A u r.(C t D)a : r.Aa : r.(C t D)(a, b) : rb:Ab:C tDb:C8. r.A u r.(C t D), r.A, r.(C t D)ar b7. r.A u r.(C t D), r.A, r.(C t D)arA, C t D, C bA, C t D, Db:DNote: The branching t rule involves duplicating of the branch.Szymon Klarman19 / 1

AR@AIIntroduction to Description LogicSummary All basic reasoning problems for ALC can be turned into a task offinding a model of the ABox and the TBox. Tableau algorithm is a decision procedure, i.e. sound, complete andterminating algorithm, employing exactly this strategy. Whenever the algorithm terminates and tableau is open, we canconstruct a canonical model of the input.Resources:F. Baader, U. Sattler. An Overview of Tableau Algorithms for Description Logics.In: Studia Logica 69(1), 2001.(see Blackboard)Description Logic resources: http://dl.kr.org/Next: LoTREC tutorial and handing in the assignment. Please bring laptops with LoTREC installedhttp://www.irit.fr/Lotrec/Szymon Klarman20 / 1

Introduction to Description Logic Szymon Klarman (part of the content based on the tutorial by Stefan Schlobach) szymon.klarman@gmail.com VU University Amsterdam, 2009-2012. AR@AI Introduction to Description Logic Plan for today Tableau algorithm for ALCwith empty TBoxes Soundness, completeness, termination Reasoning w.r.t. non-empty TBoxes Szymon Klarman 1 / 1. AR@AI Introduction to .

Related Documents:

Dynamic Logic Dynamic Circuits will be introduced and their performance in terms of power, area, delay, energy and AT2 will be reviewed. We will review the following logic families: Domino logic P-E logic NORA logic 2-phase logic Multiple O/P domino logic Cascode logic

An Introduction to Description Logic IV Relations to rst order logic Marco Cerami Palack y University in Olomouc Department of Computer Science Olomouc, Czech Republic Olomouc, November 6th 2014 Marco Cerami (UP) Description Logic IV 6.11.2014 1 / 25. Preliminaries Preliminaries: First order logic Marco Cerami (UP) Description Logic IV 6.11.2014 2 / 25. Preliminaries Syntax Syntax: signature .

Digital Logic Fundamentals Unit 1 – Introduction to the Circuit Board 2 LOGIC STATES The output logic state (level) of a gate depends on the logic state of the input(s). There are two logic states: logic 1, or high, and logic 0, or low. The output of some gates can also be in a high-Z (high impedance) state, which is neither a high

An Introduction to Modal Logic 2009 Formosan Summer School on Logic, Language, and Computation 29 June-10 July, 2009 ; 9 9 B . : The Agenda Introduction Basic Modal Logic Normal Systems of Modal Logic Meta-theorems of Normal Systems Variants of Modal Logic Conclusion ; 9 9 B . ; Introduction Let me tell you the story ; 9 9 B . Introduction Historical overview .

MOSFET Logic Revised: March 22, 2020 ECE2274 Pre-Lab for MOSFET logic LTspice NAND Logic Gate, NOR Logic Gate, and CMOS Inverter Include CRN # and schematics. 1. NMOS NMOSNAND Logic Gate Use Vdd 10Vdc. For the NMOS NAND LOGIC GATE shown below, use the 2N7000 MOSFET LTspice model that has a gate to source voltage Vgs threshold of 2V (Vto 2.0).File Size: 586KB

categorical and hypothetical syllogism, and modal and inductive logic. It is also associated with the Stoics and their propositional logic, and their work on implication. Syllogistic logic and propositional logic led later to the development of predicate logic (or first order logic, i.e. the foundational logic for mathematics)

The University of Texas at Arlington Sequential Logic - Intro CSE 2340/2140 – Introduction to Digital Logic Dr. Gergely Záruba The Sequential Circuit Model x 1 Combinational z1 x n zm (a) y y Y Y Combinational logic logic x1 z1 x n z m Combinational logic with n inputs and m switching functions: Sequential logic with n inputs, m outputs, r .

2.2 Fuzzy Logic Fuzzy Logic is a form of multi-valued logic derived from fuzzy set theory to deal with reasoning that is approximate rather than precise. Fuzzy logic is not a vague logic system, but a system of logic for dealing with vague concepts. As in fuzzy set theory the set membership values can range (inclusively) between 0 and 1, in