Tableau algorithm for ALC - cvutcz
pletion graph simple, as presented However, tableaux algorithms for expressive de-scription logics require more complex structures and more complex transformations to achieve such correspondence, see e g [1] or [2] for more details Example 1 Let’s check consistency of an ALContology O= f g, where is C(PillarScour) and Cis
The Simplex Method: Step by Step with Tableaus
The Simplex Method: Step by Step with Tableaus The simplex algorithm (minimization form) can be summarized by the following steps: Step 0 Form a tableau corresponding to a basic feasible solution (BFS)
Semantic Tableaux for Propositional Logic
tableaux Example: Let ϕ = (A1 ∧ ¬A2 ∧ A3 ∧ ¬A4) ∨ (¬A1 ∧ ¬A3 ∧ A3 ∧ ¬A4) The root of the tree is the original formula Each child of the root node is a disjunct Since one of the branches is satisfiable, the whole formula is Notice that expansion need not proceed beyond discovery of the first satisfiable node Thus, a
A Tableau Decision Procedure for SHOIQ
A Tableau Decision Procedure for SHOIQ 3 blocking to ensure termination This is of special interest for SHIQ, where the interaction between inverse roles and number restrictions results in the
Basics of SAT Solving Algorithms
Dec 10, 2008 · Outline Vocabulary and Preliminaries Basic Algorithm Boolean Constraint Propagation Con ict Analysis High-level Strategy Reading Sol Swords Basics of SAT Solving Algorithms December 8, 2008 2 / 24
LES ALGORITHMES DE TRI - New generation New mind
L'algorithme du tri à bulles (bubble sort en anglais) consiste à comparer les différentes valeurs adjacentes du tableau T, et à les permuter s'ils ne sont pas dans le bon ordre Pour i de 1 à N-1 Faire Si (T[i] > T[i+1]) Alors Proc Permuter (T[i], T[i+1])
[PDF] programmation mblock
[PDF] tuto mblock
[PDF] mbot programmation
[PDF] algorithme nombre d or
[PDF] algorithme première es
[PDF] algobox suite arithmétique
[PDF] cours et exercices corrigés complexités algorithmique
[PDF] algorithme avancé et complexité pdf
[PDF] algorithme avancé exercices corrigés pdf
[PDF] exercice corrigé algorithme recursivité
[PDF] algorithme avancé cours et exercices
[PDF] algorithmique avancée master
[PDF] td algorithme avancé
[PDF] algorithme equation 2eme degré pascal
Tableau algorithm forALC
Petr Kremen
version 0.2 The algorithm, introduced originally in [3] in slighter dierent form, aims at con- structing a model of anALContologyO=T [ A. During the algorithm run, each (possibly innite) candidate model is represented by a (necessarily nite)completion graph. Acompletion graphis a labeled oriented graphG=hVG;EG;LGi, where eachx2VG is labeled with a setLG(x) of concepts, and each edgehx;yi 2EGis labeled with a setLG(hx;yi) of roles. Furthermore, a completion graphG contains a direct clash, iffA;:Ag LG(x) for some named conceptA, or ? 2LG(x), or:> 2LG(x) is complete w.r.t. to the setJof rules, if no completion rule fromJcan be applied on it. The tableau algorithm evolves a setSof completion graphs (corresponding to partial candidate models) according to completion rules inJ. Whenever a rule application causes a clash in a completion graph, the graph is discarded (which prunes candidate models corresponding to the graph). The algorithm terminates when no more rules can be applied on a clash-free completion graph (ontology is consistent), or when no completion graph remains to explore (ontology is inconsistent).1 Tableau algorithm forALCwith empty TBox
First focus on the case when TBox is empty, i.e.T=;. In this case the setJof applicable completion rules is depicted in Table 1. The procedure is as follows: 1. (PREPR OCESSING)All concepts in Ohave to be transformed into Negational Normal Form. This means to \move negation in front of named concepts" using equivalences,like:(C1uC2) :C1t :C2, or:(9RC) 8R :C. 2. (INITIALIZA TION)Initial state of the algorithm is S0=fG0g, whereG0= hVG0;EG0;LG0iis a completion graph, that \corresponds toA", i.e. VG0contains all named individuals occuring in some axiom ofA 1 EG0contains all pairsha1;a2ioccuring in someR(a1;a2)2 A. LG0labels each vertex (individual)awith a setfCjC(a)2 Ag, and each edgeha1;a2iwith a setfRjR(a1;a2)2 Ag. 3. (CONSISTENCY TEST) Denote the curren tstate as S. Remove fromSanyG thatcontains a direct clash. IfS=;then return INCONSISTENT. 4. (MODEL TEST) T akearbitr aryG2 Sthat does not contain a direct clash. IfGiscompletewith respect to completion rules inJ.
5. (R ULEAPPLICA TION)Find a completion rule that is ap plicableon G. Denote the new stateS0created from the current stateSand go to step 2. u-ruleif: (C1uC2)2LG(a), for someaandfC1;C2g*LG(a).then:S0=S [ fG0g n fGg, whereG0=hVG;EG;LG0i.LG0=LGexceptLG0(a) =LG(a)[ fC1;C2g.t-ruleif: (C1tC2)2LG(a), for someaandfC1;C2g \LG(a) =;.then:S0=S [ fG1;G2g n fGg, whereGk=hVG;EG;LGki.L
Gk=LGexceptLGk(a) =LG(a)[ fCkgfork2 f1;2g.9-ruleif:9RC2LG(a1), for somea1, and there isnoa22VG, such that bothR2LG(ha1;a2i) andC2LG(a2).then:S0=S [ fG0g n fGg, whereG0=hVG[ fa2g;EG[ fha1;a2ig;LG0i.L
G0=LGexceptLG0(a2) =fCg,LG0(ha1;a2i) =fRg.8-ruleif:8RC2LG(a1), for somea1and there isa22VG, such thatR2LG(ha1;a2i), but notC2LG(a2).then:S0=S [ fG0g n fGg, whereG0=hVG;EG;LG0i.L
G0=LGexceptLG0(a2) =LG0(a2)[ fCg.Table 1:Completion rules used for expanding a set of ALCcompletion graphs (and
not considering TBox).G=hVG;EG;LGiis the completion graph chosen in the current iteration. The algorithm does not prescribe the order, in which the rules are selected. Of course, this can signicantly in uence performance. E.g. non-deterministic rules (t- rule in case ofALC)shouldbe performed only when no other rule is applicable, to prevent generating additional completion graphs rst, all of which need to be tested in CONSISTENCY/MODEL TEST steps of the algorithm. For details on other tableau optimization technique, see e.g. Chapter 9 in [1]. Correctness and CompletenessI will not repeat the full proof of correctness and completeness of the algorithm, that was already presented in [1] and [3]. I only sketch main rationale behind the algorithm that helps to better understand its idea. Cor- rectness is a direct consequence of the semantics of completion rules. E.g. if there was a modelIcorresponding toGandA1uA22LG(a) for somea, then, following the 2 semantics ofALC,aI2(A1uA2)IandaI2A1I\A2I. This is ensured by putting bothA1andA2into theL0G(a) by theurule. For the other direction and other rules the idea is similar. Completeness is shown by constructing a canonical modelIofOfor each complete completion graph that does not contain a direct clash, as follows: The interpretation domain Icontains all graph vertices, for each named conceptAwe deneAI=fajA2LG(a)g, for each named roleRwe deneRI=fha1;a2i jR2LG(ha1;a2i)g, Induction according to the axiom types and complex concept structure shows that it is indeed a model of the original ontology. E.g. ifC(a)2 O, thenaI2CImust hold for any complete graphG: (i) ifC=Ais a named concept, then indeedaI2AIbecause A2LG0(a) (this is, howG0was constructed in the INITIALIZATION step of the algorithm) andLG0(a)[LG(a), (ii) ifC=A1uA2where bothA1andA2are named concepts, thenaI2A1uA2Iand thusaI2A1IandaI2A2IbecausefA1;A2g LG0 whereG0is a completion graph that resulted from application theu-rule. If this rule was not applied, thenGG0is not complete, which contradicts our assumption. For the other axiom types and concept constructs the idea is similar. In case ofALC, there is a correspondence between a model and a complete com- pletion graph simple, as presented. However, tableaux algorithms for expressive de- scription logics require more complex structures and more complex transformations to achieve such correspondence, see e.g. [1] or [2] for more details. Example 1Let's check consistency of anALContologyO=fg, whereisC(PillarScour) andCis (9isFailureOfColumnu 9isFailureOfPillaru :9isFailureOf(PillaruColumn)) This axiom says thatPillarScouris failure of some bridge and it is a failure of some pillar but it is not a failure of an object that is a bridge and a pillar at the same time. The rst step is to transform the complex concept into Negational Normal Form.This produces2that isC2(PillarScour)whereC2is
(9isFailureOfColumnu 9isFailureOfPillaru 8isFailureOf(:Pillaru :Column))2is semantically equivalent with(i.e.fg j=f2gandf2g j=fg), but it has
negations only before named concepts. The initial state of the algorithm isS0=fG0g, where graph G0=hfPillarScourg;;;fPillarScour7! fC2ggi(1)
is shown in Figure 1. At this point, the algorithm passes four sequences of the steps CONSISTENCY TEST!MODEL TEST!RULE APPLICATION of the tableau algorithm, that 3Figure 1:Initial state of th etableau algorithm.
can be denoted as a state evolution during the step RULE APPLICATION (the label over the arrow denotes the rule that was used): fG0gu-rule! fG1g9-rule! fG2g9-rule! fG3g8-rule! fG4g;whereG4is depicted in Figure 2.Figure 2:Graph G4evolved deterministically fromG0usingu-rule,9-rule,8-rule.
So far, only deterministic rules (i.e. those that do not increase the number of com- pletion graphs) have been used. Looking carefully at Figure 2, it is clear that the only rule that remains applicable is thet-rule. The rule can be applied on the concept (:Columnt :Pillar)in the label of either vertex0or1. Picking e.g.0and applying t-rule produces a new statefG5;G6gdepicted in Figure 3. GraphG5contains a direct clash, asColumnand:Columnis in the label of vertex0, and thusG5is discarded, as it cannot be transformed to a model (e.g. the canonical
model dened in relation to the completeness of the algorithm). Thus,G6is picked andt-rule is applied, which results in a new statefG7;G8g, as shown in Figure 4. WhileG7contains a direct clash in vertex1, completion graphG8is complete with respect to theALCcompletion rules and does not contain a direct clash. Thus, a canonical modelI1=hI1;I1ican be constructed fromG8as follows: 4 (a) GraphG5(b) GraphG6Figure 3:
Graph sG5andG6produced by application of thet-rule on vertex0.I1=fPillarScour;0;1g
isFailureOfI1=fhPillarScour;0i;hPillarScour;1ig
Pillar
I1=f1g
Column
I1=f0g
PillarScour
I1=fPillarScourg
I1is not the only intepretation ofO- another model ofOmight beI2, for which
Column=f0;PillarScourgand coincides withI1on the rest. This documents the fact that a complete completion graph corresponds to one (canonical) model, but might 5 (a) GraphG7(b) GraphG8Figure 4:
Graph sG7andG8produced by application of thet-rule on vertex1. correspond to other models as well.2 Tableau algorithm for generalALC
In the general case, the situation is slightly complicated. The TBox knowledge is included in the algorithm by an extra rulev-ruleif: (C1vC2)2 Tand (:C1tC2)=2LG(a) for someathat is not blocked.then:S0=S [ fG0g n fGg, whereG0=hVG;EG;LG0i.L
G0=LGexceptLG0(a) =LG(a)[ f:C1tC2g.6
For this rule to be applicable, each equivalence axiomC1C22 Thas to be replaced by two subsumption axiomsC1vC2andC2vC1in the PREPROCESS- ING step of the algorithm. Unfortunately, such simple extension of the tableau al- gorithm need not terminate. E.g. consider ontologyO=fObjectv 9hasPartObject;Object(CharlesBridge)g.
2.1 Blocking
To ensure termination of the algorithm it is necessary to detect cycles of the generated model that might occur due to the application of thev-rule. The cycles are detected usingblockingthat ensures that a completion graph, although representing possibly innite model, is always nite. This is ensured by preventing the inference rules to generate node and edge patterns that \repeat regularly". The notion of regularity is dierent for each description logic; forALC,so calledsubset blocking[1] is used: A vertexa1in a completion graphG, but not occuring inA,is blocked by a vertexa2, if there is an oriented path inGfroma2toa1and a LG(a1)LG(a1).
Then all rules are applicableonlyon an individual, only if this individual is not blocked. As a result we get a set of completion rules inALCwith general TBox, as shown in Table 2v-ruleif: (C1vC2)2 Tand (:C1tC2)=2LG(a) for someathat is not blocked.then:S0=S [ fG0g n fGg, whereG0=hVG;EG;LG0i.L
G0=LGexceptLG0(a) =LG(a)[ f:C1tC2g.u-ruleif: (C1uC2)2LG(a), for someathat is not blockedandfC1;C2g*LG(a).then:S0=S [ fG0g n fGg, whereG0=hVG;EG;LG0i.L
G0=LGexceptLG0(a) =LG(a)[ fC1;C2g.t-ruleif: (C1tC2)2LG(a), for someathat is not blockedandfC1;C2g \LG(a) =;.then:S0=S [ fG1;G2g n fGg, whereGk=hVG;EG;LGki.L
Gk=LGexceptLGk(a) =LG(a)[ fCkgfork2 f1;2g.9-ruleif:9RC2LG(a1), for somea1that is not blocked, and there isnoa22VG, such that bothR2LG(ha1;a2i) andC2LG(a2).then:S0=S [ fG0g n fGg, whereG0=hVG[ fa2g;EG[ fha1;a2ig;LG0i.L
G0=LGexceptLG0(a2) =fCg,LG0(ha1;a2i) =fRg.8-ruleif:8RC2LG(a1), for somea1that is not blockedand there isa
22VG, such thatR2LG(ha1;a2i), but notC2LG(a2).then:S0=S [ fG0g n fGg, whereG0=hVG;EG;LG0i.L
G0=LGexceptLG0(a2) =LG0(a2)[ fCg.Table 2:Completion rules used for expanding a se tof ALCcompletion graphs.G=
hVG;EG;LGiis the completion graph chosen in the current iteration. 7