A horn fragment with ptime data complexity of regular description logic with inverse

Đăng ngày 4/25/2019 3:41:12 AM | Thể loại: | Lần tải: 0 | Lần xem: 13 | Page: 15 | FileSize: 0.32 M | File type: PDF
A horn fragment with ptime data complexity of regular description logic with inverse. 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 finite 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.
c
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 finite 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 satisfiability 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
suitable Horn fragments of the corresponding full
languageswithappropriaterestrictionsadoptedto
Description logics (DLs) are variants of modal
eliminate nondeterminism.
A number of Horn
logics
suitable
for
expressing
terminological
fragments of DLs with PTime data complexity
knowledge. Theyrepresentthedomainofinterest
have
also
been
investigated
in
[7,
8,
9,
10,
in terms of individuals (objects), concepts and
11,
12,
13].
The
combined
complexities
of
roles.
A concept stands for a set of individuals,
Horn fragments of DLs were studied, amongst
a
role
stands
for
a
binary
relation
between
others, in [14].
Some Horn fragments of DLs
individuals.
The DL SROIQ [1] founds the
withoutABoxesthathavePTimecomplexityhave
logical
base
of
the
Web
Ontology
Language
also been studied in [15, 2].
The fragments
OWL 2, which was recommended by W3C as a
Horn-SHIQ [7, 11] and Horn-SROIQ [13] are
layer for the architecture of the Semantic Web.
notable, with considerable rich sets of allowed
As
reasoning
in
SROIQ
has
a
very
high
constructors and features.
Combinations of rule
complexity, W3C also recommended the profiles
languageslikeDatalogoritsextensionswithDLs
OWL 2 EL, OWL 2 QL and OWL 2 RL, which
have also been widely studied.
are based on the families of DLs EL [2, 3], DL-
To eliminate nondeterminism, all EL [2, 3],
Lite [4, 5] and DLP [6].
These families of DLs
DL-Lite [4, 5], DLP [6], Horn-SHIQ [7] and
are monotonic rule languages enjoying PTime
Horn-SROIQ [13] disallow (any form of) the
data complexity.
They are defined 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
However, a big challenge is faced: the bottom-up
ALCallowing8R:C atthelefthandsideofvhas
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
a consequence, the work [12] on Horn-Reg is
condition 8x9yR(x;y)), which complicates the
already complicated and the problem whether
construction of logically least models.
Horn-Reg has PTime data complexity remained
For many application domains,
the profiles
open until [17].
OWL2EL,OWL2QLandOWL2RLlanguages
This paper is a revised and extended version
and the underlying Horn fragments EL, DL-Lite,
of
our
conference
paper
[17].
In
this
work
DLP seem satisfactory.
However,
in general,
we study a Horn fragment called Horn-RegI of
forbidding 8R:C at the left hand side of v in
the regular description logic with inverse RegI.
terminological axioms is a serious restriction.
This fragment extends Horn-Reg with inverse
In [16] Nguyen introduced the deterministic
roles.
In
contrast
to
the
well-known
Horn
Horn fragment of ALC, where the constructor
fragments EL, DL-Lite, DLP, Horn-SHIQ and
8R:C
is
allowed
at
the
left
hand
side
of
v
Horn-SROIQ of description logics, Horn-RegI
in
the
combination
with
9R:C
(in
the
form
allows the concept constructor 89R:C to appear
8R:C u 9R:C,
denoted by 89R:C
[15]).
He
at the left hand side of terminological inclusion
proved
that
such
a
fragment
has
PTime
data
axioms.
We provide an algorithm with PTime
complexity by providing a bottom-up method for
data
complexity
for
checking
satisfiability
of
constructing a logically least pseudo-model for
Horn-RegI knowledge bases. The key idea is to
a given deterministic positive knowledge base
follow the top-down approach1 and use a special
in
the
restricted
language.
In
[12]
Nguyen
technique to deal with non-seriality of roles.
applied the method of [16] to regular DL Reg,
which extends ALC with regular role inclusion
axioms characterized by finite 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:
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
di erence 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
89hasChild:Happy v HappyParent
that:
89hasChild:Male v ParentWithOnlySons
89hasChild:Female v ParentWithOnlyDaughters
interestingu89path:interesting v perfect
interestingt89link:interesting v worth surfing:
 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
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
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];
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
 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.
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
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 flexibility for
optimizing the computation.
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 finite set of RIAs such
that
 The current paper provides full proofs for
fR ! S1 :::Sk j (S1 Sk v R) 2 Rg
the results as well as additional examples
and explanations.
is a symmetric regular semi-Thue system S over
R. We assume that R is given together with a
The rest of this paper is structured as follows.
In Section 2 we present notation and semantics
ofRegI andrecallautomaton-modaloperators. In
Section 3 we define the Horn-RegI fragment. In
Section 4 we present our algorithm of checking
satisfiability 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.
mapping A that associates every R 2 R with
a finite automaton AR recognizing the words
derivable from R using S. We call A the RIA-
automaton-specification of R.
Recall that a finite automaton A over alphabet
R is a tuple hR;Q;q0;;Fi, where Q is a finite
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 finite sequence of
states q0;q1;:::;qk such that (qi 1;Ri;qi) holds
2. Preliminaries
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
2.1. Notation and Semantics of RegI
an accepting run of A on w.
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
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:
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
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-specification A is specified by:
a finite set of context-free production rules over
alphabet R. It is symmetric if, for every rule
2In the case k = 0, the right hand sides of the rules stand
for ".
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  
13 lần xem

A horn fragment with ptime data complexity of regular description logic with inverse. 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 finite 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..

Nội dung

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 finite 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 satisfiability 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 profiles 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 defined 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 profiles 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 finite 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 surfing: 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 satisfiability 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 flexibility 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 define the Horn-RegI fragment. In Section 4 we present our algorithm of checking satisfiability 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 finite 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 finite 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 finite automaton AR recognizing the words derivable from R using S. We call A the RIA-automaton-specification of R. Recall that a finite automaton A over alphabet R is a tuple hR;Q;q0;;Fi, where Q is a finite 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 finite 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-specification A is specified 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 definition. 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 defined 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-specification. 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 defined 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 finite set of TBox axioms of the form C v D. An ABox is a finite 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. Define 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 satisfiable 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 finite automaton A over alphabet R, define 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 finite 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 defined 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 finite 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 finite automaton A then by Aq we denote the finite 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-specification 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 first 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 definition, 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 defined 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 defined 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 finite 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 finite 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 finite 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 “defines” path to be the transitive closure of link. As the RIA-automaton-specification of R we can take the mapping A such that: The data complexity class of Horn-RegI is defined to be the complexity class of the problem of checking satisfiability of a Horn-RegI knowledge base hR;T;Ai, measured in the size of A when assuming that R and T are fixed 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 unsatisfiable, 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 surfing: 3. KB can beiconverted in polynomial time in Let A be the ABox specified 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 satisfiable i KB0 is satisfiable. 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 surfing 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 first 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 satisfiable i KB is satisfiable. 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 satisfiable i KB0 is satisfiable. 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 first 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 defined then Next(x,∃R.C) := Find(Satr({C} ∪ Trans(Label(x),R)) ∪ T 0); 4. Checking Satisfiability 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-specification A of R, checks whether the knowledge base is satisfiable. 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), isdefined 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 satisfiability 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 defined 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 satisfiability in Horn-RegI Input: a clausal Horn-RegI knowledge base hR,T ,Ai

Tài liệu liên quan