HƯỚNG DẪN DOWNLOAD TÀI LIỆU

Bước 1:Tại trang tài liệu slideshare.vn bạn muốn tải, click vào nút Download màu xanh lá cây ở phía trên.

Bước 2: Tại liên kết tải về, bạn chọn liên kết để tải File về máy tính. Tại đây sẽ có lựa chọn tải File được lưu trên slideshare.vn

Bước 3: Một thông báo xuất hiện ở phía cuối trình duyệt, hỏi bạn muốn lưu . - Nếu click vào Save, file sẽ được lưu về máy (Quá trình tải file nhanh hay chậm phụ thuộc vào đường truyền internet, dung lượng file bạn muốn tải)

Có nhiều phần mềm hỗ trợ việc download file về máy tính với tốc độ tải file nhanh như: Internet Download Manager (IDM), Free Download Manager, ... Tùy vào sở thích của từng người mà người dùng chọn lựa phần mềm hỗ trợ download cho máy tính của mình

VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28
A Horn Fragment with PTime Data Complexity of Regular Description Logic with Inverse
Linh Anh Nguyen1;2, Thi-Bich-Loc Nguyen3, Andrzej Szałas1;4
1Institute of Informatics, University of Warsaw, Poland
2Faculty of Information Technology, VNU University of Engineering and Technology, Vietnam 3Department of Information Technology, Hue University of Sciences, Vietnam 4Department of Computer and Information Science, Linko¨ping University, Sweden
Abstract
We study a Horn fragment called Horn-RegI of the regular description logic with inverse RegI, which extends the description logic ALC with inverse roles and regular role inclusion axioms characterized by ﬁnite automata. In contrast to the well-known Horn fragments EL, DL-Lite, DLP, Horn-SHIQ and Horn-SROIQ of description logics, Horn-RegI allows a form of the concept constructor “universal restriction” to appear at the left hand side of terminological inclusion axioms, while still has PTime data complexity. Namely, a universal restriction can be used in such places in conjunction with the corresponding existential restriction. We provide an algorithm with PTime data complexity for checking satisﬁability of Horn-RegI knowledge bases.
2014 Published by VNU Journal of Science.
Manuscript communication: received 16 December 2013, revised 27 April 2014, accepted 13 May 2014 Corresponding author: Linh Anh Nguyen, nguyen@mimuw.edu.pl
Keywords: Description logics, Horn fragments, rule languages, Semantic Web.
1. Introduction
Description logics (DLs) are variants of modal logics suitable for expressing terminological knowledge. Theyrepresentthedomainofinterest in terms of individuals (objects), concepts and roles. A concept stands for a set of individuals, a role stands for a binary relation between individuals. The DL SROIQ [1] founds the logical base of the Web Ontology Language OWL 2, which was recommended by W3C as a layer for the architecture of the Semantic Web.
As reasoning in SROIQ has a very high complexity, W3C also recommended the proﬁles OWL 2 EL, OWL 2 QL and OWL 2 RL, which are based on the families of DLs EL [2, 3], DL-Lite [4, 5] and DLP [6]. These families of DLs are monotonic rule languages enjoying PTime
suitable Horn fragments of the corresponding full languageswithappropriaterestrictionsadoptedto eliminate nondeterminism. A number of Horn fragments of DLs with PTime data complexity have also been investigated in [7, 8, 9, 10, 11, 12, 13]. The combined complexities of Horn fragments of DLs were studied, amongst others, in [14]. Some Horn fragments of DLs withoutABoxesthathavePTimecomplexityhave also been studied in [15, 2]. The fragments Horn-SHIQ [7, 11] and Horn-SROIQ [13] are notable, with considerable rich sets of allowed constructors and features. Combinations of rule languageslikeDatalogoritsextensionswithDLs have also been widely studied.
To eliminate nondeterminism, all EL [2, 3], DL-Lite [4, 5], DLP [6], Horn-SHIQ [7] and Horn-SROIQ [13] disallow (any form of) the
data complexity. They are deﬁned by selecting universal restriction 8R:C at the left hand side
L.A. Nguyen et al. / VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28 15
of v in terminological axioms. The problem is axioms guaranteeing PTime data complexity.
that the general Horn fragment of the basic DL ALCallowing8R:C atthelefthandsideofvhas
However, a big challenge is faced: the bottom-up approachisused,butnoteverypositiveHorn-Reg
NP-complete data complexity [12]. Also, roles knowledge base has a logically least model. As
are not required to be serial (i.e., satisfying the condition 8x9yR(x;y)), which complicates the construction of logically least models.
For many application domains, the proﬁles OWL2EL,OWL2QLandOWL2RLlanguages and the underlying Horn fragments EL, DL-Lite, DLP seem satisfactory. However, in general, forbidding 8R:C at the left hand side of v in terminological axioms is a serious restriction.
In [16] Nguyen introduced the deterministic Horn fragment of ALC, where the constructor 8R:C is allowed at the left hand side of v in the combination with 9R:C (in the form 8R:C u 9R:C, denoted by 89R:C [15]). He proved that such a fragment has PTime data complexity by providing a bottom-up method for constructing a logically least pseudo-model for a given deterministic positive knowledge base in the restricted language. In [12] Nguyen applied the method of [16] to regular DL Reg, which extends ALC with regular role inclusion axioms characterized by ﬁnite automata. Let us denote the Horn fragment of Reg that allows the constructor 89R:C at the left hand side of v by Horn-Reg. As not every positive Horn-Reg knowledge base has a logically least model, Nguyen [12] proposed to approximate the instance checking problem in Horn-Reg by using its weakenings with PTime data complexity.
To see the usefulness of the constructor 89R:C at the left hand side of v in terminological axioms, note that the following axioms are very intuitive and similar axioms are desirable:
89hasChild:Happy v HappyParent 89hasChild:Male v ParentWithOnlySons 89hasChild:Female v ParentWithOnlyDaughters
interestingu89path:interesting v perfect interestingt89link:interesting v worth surﬁng:
The works [16, 12] found a starting point for the research concerning the universal restriction 8R:C at the left hand side of v in terminological
a consequence, the work [12] on Horn-Reg is already complicated and the problem whether Horn-Reg has PTime data complexity remained open until [17].
This paper is a revised and extended version
of our conference paper [17]. In this work we study a Horn fragment called Horn-RegI of the regular description logic with inverse RegI. This fragment extends Horn-Reg with inverse roles. In contrast to the well-known Horn fragments EL, DL-Lite, DLP, Horn-SHIQ and Horn-SROIQ of description logics, Horn-RegI allows the concept constructor 89R:C to appear at the left hand side of terminological inclusion axioms. We provide an algorithm with PTime data complexity for checking satisﬁability of Horn-RegI knowledge bases. The key idea is to follow the top-down approach1 and use a special technique to deal with non-seriality of roles.
The DL RegI (resp. Reg) is a variant of regular grammar logic with (resp. without) converse [18, 19, 20, 21]. The current work is based on the previous works [16, 12, 22]. Namely, [22] considers Horn fragments of serial regular grammar logics with converse. The current work exploits the technique of [22] in dealing with converse (like inverse roles), but the dierence is that it concerns non-serial regular DLwithinverseroles. Thechangefromgrammar logic (i.e., modal logic) to DL is syntactic, but may increase the readability for the DL community.
Themainachievementsofthecurrentpaperare that:
it overcomes the diculties encountered in [16, 12] by using the top-down rather than bottom-up approach, and thus enables to show that both Horn-Reg and Horn-RegI
1In the top-down approach, the considered query is negated and added into the knowledge base, and in general, a knowledge base may contain “negative” constraints.
16 L.A. Nguyen et al. / VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28
havePTimedatacomplexity,solvinganopen problem of [12];
thetechniqueintroducedinthecurrentpaper for dealing with non-seriality leads to a solution for the important issue of allowing the concept constructor 89R:C to appear at the left hand side of v in terminological inclusion axioms.
In comparison with [17], note that:
Our algorithm now allows expansion rules to be applied in an arbitrary order. That is, any strategy can be used for expanding the constructed graph. This gives ﬂexibility for optimizing the computation.
The current paper provides full proofs for the results as well as additional examples and explanations.
The rest of this paper is structured as follows. In Section 2 we present notation and semantics ofRegI andrecallautomaton-modaloperators. In Section 3 we deﬁne the Horn-RegI fragment. In Section 4 we present our algorithm of checking satisﬁability of Horn-RegI knowledge bases and discuss our technique of dealing with 89R:C at the left hand side of v. In Section 5 we give proofs for the properties of the algorithm. We conclude this work in Section 6.
2. Preliminaries
2.1. Notation and Semantics of RegI
OurlanguageusesacountablesetCofconcept names, a countable set R+ of role names, and a countable set I of individual names. We use letterslikea, btodenoteindividualnames, letters like A, Btodenoteconceptnames,andletterslike r, s to denote role names.
Forr 2 R+, wecalltheexpressionr theinverse of r. Let R = fr j r 2 R+g and R = R+ [ R . For R = r, let R stand for r. We call elements of R roles and use letters like R, S to denote them.
A context-free semi-Thue system S over R is a ﬁnite set of context-free production rules over alphabet R. It is symmetric if, for every rule
R ! S1 :::Sk of S, the rule R ! Sk :::S1 is also in S.2 It is regular if, for every R 2 R, the
set of words derivable from R using the system is a regular language over R.
A context-free semi-Thue system is like a context-free grammar, but it has no designated start symbol and there is no distinction between terminal and non-terminal symbols. We assume that, for R 2 R, the word R is derivable from R using such a system.
A role inclusion axiom (RIA for short) is an expression of the form S1 Sk v R, where k 0. In the case k = 0, the left hand side of the inclusion axiom stands for the empty word ".
A regular RBox R is a ﬁnite set of RIAs such that
fR ! S1 :::Sk j (S1 Sk v R) 2 Rg
is a symmetric regular semi-Thue system S over R. We assume that R is given together with a mapping A that associates every R 2 R with a ﬁnite automaton AR recognizing the words derivable from R using S. We call A the RIA-automaton-speciﬁcation of R.
Recall that a ﬁnite automaton A over alphabet R is a tuple hR;Q;q0;;Fi, where Q is a ﬁnite set of states, q0 2 Q is the initial state, Q R Q is the transition relation, and F Q is the set of accepting states. A run of A on a word R1 :::Rk over alphabet R is a ﬁnite sequence of states q0;q1;:::;qk such that (qi 1;Ri;qi) holds for every 1 i k. It is an accepting run if qk 2 F. We say that A accepts a word w if there exists an accepting run of A on w.
Example 1. Let R = fr r v r; r r v rg. The symmetric regular semi-Thue system corresponding to R is
S = fr ! rr; r ! rrg:
The set of words derivable from r (resp. r) using S is a regular language characterized by the regular expression r [ (r;(r [ r);r) (resp. r [ (r;(r[r);r)). Hence,RisaregularRBox,whose RIA-automaton-speciﬁcation A is speciﬁed by:
2In the case k = 0, the right hand sides of the rules stand for ".
L.A. Nguyen et al. / VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28 17
Ar = hR;f0;1;2g;0;fh0;r;1i;h0;r;2i;h2;r;2i; h2;r;2i;h2;r;1ig;f1gi
The interpretation function I is extended to complex concepts as follows:
Ar = hR;f0;1;2g;0;fh0;r;1i;h0;r;2i;h2;r;2i; h2;r;2i;h2;r;1ig;f1gi:
Observe that every regular set of RIAs in SROIQ [1] and Horn-SROIQ [13] is a regular RBox by our deﬁnition. However, the above RBox R shows that the converse does not hold. Roughly speaking using the notion of regular expressions, “regularity” of a set of RIAs in SROIQ [1] and Horn-SROIQ [13] allows only a bounded nesting depth of the star operator , while “regularity” of a regular RBox in Horn-RegI is not so restricted. That is, our notion of regular RBox is more general than the notion of regular set of RIAs in SROIQ [1] and Horn-SROIQ [13]. C
>I = I; ?I = ;; (:C)I = I nCI; (C u D)I = CI \ DI; (C t D)I = CI [ DI;
(8R:C)I = fx 2 I j 8y(hx;yi 2 RI ) y 2 CI)g; (9R:C)I = fx 2 I j 9y(hx;yi 2 RI ^y 2 CI)g:
Given an interpretation I and an axiom/assertion ’, the satisfaction relation I j= ’ is deﬁned as follows, where at the right hand side of “if” stands for composition of relations:
I j= S1 Sk v R if SI Sk RI I j= " v R if "I v RI
I j= C v D if CI DI
Let R be a regular RBox and A be its RIA-automaton-speciﬁcation. For R;S 2 R, we say that R is a subrole of S w.r.t. R, denoted by
I j= C(a)
I j= r(a;b)
if aI 2 CI
if haI;bIi 2 rI:
R vR S, if the word R is accepted by AS. Concepts are deﬁned by the following BNF
grammar, where A 2 C, R 2 R:
C ::= > j ? j A j :C j C uC j C tC j 8R:C j 9R:C
We use letters like C, D to denote concepts (including complex concepts).
A TBox is a ﬁnite set of TBox axioms of the form C v D. An ABox is a ﬁnite set of assertions of the form C(a) or r(a;b). A knowledge base is a tuple hR;T;Ai, where R is a regular RBox, T is a TBox and A is an ABox.
An interpretation is a pair I = hI;Ii, where I is a non-empty set called the domain of I and I is a mapping called the interpretation function of I that associates each individual name a 2 I with an element aI 2 I, each concept name A 2
C with a set AI I, and each role name r 2 R+ with a binary relation rI I I.
Deﬁne
If I j= ’ then we say that I validates ’.
An interpretation I is a model of an RBox R, a TBox T or an ABox A if it validates all the axioms/assertions of that “box”. It is a model of a knowledge base hR;T;Ai if it is a model of all R, T and A.
A knowledge base is satisﬁable if it has a model. For a knowledge base KB, we write KB j= ’ to mean that every model of KB validates ’. If KB j= C(a) then we say that a is an instance of C w.r.t. KB.
2.2. Automaton-Modal Operators
Given an interpretation I and a ﬁnite automaton A over alphabet R, deﬁne AI = fhx;yi 2 I I j there exist a word R1 :::Rk acceptedbyAandelements x0 = x, x1,..., xk = y of I such that hxi 1;xii 2 RI for all 1 i kg.
We will use auxiliary modal operators [A]
and hAi, where A is a ﬁnite automaton over alphabet R. We call [A] (resp. hAi) a universal
(r)I = (rI) 1 =
"I =
fhy;xi j hx;yi 2 rIg
(for r 2 R+) fhx;xi j x 2 Ig:
(resp. existential) automaton-modal operator. Automaton-modal operators were used earlier, among others, in [23, 20, 24, 25, 12].
18 L.A. Nguyen et al. / VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28
Intheextendedlanguage,ifC isaconceptthen [A]C and hAiC are also concepts. The semantics of [A]C and hAiC are deﬁned as follows:
([A]C)I = x 2 I j 8y hx;yi 2 AI implies y 2 CI (hAiC)I = x 2 I j 9y hx;yi 2 AI and y 2 CI :
For a ﬁnite automaton A over R, let the components of A be denoted as in the following:
A = hR;QA;qA;A;FAi:
If q is a state of a ﬁnite automaton A then by Aq we denote the ﬁnite automaton obtained from A by replacing the initial state by q.
Lemma 1. Let I be a model of a regular RBox R, A be the RIA-automaton-speciﬁcation of R, C be a concept, and R 2 R. Then:
1. (8R:C)I = ([AR]C)I, 2. (9R:C)I = (hARiC)I,
3. CI ([AR]hARiC)I, 4. CI ([AR]9R:C)I.
Proof: The ﬁrst assertion holds because the following conditions are equivalent:
x 2 (8R:C)I;
for all y 2 I, if hx;yi 2 RI then y 2 CI;
for all y 2 I, if hx;yi 2 (AR)I then y 2 CI;
x 2 ([AR]C)I.
Analogously, the second assertion holds. Consider the third assertion and suppose x 2
CI. We show that x 2 ([A ]hARiC)I. Let y be an arbitrary element of I such that hx;yi 2 (A )I. By deﬁnition, there exist a word R1 :::Rk accepted by A and elements x0 = x, x1, ..., xk = y of I such that hxi 1;xii 2 Ri for all 1 i k. Observe that the word Rk :::R1 is
accepted by AR. Since x 2 CI, xk = y, x0 = x and hxi;xi 1i 2 RI for all k i 1, we have that
y 2 (hARiC)I. Therefore, x 2 ([AR]hARiC)I. The fourth assertion directly follows from the
third and second assertions. C
3. The Horn-RegI Fragment
Let 89R:C stand for 8R:C u 9R:C. Left-hand-side Horn-RegI concepts, called LHS Horn-RegI concepts for short, are deﬁned by the following grammar, where A 2 C and R 2 R:
C ::= > j A j C uC j C tC j 89R:C j 9R:C
Right-hand-side Horn-RegI concepts, called RHS Horn-RegI concepts for short, are deﬁned by the following BNF grammar, where A 2 C, D is an LHS Horn-RegI concept, and R 2 R:
C ::= > j ? j A j :D j C uC j :DtC j 8R:C j 9R:C
A Horn-RegI TBox axiom, is an expression of the form C v D, where C is an LHS Horn-RegI concept and D is an RHS Horn-RegI concept.
A Horn-RegI TBox is a ﬁnite set of Horn-RegI TBox axioms.
A Horn-RegI clause is a Horn-RegI TBox axiom of the form C1 u ::: u Ck v D or > v D, where:
each Ci is of the form A, 89R:A or 9R:A,
D is of the form ?, A, 8R:A or 9R:A,
k 1, A 2 C and R 2 R.
A clausal Horn-RegI TBox is a TBox consisting of Horn-RegI clauses.
A Horn-RegI ABox is a ﬁnite set of assertions of the form C(a) or r(a;b), where C is an RHS Horn-RegI concept. A reduced ABox is a ﬁnite set of assertions of the form A(a) or r(a;b).
A knowledge base hR;T;Ai is called a Horn-RegI knowledge base if T is a Horn-RegI TBox and A is a Horn-RegI ABox. When T is a clausal Horn-RegI TBox and A is a reduced ABox, we call such a knowledge base a clausal Horn-RegI knowledge base.
Example 2. This example is about Web pages. Let R+ = flink;pathg and let R be the regular RBox consisting of the following role axioms:
link v path; link v path;
link path v path; pathlink v path:
L.A. Nguyen et al. / VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28 19
This RBox “deﬁnes” path to be the transitive closure of link. As the RIA-automaton-speciﬁcation of R we can take the mapping A such that:
The data complexity class of Horn-RegI is deﬁned to be the complexity class of the problem of checking satisﬁability of a Horn-RegI knowledge base hR;T;Ai, measured in the size of A when assuming that R and T are ﬁxed and
Alink = hR;f1;2g;1;fh1;link;2ig;f2gi; A is a reduced ABox.
Alink = hR;f1;2g;2;fh2;link;1ig;f1gi; Proposition 2. Let KB = hR;T;Ai be a Apath = hR;f1;2g;1; Horn-RegI knowledge base.
fh1;link;1i;h1;link;2i;h1;path;2ig;f2gi; 1. If C is an LHS Horn-RegI concept then Apath = hR;f1;2g;2; KB j= C(a) i the Horn-RegI knowledge
fh1;link;1i;h2;link;1i;h2;path;1ig;f1gi: base hR, T [ fC v Ag, A[f:A(a)gi is Let T be the TBox consisting of the following unsatisﬁable, where A is a fresh concept
program clauses: 2. KB can be converted in polynomial time in the sizes of T and A to a Horn-RegI
perfect v interestingu8path:interesting knowledge base KB0 = hR;T0;A0i with
interestingu89path:interesting v perfect A0 being a reduced ABox such that KB is interestingt89link:interesting v worth surﬁng: 3. KB can beiconverted in polynomial time in
Let A be the ABox speciﬁed by the concept thesizeofT toaHorn-RegI knowledgebase assertion perfect(b) and the following role KB0 = hR;T0;Ai with T0 being a clausal assertions of link: Horn-RegI TBox such that KB is satisﬁable
i KB0 is satisﬁable.
a b ===
=
== h i
Then KB = hR;T;Ai is a Horn-RegI knowledge base. (Ignoring link and path, which are not essential in this example, KB can be treated as a Horn-Reg knowledge base.) It can be seen that b, e, f, i are instances of the concepts perfect, interesting, worth surﬁng w.r.t. KB. Furthermore, h is also an instance of the concept interesting w.r.t. KB. C
The length of a concept, an assertion or an axiom ’ is the number of symbols occurring in ’. The size of an ABox is the sum of the lengths of its assertions. The size of a TBox is the sum of the lengths of its axioms.
Proof: The ﬁrst assertion is clear. For the second assertion, we start with T0 := T and A0 := A and then modify them as follows: for each C(a) 2 A0 where C is not a concept name, replace C(a) in A0 by A(a), where A is a fresh concept name, and add to T0 the axiom A v C. It is easy to check that the resulting Horn-RegI knowledge base KB0 = hR;T0;A0i is satisﬁable i KB is satisﬁable.
For the third assertion, we apply the technique that replaces complex concepts by fresh concept names. For example, if 89R:C v 9S:D is an axiom of T, where C and D are complex concepts, then we replace it by axioms C v AC, 89R:AC v 9S:AD and AD v D, where AC and AD are fresh concept names. C
Corollary 3. Every Horn-RegI knowledge base KB = hR;T;Ai can be converted in polynomial time in the sizes of T and A to a clausal Horn-RegI knowledge base KB0 = hR;T0;A0i such that KB is satisﬁable i KB0 is satisﬁable.
20 L.A. Nguyen et al. / VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 4 (2014) 14–28
Proof: This corollary follows from the second and third assertions of Proposition 2. In particular, we ﬁrst apply the conversion mentioned in the second assertion of Proposition 2 to KB to obtain KB2, and then apply the conversion mentioned in the third assertion of Proposition 2 to KB2 to obtain KB0.C
(∀i) if r(a,b) ∈ A then ExtendLabel(b,Trans(Label(a),r));
(∀) if x is reachable from Δ0 and Next(x,∃R.C) = y then Next(x,∃R.C) :=
Find(Label(y) ∪ Satr(Trans(Label(x),R)));
(∀I) if x is reachable from Δ0 and hx,R,yi ∈ Edges then ExtendLabel(x,Trans(Label(y),R));
(∃) if x is reachable from Δ0, ∃R.C ∈ Label(x), R ∈ R and Next(x,∃R.C) is not deﬁned then Next(x,∃R.C) :=
Find(Satr({C} ∪ Trans(Label(x),R)) ∪ T 0);
4. Checking Satisﬁability of Horn-RegI Knowledge Bases
(v) if x is reachable from Δ0, (C v D) ∈ Label(x) and CheckPremise(x,C) then ExtendLabel(x,{D});
Table 1: Expansion rules for Horn-RegI graphs.
In this section we present an algorithm that, given a clausal Horn-RegI knowledge base hR;T;Ai together with the RIA-automaton-speciﬁcation A of R, checks whether the knowledge base is satisﬁable. The algorithm has PTime data complexity.
We will treat each TBox axiom C v D from T as a concept standing for a global assumption. That is, C v D is logically equivalent to :C t D, and it is a global assumption for an interpretation I if (:C t D)I = I.
Let X be a set of concepts. The saturation of X (w.r.t.AandT), denotedbySatr(X), isdeﬁned to be the least extension of X such that:
1. if 8R:C 2 Satr(X) then [AR]C 2 Satr(X),
2. if [A]C 2 Satr(X) and qA 2 FA then C 2 Satr(X),
3. if 89R:A occurs in T for some A then
[AR]9R:> 2 Satr(X),
4. if A 2 Satr(X) and 9R:A occurs at the left
hand side of v in some clause of T then [AR]hARiA 2 Satr(X).
Notice the third item in the above list. It is used for dealing with non-seriality and the concept constructor 89R:A. Another treatment for the problem of non-seriality and 89R:A is the step 5 of Function CheckPremise (used in our algorithm). It will be explained later.
For R 2 R, the transfer of X through R is
Trans(X;R) = f[Aq]C j [A]C 2 X and hqA;R;qi 2 Ag:
Our algorithm for checking satisﬁability of hR;T;Ai uses the data structure h0;;Label;Nexti, which is called a Horn-RegI graph, where:
Function Find(X)
1 if there exists z ∈ Δ \ Δ0 with Label(z) = X then 2 return z
3 else
4 add a new element z to Δ with Label(z) := X; 5 return z
Procedure ExtendLabel(z,X)
1 if X ⊆ Label(z) then return;
2 if z ∈ Δ0 then Label(z) := Label(z) ∪ Satr(X) 3 else
4 z∗ := Find(Label(z) ∪ Satr(X));
5 foreach y, R, C such that Next(y,∃R.C) = z do 6 Next(y,∃R.C) := z∗
Function CheckPremise(x,C)
1 if C = > then return true 2 else let C = C1 u ... u Ck; 3 foreach 1 ≤ i ≤ k do
4 if Ci = A and A ∈/ Label(x) then return false 5 else if Ci = ∀∃R.A and (∃R.> ∈/ Label(x) or
Next(x,∃R.>) is not deﬁned or A ∈/ Label(Next(x,∃R.>))) then
6 return false
7 else if Ci = ∃R.A and hARiA ∈/ Label(x) then 8 return false
9 return true
Algorithm 1: checking satisﬁability in Horn-RegI Input: a clausal Horn-RegI knowledge base hR,T ,Ai