Description Logics (DLs) are a family of knowledge representation languages that have gained considerable attention the last 20 years. It is wellknown that the interpretation domain of classical DLs is a classical set. However, in Science and in the ordinary life the situation is not at all like this. In order to handle these types of knowledge in DLs, in this paper we present a DL framework based on multiset theory. Concretely, we present the DL over multisets ALCmsets which is a semantic extension of the classical DL ALC. The syntax and semantics of ALCmsets are presented. Moreover, we investigate the logical properties of ALCmsets and provide a sound and terminating reasoning algorithm for satisfiability problem of ALCmsets.
In the last 20 years a substantial amount of work has been carried out in the
context of Description Logics (DLs for short) [
From the semantics of DLs [
As a matter of fact, in order to process the collections with repetition, multi-set
theory (MST for short) has been presented and several operations as the addition, the
union and the intersection of multisets have been defined and their properties
investigated in several papers [
Naturally, a problem is raised: how we can interpret the concepts and the roles of DLs using multi-set theory? Furthermore, what are the benefits of doing so? After careful thought, we find that it is feasible to interpret the concepts and the roles of DLs using multi-set theory. Moreover, it is a more accurate interpretation for the concepts and the roles of DLs. For example, when we interpret the concept commended-students (students who are commended), we can say that Zhangsan, Lisi and Wangwu are the instances of the concept commended-students. More formally, we can say commended-studentsI={Zhangsan, Lisi, Wangwu} in classical DLs. However, if we consider more accurate situation, e.g., Zhangsan is commended three times, Lisi is commended twice, and Wangwu is commended once, obviously, the classical interpretation of DLs cannot process this situation. Here we can interpret the concept commended-students using multi-set theory. Formally, commendedstudentsMI={Zhangsan, Zhangsan, Zhangsan, Lisi, Lisi, Wangwu}, where {Zhangsan, Zhangsan, Zhangsan, Lisi, Lisi, Wangwu} is a multiset.
In this paper we extend DLs allow to express that interpretation of a concept
(resp., a role) is not a subset of classical set (traditional interpretation domain DI)
(resp., a subset of DI´DI) like in classical DLs, but a subset of multisets (resp., a subset
of Cartesian product of multisets). That is, we will extend the interpretation domain of
DLs to multisets. More concretely, we will present the DL ALCmsets, which is a
semantic extension of the DL ALC [
A naive concept of multiset was formalized by Blizard [
A collection of elements containing duplicates is called a multiset. Formally, if X is a set of elements, a multiset M drawn from the set X is represented by a function count M or CM: X®N where N represents the set of non-negative integers. For each xÎX, CM(x) is the characteristic value of x in M and indicates the number of occurrences of the element x in M. A multiset M is a set if "xÎX, CM(x)=0 or 1.
The word “multiset” often shortened to “mset” abbreviates the term “multiple membership set”.
Let M1 and M2 be two msets drawn from a set X. M1 is a sub mset of M2 (M1ÍM2) if "xÎX, CM1(x)£CM2(x). M1 is a proper sub mset of M2 (M1ÌM2) if CM1(x)£CM2(x) "xÎX and there exists at least one "xÎX such that CM1(x)<CM2(x). Two msets M1 and M2 are equal (M1=M2) if M1ÍM2 and M2ÍM1. An mset M is empty if "xÎX, CM(x)=0. The cardinality of an mset M drawn from a set X is Card M=SxÎXCM(x). It is also denoted by |M|.
The insertion of an element x into an mset M results in a new mset M¢ denoted by M¢=MÅx such that CM¢(x)=CM(x)+1 and CM¢(y)=CM(y) "y¹x. Addition of two msets M1 and M2 drawn from a set X results in a new mset M=M1ÅM2 such that "xÎX, CM(x)=CM1(x)+CM2(x). The removal of an element x from an mset M results in a new mset M¢ denoted by M¢=MQx such that CM¢(x)= max{CM(x)-1, 0} and CM¢(y)=CM(y) "y¹x. Subtraction of two msets M1 and M2 drawn from a set X results in a new mset M=M1QM2 such that "xÎX, CM(x)=max{CM1(x)-CM2(x), 0}. The union of two msets M1 and M2 drawn from a set X is an mset M denoted by M=M1ÈM2 such that "xÎX, CM(x)=max{CM1(x), CM2(x)}. The intersection of two msets M1 and M2 drawn from a set X is an mset M denoted by M=M1ÇM2 such that "xÎX, CM(x)=min{CM1(x), CM2(x)}.
Let M be an mset from X with x appearing n times in M. It is denoted by xÎnM. M={k1/x1, k2/x2, …, kn/xn} where M is an mset with x1 appearing k1 times, x2 appearing k2 times and so on. [M]x denotes that the element x belongs to the mset M and |[M]x| denotes the cardinality of an element x in M. The entry of the form (m/x, n/y)/k denotes that x is repeated m times, y is repeated n times and the pair (x, y) is repeated k times. C1(x, y) denotes the count of the first co-ordinate in the ordered pair (x, y) and C2(x, y) denotes the count of the second co-ordinate in the ordered pair (x, y).
The mset space Xn is the set of all msets whose elements are in X such that no element in the mset occurs more than n times. The set X¥ is the set of all msets over a domain X such that there is no limit to the number of occurrences of an element in an mset. If X={x1, x2, …, xk} then Xn= {{n1/x1, n2/x2, …, nn/xn} | for i=1, 2, …, k; niÎ{0, 1, 2, …, n}}.
Let X be a support set and Xn be the mset space defined over X. Then for any mset MÎXn, the complement Mc of M in Xn is an element of Xn such that "xÎX, CMc(x)=n-CM(x).
Let M1 and M2 be two msets drawn from a set X, then the Cartesian product of M1 and M2 is defined as M1´M2={(m/x, n/y)/mn | xÎmM1, yÎnM2}. The Cartesian product of three or more nonempty msets can be defined by generalizing the definition of the Cartesian product of two msets. Thus the Cartesian product M1´M2´…´Mn of the nonempty msets M1, M2, …, Mn is the mset of all ordered ntuples (m1, m2, …, mn) where miÎriMi, i=1, 2, …, n and (m1, m2, …, mn)Îp M1´M2´…´Mn with p=Õri, where ri=CMi(mi), and i=1, 2, …, n.
A sub mset R of M´M is said to be an mset relation on M if every member (m/x, n/y) of R has a count C1(x, y).C2(x, y). We denote m/x related to n/y by m/xRn/y.
The domain and range of the mset relation R on M is defined as follows: Dom R={xÎrM | $yÎsM such that r/xRs/y} where CDomR(x)=sup{C1(x, y) | xÎrM}, Ran R={yÎsM | $xÎrM such that r/xRs/y} where CRanR(y)=sup{C2(x, y) | yÎsM}. 3
The ALCmsets DL
In the current section we will present the description logic over multisets ALCmsets,
which is a semantic extension of the ALC [
As usual, we consider an alphabet of distinct concept names (C), role names (R)
and individual names (I). The abstract syntax of ALCmsets-concepts and ALCmsets-roles is
the same as that of ALC [
In the following, we give the semantics of ALCmsets-concepts and ALCmsets-roles formally.
An mset interpretation is a pair MI = (ΔMI, ·MI), where ΔMI is a non-empty mset (the interpretation domain), and ·MI is an interpretation function that assigns each atomic concept (concept name) AÎC to a set AMIÍΔMI, each atomic role (role name) RÎR (note that in ALCmsets roles are always atomic) to a binary relation RMIÍΔMI´ΔMI, and each individual name m/aÎI to an element aMIÎmΔMI. This interpretation function is extended to ALCmsets concept descriptions as follows: l l l l l l l ⊤MI=ΔMI; ⊥MI=f; (ØC)MI=ΔMIQCMI; (C⊓D)MI=CMIÇDMI; (C⊔D)MI=CMIÈDMI; ($R.C)MI={aÎmΔMI| $bÎnΔMI, (m/a, n/b)ÎmnRMI Ù bÎnCMI}; ("R.C)MI={aÎmΔMI| "bÎnΔMI, (m/a, n/b)ÎmnRMI ® bÎnCMI}.
Note that in this paper we restrict the interpretation domain to be finite. This is not a severe limitation as it is hard to imagine an application involving infinite interpretation domains.
An ALCmsets knowledge base KB is also composed of a TBox and an ABox. A TBox T is a finite, possibly empty, set of terminological axioms that could be a combination of concept inclusions of the form áC⊑Dñ and concept equations of the form áCºDñ, where C and D are concept descriptions. An mset interpretation MI satisfies áC⊑Dñ if CMIÍDMI, and it satisfies áCºDñ if CMI=DMI (i.e., CMIÍDMI and DMIÍCMI). An mset interpretation MI satisfies a TBox T iff MI satisfies every axiom in T; in this case, we say that MI is a model of T.
An ABox A includes of a set of mset assertions that could be a combination of concept assertions of the form ám/a:Cñ and role assertions of the form á(m/a, n/b):Rñ, where a and b are individuals, C is a concept, and R is a role. An mset interpretation MI satisfies ám/a:Cñ if aMIÎmCMI, and it satisfies á(m/a, n/b):Rñ if (m/aMI, n/bMI)ÎmnRMI. An mset interpretation MI satisfies an ABox A iff MI satisfies every mset assertion in A w.r.t. a TBox T; in this case, we say that MI is a model of A w.r.t. T.
An mset interpretation MI satisfies (or is a model of) a knowledge base KB=áT, Añ (denoted MI⊨KB), iff it satisfies both components of KB; in this case, we say that MI is a model of KB. The knowledge base KB is consistent if there exists an mset interpretation MI that satisfies KB. We say KB is inconsistent otherwise.
Description logics over multisets should provide their users with reasoning capabilities that allow them to derive implicit knowledge from the one explicitly represented. In the following we will define the most important reasoning problems of the ALCmsets DL.
Let T be a TBox, A an ABox, C, D concept descriptions, and a an individual name. The definitions of the main reasoning problems of the ALCmsets DL are as follows: l l l l
C is subsumed by D w.r.t. T (áC⊑TDñ) iff CMIÍDMI for all models MI of T; C is equivalent to D w.r.t. T (áCºTDñ) iff CMI=DMI for all models MI of T; C is satisfiable w.r.t. T iff CMI¹f for some model MI of T; A is consistent w.r.t. T iff it has a model that is also a model of T; l m/a is an instance of C w.r.t. A and T (A⊨Tám/a:Cñ) iff aMIÎmCMI for all models MI of T and A.
One might think that, in order to realize the reasoning component of an ALCmsets system, one need to design and implement five algorithms, each solving one of the above reasoning problems. Fortunately, this is not the case since there exist some polynomial time reductions (see Section 3.2). 3.2
It can be easily shown that ALCmsets is a sound extension of ALC, in the sense that the mset interpretations coincide with the traditional interpretations if we restrict the interpretation domain ΔMI to a classical set. However, since ALCmsets is based on multiset theory, some properties which are different from ALC are obtained. Of course, some properties are the same as that of ALC. In the following, we will discuss these properties.
The first ones are straightforward: áØ⊤º⊥ñ, áØ⊥º⊤ñ, áC⊓⊤ºCñ, áC⊔⊥ºCñ, áC⊓⊥º⊥ñ, áC⊔⊤º⊤ñ and á$R.⊥º⊥ñ, where C is a concept, R is a role.
The following properties show that some interesting equivalences hold in ALCmsets.
Proposition 1. Let C, C1, C2, C3 and D be five concepts. Then (1) áØØCºCñ, áC⊓CºCñ, áC⊔CºCñ; (2) áØ(C⊓D)ºØC⊔ØDñ, áØ(C⊔D)ºØC⊓ØDñ; (3) áC1⊔(C2⊓C3)º(C1⊔C2)⊓(C1⊔C3)ñ, áC1⊓(C2⊔C3)º(C1⊓C2)⊔(C1⊓C3)ñ.
Note 1. Please note that the following properties are satisfied in ALC, however, these properties are not satisfied in ALCmsets:
á(C⊓ØC)º⊥ñ, á(C⊔ØC)º⊤ñ, á"R.⊤º⊤ñ, áØ("R.C)º$R.ØCñ, áØ($R.C)º "R.ØCñ, á($R.C)⊔ ($R.D)º$R.(C⊔D)ñ, and á("R.C)⊓("R.D)º"R.(C⊓D)ñ.
There are two interesting remarks here. Firstly, in ALC, we can assume concepts to be in negation normal form (NNF), i.e., negation signs occur immediately in front of concept names only. However, in ALCmsets, we cannot do this translation due to áØ("R.C)≢$R.ØCñ and áØ($R.C) ≢"R.ØCñ. Secondly, in ALC, an ABox A contains a clash iff {A(a), ØA(a)}ÍA for some individual name a and some concept name A. However, in ALCmsets, we cannot use this definition due to á(C⊓ØC)≢⊥ñ and á(C⊔ØC)≢⊤ñ. For example, let ΔMI={6/a, 8/b} and {á3/a:Cñ, á4/b:Cñ}ÍA. Since á3/a:Cñ and á4/b:Cñ, then we have á3/a:ØCñ, á4/b:ØCñÎA. That is, {á3/a:Cñ, á3/a:ØCñ, á4/b:Cñ, á4/b:ØCñ}ÍA.
The properties of the polynomial time reductions for reasoning problems are as follows.
Proposition 2. Let T be a TBox, A an ABox, C, D concept descriptions, and a an individual name. Then (1) áC⊑TDñ iff áC⊓DºTCñ; (2) áCºTDñ iff áC⊑TDñ and áD⊑TCñ; (3) C is satisfiable w.r.t. T iff not áC⊑T⊥ñ; (4) C is satisfiable w.r.t. T iff there exist m>0 and individual a such that {ám/a:Cñ} is consistent w.r.t. T; (5) A is consistent w.r.t. T iff A⊭Tám/a:⊥ñ for any m>0 and individual a.
Note 2. It needs to be noted that the polynomial time reductions for instance problem to (in)consistency (i.e., A⊨Tám/a:Cñ iff AÈ{ám/a:ØCñ} is inconsistent w.r.t. T) and subsumption problem to (un)satisfiability (i.e., áC⊑TDñ iff C⊓ØD is unsatisfiable w.r.t. T), are satisfied in ALC, however, these reductions are not satisfied in ALCmsets.
Lastly, we have to point out that in the rest of this paper we only consider unfoldable TBoxes. More concretely, a concept definition is of the form áAºCñ where A is a concept name and C is a concept description. Given a set T of concept definitions, we say that the concept name A directly uses the concept name B if T contains a concept definition áAºCñ such that B occurs in C. Let uses be the transitive closure of the relation “directly uses”. We say that T is cyclic if there is a concept name A that uses itself, and acyclic otherwise. A TBox T is a finite, possibly empty, set of terminological axioms of the form áA⊑Cñ, called inclusion introductions, and of the form áAºCñ, called equivalence introductions. A TBox is unfoldable if it contains no cycles and contains only unique introductions, i.e., terminological axioms with only concept names appearing on the left hand side and, for each concept name A, there is at most one axiom in T of which A appears on the left side.
In classical DLs [
In DLs over msets such as ALCmsets presented in this paper, we also can prove that a knowledge base with an unfoldable TBox can be transformed into an equivalent one with an empty TBox.
Firstly, we can transform an ALCmsets-TBox T into a regular ALCmsets-TBox T¢, containing equivalence introductions only, such that T¢ is equivalent to T in a sense that will be specified below. We obtain T¢ from T by choosing for every concept inclusion introduction áA⊑Cñ in T a new concept name A¢ and by replacing the inclusion introduction áA⊑Cñ with the equivalence introduction áAºA¢⊓Cñ. The TBox T¢ is the normalization of T.
Now we show that T and T¢ are equivalent.
Proposition 3. Let T be a TBox and T¢ its normalization. Then (1) Every model of T¢ is a model of T.
(2) For every model MI of T there is a model MI¢ of T¢ that has the same domain as MI and agrees with MI on the concept names and roles in T.
Thus, in theory, inclusion introductions do not add to the expressivity of TBoxes.
However, in practice, they are a convenient means to introduce concepts into a TBox
that cannot be defined completely. In fact, this case is the same as classical DLs [
Now we show that, if T is an unfoldable TBox, we can always reduce reasoning problems w.r.t. T to problems w.r.t. the empty TBox. Instead of saying “w.r.t. f” one usually says “without a TBox”, and omits the index T for subsumption, equivalence, and instance, i.e., writes º, ⊑, ⊨ instead of ºT, ⊑T, and ⊨T. As we have seen in Proposition 3, T is equivalent to its expansion T¢. Recall that in the expansion every equivalence introduction áAºDñ such that D contains only concept names, but no concept descriptions. Now, for each concept description C we define the expansion of C w.r.t. T as the concept description C² that is obtained from C by replacing each occurrence of a concept name A in C by the concept description D, where áAºDñ is the equivalence introduction of A in T¢, the expansion of T.
Proposition 4. Let T be an unfoldable TBox, C, D concept descriptions, C² expansion of C, and D² expansion of D. Then (1) áCºTC²ñ; (2) C is satisfiable w.r.t. T iff C² is satisfiable; (3) áC⊑TDñ iff áC²⊑D²ñ; (4) áCºTDñ iff áC²ºD²ñ. 4
In this section, we will provide a detailed presentation of the reasoning algorithm for the ALCmsets-satisfiability problem and the properties for the termination and soundness of the procedure. There is one point we have to point out here. Since we restrict the maximal number of occurrences of an element (i.e., an individual) in a multiset (i.e., subset of interpretation domain), it is obvious to know that the satisfiability reasoning algorithm (see below) is incomplete.
In the following, we will present a tableau algorithm for testing satisfiability of an ALCmsets-concept. Before we can describe the tableau-based satisfiability algorithm for ALCmsets more formally, we need to introduce some basic notions firstly.
A constraint (denoted by a) is an expression of the form ám/a:Cñ, or á(m/a, n/b):Rñ, where a and b are individuals, C is a concept, and R is a role. Our calculus, determining whether a finite set S of constraints or not, is based on a set of constraint propagation rules transforming a set S of constraints into “simpler” satisfiability preserving sets Si until either all Si contain a clash (indicating that from all the Si no model of S can be build) or some Si is completed and clash-free, that is, no rule can further be applied to Si and Si contains no clash (indicating that from Si a model of S can be build). A set of constraints S contains a clash iff {ám/a:Cñ, á0/a:Cñ}ÍS for some m>0, individual a, and concept description C.
The ®Ø-rule
Condition: Si contains ám/a:ØCñ, but it does not contain á1/a:Cñ, á2/a:Cñ, …, or ánmax-m/a:Cñ.
Action: Si,1=SiÈ{á1/a:Cñ}, Si,2=SiÈ{á2/a:Cñ}, …, Si,nmax-m=SiÈ{ánmax-m/a:Cñ}. The ®⊓-rule
The ®⊔-rule Condition: Si contains ám/a:C1⊓C2ñ, but neither {ám/a:C1ñ, áj/a:C2ñ} nor {ám/a:C2ñ, áj/a:C1ñ}, where m£j£nmax.
Action: Si,1¢=SiÈ{ám/a:C1ñ, ám/a:C2ñ}, Si,2¢=SiÈ{ám/a:C1ñ, ám+1/a:C2ñ}, ..., Si,nmax+1¢ =SiÈ{ám/a:C1ñ, ánmax/a:C2ñ}, Si,1²=SiÈ{ám/a:C2ñ, ám/a:C1ñ}, Si,2²=SiÈ {ám/a:C2ñ, ám+1/a: C1ñ}, ..., Si,nmax+1²=SiÈ{ám/a:C2ñ, ánmax/a:C1ñ}.
Condition: Si contains ám/a:C1⊔C2ñ, but neither {ám/a:C1ñ, áj/a:C2ñ} nor {ám/a:C2ñ, áj/a:C1ñ}, where 1£j£m.
Action: Si,1¢=SiÈ{ám/a:C1ñ, ám/a:C2ñ}, Si,2¢=SiÈ{ám/a:C1ñ, ám-1/a:C2ñ}, ..., Si,m¢= SiÈ{ám/a:C1ñ, á1/a:C2ñ}, Si,1²=SiÈ{ám/a:C2ñ, ám/a:C1ñ}, Si,2²=SiÈ{ám/a: C2ñ, ám-1/a:C1ñ}, ..., Si,m²= SiÈ{ám/a:C2ñ, á1/a:C1ñ}.
The ®$-rule Condition: Si contains ám/a:$R.Cñ, but there are no individuals 1/b, 2/b, …, nmax/b such that á1/b:Cñ and á(m/a, 1/b):Rñ, á2/b:Cñ and á(m/a, 2/b): Rñ, …, or ánmax/b:Cñ and á(m/a, nmax/b):Rñ are in Si.
Action: Si,1=SiÈ{á1/b:Cñ, á(m/a, 1/b):Rñ}, Si,2=SiÈ{á2/b:Cñ, á(m/a, 2/b):Rñ}, …, Si,nmax=SiÈ {ánmax/b:Cñ, á(m/a, nmax/b):Rñ}, where 1/b, 2/b, ..., nmax/b are individuals not occurring in Si.
The ®"-rule
Condition: Si contains ám/a:"R.Cñ and á(m/a, n/b):Rñ, but it does not contain án/b:Cñ.
Action: Si¢=SiÈ{án/b:Cñ}.
The tableau-based satisfiability algorithm for ALCmsets works as follows. Let C by an ALCmsets-concept. In order to test satisfiability of C, the algorithm starts with a finite set of constraints {S1, S2, …, Snmax}, and applies satisfiability preserving transformation rules (see Figure 1) (in arbitrary order) to the set of constraints Si (1£i£nmax) until no more rules apply, where S1={á1/a:Cñ}, S2={á2/a:Cñ}, …, Snmax= {nmax/a:C}. If the “complete” constraint obtained this way does not contain an obvious contradiction (called clash), then S is consistent (and thus C is satisfiable), and inconsistent (unsatisfiable) otherwise. The transformation rules that handle negation, conjunction, disjunction, and exists restrictions are non-deterministic in the sense that a given set of constraints is transformed into finitely many new sets of constraints such that the original set of constraints is consistent iff one of the new sets of constraints is so. For this reason we will consider finite sets of constraints S={S1, S2, …, Sk} instead of the original set of constraints {S1, S2, …, Snmax}, where k³nmax. Such a set is consistent iff there is some i, 1£i£k, such that Si is consistent. A rule of Figure 1 is applied to a given finite set of constraints S as follows: it takes an element Si of S, and replaces it by one set of constraints Si¢, by two sets of constraints Si¢ and Si², or by finitely many sets of constraints Si,j.
Proposition 5 (Termination). Let C be an ALCmsets-concept. There cannot be some infinite sequences of rule applications
{áj/a:Cñ}®S1®S2®…, where 1£j£nmax.
Proof. The main reasons for this proposition to hold are the following. (1) The original sets of constraints {áj/a:Cñ} is finite. Namely, there exist nmax original sets of constraints {á1/a:Cñ}, {á2/a:Cñ}, …, {ánmax/a:Cñ}.
(2) Without loss of generality, we consider the original set of constraints {áj/a:Cñ}. Let S¢ be a set of constraints contained in Si for some i³1. For every individual m/b¹j/a occurring in S¢, there is a unique sequence R1, …, Rk (k³1) of role names and a unique sequence of individuals of the form 1/b1, 1/b2, …, 1/bk-1, or 1/b1, 1/b2, …, 2/bk-1, …, or 1/b1, 1/b2, …, nmax/bk-1, …, or nmax/b1, nmax/b2, …, nmax/bk-1, such that {á(j/a, 1/b1):R1ñ, á(1/b1, 1/b2):R2ñ, …, á(1/bk-1, m/b):Rkñ}ÍS¢, {á(j/a, 1/b1):R1ñ, á(1/b1, 1/b2):R2ñ, …, á(2/bk-1, m/b):Rkñ}ÍS¢, …, or {á(j/a, nmax/b1):R1ñ, á(nmax/b1, nmax/b2):R2ñ, …, á(nmax/bk-1, m/b):Rkñ}ÍS¢. In this case, we say that m/b occurs on the level k in S¢.
(3) If ám/b:C¢ñÎS¢ for an individual m/b on level k, then the maximal role depth of C¢ (i.e., the maximal nesting of constructors involving roles) is bounded by the maximal role depth of C minus k. Consequently, the level of any individual in S¢ is bounded by the maximal role depth of C.
(4) If ám/b:C¢ñÎS¢, then C¢ is a subdescription of C. Consequently, the number of different concept assertions on m/b is bounded by the size of C.
(5) The number of different role successors of m/b in S¢ (i.e., individuals l/c such that á(m/b, l/c):RñÎS¢ for a role name R) is bounded by the number of different existential restrictions in C.
Proposition 6 (Soundness). Assume that S¢ is obtained from the finite set of constraints S by application of a transformation rule. If S is consistent, then S¢ is consistent.
Proof. [Sketch] Given the termination property (see Proposition 5), it is easily verified, by case analysis, that the transformation rules of the satisfiability algorithm are sound. For example, the ®Ø-rule: Assume that MI is an mset interpretation satisfying ám/a:ØCñ, where 0<m£nmax. Let us show that MI satisfies á1/a:Cñ, á2/a:Cñ, …, or ánmax-m/a:Cñ. Since MI satisfies ám/a:ØCñ, by the semantics of ØC we have that aÎm(ØC)MI=ΔMIQCMI. Since the maximal number of occurrences of a in ΔMI is nmax, thus, by the definition of subtraction of two msets, we know that the number of occurrences of a in CMI is 1, 2, …, or nmax-m. That is, aÎ1CMI, aÎ2CMI, …, or aÎnmax-mCMI. Therefore, MI satisfies á1/a:Cñ, á2/a:Cñ, …, or ánmax-m/a:Cñ. 5
We present a DL framework based on multiset theory. Our main feature is that we extend classical DLs allow to express that interpretation of a concept (resp., a role) is not a subset of classical set (resp., a subset of Cartesian product of sets) like in classical DLs, but a subset of multisets (resp., a subset of Cartesian product of multisets). To the best of our knowledge, this is the first attempt in this direction.
Current research effort is to implement the reasoning algorithm and to perform an empirical evaluation in real scenarios. An interesting topic of future research is to study the complexity and optimization techniques of reasoning in DLs over multisets such as ALCmsets. Furthermore, additional research effort can be focused on the reasoning algorithms for the (very) expressive DLs over multisets such as SROIQmsets. Acknowledgments. The works described in this paper are supported by The National Natural Science Foundation of China under Grant No. 60663001; The Foundation of the State Key Laboratory of Computer Science of Chinese Academy of Sciences under Grant No. SYSKF0904; The Natural Science Foundation of Guangdong Province of China under Grant No. 10151063101000031; The Natural Science Foundation of Guangxi Province of China under Grant No. 0991100.