To support nonmonotonic reasoning we introduce the description logic of minimal knowledge and negation as failure (MKNF-DL) as an extension of description logic with modal operators K and A. We discuss the problems with representation of a model for an MKNF-DL theory. For satis ability checking of MKNF-DL theories, we introduce a tableaux algorithm with blocking, where blocking works with the modal part of an MKNF-DL theory. This blocking technique allows for reasoning about a larger class of MKNF-DL theories than previous approaches.
We start with usual formalism of MKNF-DL, which roughly follow Donini [
Syntax De nition 1 (ALCKN F Syntax) The ALCKN F syntax is de ned as follows: C ::= > j ? j Ca j :C j C1 u C2 j C1 t C2 j 9R:C j 8R:C j KC j AC R ::= Ra j KR j AR where Ca is an atomic concept, C; C1; C2 are concept expressions, Ra is an atomic role, R is a role, and K and A are modal operators.
De nition 2 An ALCKN F concept C is subjective if each ALC atomic subconcept of C is also a subconcept of a modal subconcept of C. An ALCKN F concept C is objective if C does not contain a modal role or a modal subconcept. An ALCKN F concept C is mixed if C is neither subjective nor objective.
Objective concepts are the ALC concepts. For example, concept 9KR:C is neither subjective nor objective.
The ALCKN F knowledge base (KB) is an extension of ALC KB to which we add the modal formulae.
De nition 3 (ALCKN F Knowledge Base) The ALCKN F knowledge base is a triple hT ; ; Ai, where TBox T is a set of objective axioms, MBox is a set of non-objective axioms, and ABox A is a set of (both objective and nonobjective) assertions.
In the remainder we consider the following simpli cation of notation. We assume an ALCKN F KB = hT ; ; Ai. M denotes a modal operator, i.e., M 2 fK; Ag, N denotes a possibly negated modal operator, i.e., N 2 fK; A; :K; :Ag. Ra denotes an atomic ALC role, Ca; Da denote atomic ALC concepts, A; B; C; D (possibly with indices or primes) denote arbitrary ALCKN F concepts. 1.2
Semantics Remind, that an ALC interpretation I = ( ; I ) consists of domain and interpretation function I which maps each atomic concept Ca to a subset of domain: CaI , each atomic role Ra to a subset of cartesian product of domain: RaI , and each individual name x to an element of domain: xI 2 .
The semantics of ALCKN F considers sets of ALC interpretations with the following properties: (i) The domain is a countable (possibly in nite) set. (ii) All ALC interpretations are de ned over the same domain . (iii) Each individual name in every interpretation maps to the same domain element.
De nition 4 (ALCKN F Semantics) An ALCKN F interpretation is a triple (I; M; N ), where I is an ALC interpretation ( ; I ), and M and N are sets of ALC interpretations.
Atomic concepts Ca, roles Ra, and individuals a are interpreted in I as usual in ALC: (Ca)I;M;N = CaI (Ra)I;M;N = RaI
(a)I;M;N = aI :
The ALCKN F interpretation (I; M; N ) is extended to non-atomic and modal concepts and modal roles as follows: (>)I;M;N = (?)I;M;N = ; (:C)I;M;N = n (C)I;M;N (C1 u C2)I;M;N = (C1)I;M;N \ (C2)I;M;N (C1 t C2)I;M;N = (C1)I;M;N [ (C2)I;M;N (9R:C)I;M;N = fx 2 j 9y 2 : (x; y) 2 (R)I;M;N ^ y 2 (C)I;M;N g (8R:C)I;M;N = fx 2 j 8y 2 : (x; y) 2 (R)I;M;N ) y 2 (C)I;M;N g (KC)I;M;N = T (C)J ;M;N (AC)I;M;N = TJ 2M(C)J ;M;N (KRa)I;M;N = TJ 2N (Ra)J ;M;N (ARa)I;M;N = TJ 2M(Ra)J ;M;N
J 2N De nition 5 (Satis ability in (I, M, N )) A concept inclusion C v D is satis ed in (I, M, N ), denoted as (I; M; N ) j= C v D, i CI;M;N DI;M;N . A concept assertion C(a) is satis ed in (I, M, N ), denoted as (I; M; N ) j= C(a), i a 2 CI;M;N . A role assertion R(a; b) is satis ed in (I, M, N ), denoted as (I; M; N ) j= R(a; b), i (a; b) 2 RI;M;N .
De nition 6 (Satis ability in (M, N )) A concept inclusion C v D is satis ed in (M, N ), denoted as (M; N ) j= C v D, i CI;M;N DI;M;N for each I 2 M. A concept assertion C(a) is satis ed in (M, N ), denoted as (M; N ) j= C(a), i a 2 CI;M;N for each I 2 M. A role assertion R(a; b) is satis ed in (M, N ), denoted as (M; N ) j= R(a; b), i (a; b) 2 RI;M;N for each I 2 M.
A TBox T is satis ed in (M, N ), denoted as (M; N ) j= T , i all axioms in T are satis ed in (M; N ). An MBox is satis ed in (M, N ), denoted as (M; N ) j= , i all axioms in are satis ed in (M; N ). An ABox A is satis ed in (M, N ), denoted as (M; N ) j= A, i all assertions in A are satis ed in (M; N ). A KB is satis ed in (M, N ), denoted as (M; N ) j= , i all T , and A are satis ed in (M; N ).
Up to now, the de nition of modal operators K and A were the same. Their meaning is distinguished by imposing the maximality condition on K. De nition 7 (ALCKN F Model) A set of ALC interpretations M is a model for an ALCKN F KB i the following two conditions hold: (i) the structure (M; M) satis es ; and (ii) for each set of ALC interpretations M0, if M0 (M0; M) does not satisfy .
M then the structure De nition 8 (Entailment) A concept inclusion C v D is a consequence of KB , denoted as j= C v D, i (M; M) j= C v D for each model M of . A concept assertion C(a) is a consequence of KB , denoted as j= C(a), i (M; M) j= C(a) for each model M of . A role assertion R(a; b) is a consequence of KB , denoted as j= R(a; b), i (M; M) j= R(a; b) for each model M of .
De nition 9 (Satis ability) A KB is satis able if there is a model for . Two KBs and 0 are equivalent, denoted as 0, i for every set of ALC interpretations M, M is model for i M is model for 0. Two concepts C and C0 are equivalent in KB , denoted as j= C C0, i for every set of ALC interpretations M of , M j= C v C0 and M j= C0 v C. 2
Model Representation Our intention is to introduce a reasoning technique for ALCKN F . This will be attained in the next section. In this section, we discuss the representation of
In our treatment of representing and reasoning in ALCKN F we follow several
approaches to reasoning in propositional modal logic [
The reasoning problem for ALCKN F is reduced to several reasoning problems in the underlying nonmodal logic ALC. Each model for an ALCKN F KB is characterized by an ALC KB. Therefore, the set of ALC KBs that represents all the models of constitute a nonmodal representation of . Such a representation allows for using classical reasoning techniques for ALC to solve the reasoning problems for ALCKN F .
Recall that an ALCKN F model M is a set of ALC interpretations. The model M is rst-order representable if there exists a rst-order theory (resp. ALC KB) M such that
M = fI : I j=
Mg: Therefore the set of interpretations belonging to M can be represented by a rst-order theory M. Note that the theory M may be either nite or in nite.
Following the motivation of this approach, we consider only the case when the ALCKN F model M is ALC representable, i.e. there exists an ALC KB M such that M = fI : I j= Mg. Moreover, we consider only the case when the corresponding M is nite. Since ALC is a fragment of rst-order logic, if M is ALC representable then M is also rst-order representable.
To guarantee ALC representability of ALCKN F KB models, the KB is
restricted to a subjectively quanti ed KB. In previous publications [
The approach of subjectively quanti ed KBs and simple KBs was rst
introduced and extensively analysed in Donini et al. [
First, Donini et al. [
ALCKN F KBs not rst-order representable
- Subjectively quanti ed to gAuaLraCntee ALCKN F KBs representability
Simple representation ALCKN F KBs
finite representation by nite ALC KBs decidable
Brie y, the proof considers a carefully constructed ALCKN F KB , shows a model M for , and shows that M cannot be characterized in terms of rstorder theory.
Second, they identify a subset of ALCKN F KBs whose models are
rstorder representable by means of (either nite or in nite) rst-order theories.
This is achieved by the notion of subjectively quanti ed KBs. We consider two
de nitions from previous papers [
De nition 11 (Subjectively Quanti ed KB) A subjectively quanti ed ALCKN F KB is an ALCKN F KB such that each concept C of the form 9R:D or 8R:D satis es one of the following conditions: (i) R is an ALC role and D is an ALC concept; (ii) R is of the form MRa and D is subjective.
To summarize, the De nition 11 by [
Brie y, the proof shows that the models of a subjectively quanti ed ALCKN F KB can be characterized in terms of an ALC KB. The characterization relies on the notion of modal atom: there is a one-to-one correspondence between certain sets of modal atoms and the models of subjectively quanti ed ALCKN F KB. 2.1
Previous Work
In previous publications [
In the following, we say that an ALCKN F concept is simple if C is subjectively quanti ed and each quanti ed concept subexpression of the form 9AR:ND, 8AR:ND, where N 2 fK; :K; A; :Ag, occurring in C is such that in D there are no occurrences of role expressions of the form KR. De nition 13 (Simple KB) A simple ALCKN F ALCKN F KB that satis es the following conditions: KB = hT ; ; Ai is an (i) is a set of ALCKN F simple inclusions, i.e. inclusions assertions of the form KC v D, where C is an ALC-concept such that T 6j= > v C, and D is a subjectively quanti ed concept expression in which there are no occurrences of the operator K within the scope of quanti ers; and (ii) A is a set of instance assertions such that all concept subexpressions occurring in A are simple.
Ke et al. [
Theorem 14 A simple ALCKN F KB is representable by a nite ALC theory. 2.2
Our Approach We present a reasoning algorithm for deciding the satis ability of a subjectively quanti ed ALCKN F KB. We use a novel tableaux algorithm with a blocking technique to deal with modal part of ALCKN F theory.
In standard DLs, the tableaux algorithm tests satis ability of a concept description. The algorithm starts with a concept description and applies consistency-preserving expansion rules that build a tree representing a model. In the tree, the nodes correspond to individuals and are labelled with sets of DL concept descriptions the individual belongs to.
The models of standard DL KBs can be in nite and therefore the tableaux algorithm uses a blocking technique that identi es in nite branches. This allows to represent the in nite models by nitely-representable models.
The main motivation of our approach is analogous: the the in nite models of ALCKN F can be blocked and represented by nitely-representable ALCKN F models. 3
Reasoning by Tableaux Algorithm with Blocking In our approach, we reduce the reasoning problem for ALCKN F to several reasoning problems in ALC. Since each model for a subjectively quanti ed ALCKN F KB can be represented by a set of ALC KBs, this allows us to use classical reasoning techniques for ALC to solve reasoning problems in ALCKN F .
In this section we de ne the tableaux algorithm that tests the satis ability of a subjectively quanti ed ALCKN F KB = hT ; ; Ai.
The reader is referred to Malenko et al. [
Since every ALCKN F KB can be translated to atten normal form, we assume w.l.o.g. the to be in atten normal form.
The satis ability problem for is solved by a tableaux algorithm for . The tableaux algorithm is trying to construct a model for by means of branches which correspond to nite subsets of modal atoms. A branch satisfying certain conditions corresponds to a model for .
The ALCKN F tableaux algorithm is similar to a standard ALC tableaux algorithm. However, the are di erences: Only modal assertions are decomposed by the ALCKN F tableaux algorithm, including the GCIs in . An ALC reasoner is used as an underlying reasoner, which considers T and ALC assertions through the so-called objective knowledge of a branch. The ALC reasoner is called in the conditions of trigger-rule and testing the conditions of models (open branch, pre-preferred branch, minimality condition).
A branch B is a set of membership assertions of the form C(x), where C is an ALCKN F concept description.
The tableaux starts with an initial branch B0 = fKC(x) j C(x) 2 Ag. New branches are obtained from the current branch by applying the tableaux expansion rules from Figure 2. We use :_C to denote the negation normal form of the :C. The set of individuals appearing in B is denoted by OB.
We now brie y describe the ALCKN F expansion rules and compare them
with standard DL tableaux rules [
To employ a blocking technique, the algorithm keeps ordering of individual names according to time of their introduction to tableaux algorithm. Moreover, for each individual y that is introduced into the tableaux by application of the 9-rule to individual x, the algorithm keeps track of the relationship and we de ne parent(y) = x. Then, predcessor is transitive closure of parent. u-rule: t-rule:
If C u D(x) 2 B,
and fC(x); D(x)g 6 B, then add C(x); D(x) to B.
If C t D(x) 2 B we distinguish the following four cases: (a) if fC(x); :_C(x); D(x); :_D(x)g \ B = ;,
then add either C(x); D(x) or C(x); :_D(x) or :_C(x); D(x) to B. (b) if fC(x); :_C(x)g \ B = ; and fD(x); :_D(x)g \ B 6= ;,
then add either C(x) or :_C(x) to B. (c) if fC(x); :_C(x)g \ B 6= ; and fD(x); :_D(x)g \ B = ;,
then add either D(x) or :_D(x) to B. (d) if f :_C(x); :_D(x)g B,
then add C(x) to B.
If 9MR:C(x) 2 B, and fMR(x; y); C(y)g 6 B for any y 2 OB, and x is not blocked by some y 2 OB, then add MR(x; z); C(z) to B, for some z 2 OB [ fig, where i 62 OB.
We distinguish the following two cases: (a) if 8MR:C(x) 2 B,
then for each MR(x; y) 2 B, if C(y) 62 B then add C(y) to B. (b) if 8AR:C(x) 2 B,
then for each KR(x; y) 2 B, if AR(x; y) 62 B then add AR(x; y) to B. trigger -rule:
If KCa v D 2 ; x 2 OB; ObK(B) j= Ca(x),
and fKCa(x); D(x)g 6 B, then add KCa(x); D(x) to B. De nition 15 (Blocking) The application of an expansion rule to an individual x is blocked in a branch B if there is a predecessor y of x and a predecessor z of y such that fC j C(y) 2 Bg = fC j C(z) 2 Bg.
The idea behind blocking is that the blocked individual x can use role successors of y instead of generating new ones. The ordering of individual names according to time of their introduction to tableaux algorithm is considered to avoid cyclic blocking (of x by y and vice versa).
To guarantee termination of this blocking technique, the following strategy for application of expansion rules to the individuals in a branch is used: all rules are applied to the rst introduced individual until no more rules apply, then all rules are applied to the second introduced individual until no more rules apply, etc. When a rule is successfully applied to an individual, the rule applications start again from the rst individual. When no expansion rules are applicable the tableaux algorithm ends. An e ective implementation of this strategy can be achieved by keeping track of tableaux changes and proper backtracking (backjumping).
De nition 16 (Completed Branch) We say a branch B is completed if no expansion rules from Figure 2 are applicable to B.
De nition 17 ((PB; NB)) The partition (PB; NB) associated with a branch B is de ned as follows:
PB = fMC(x) j MC(x) 2 Bg [ fMR(x; y) j MR(x; y) 2 Bg
NB = fMC(x) j :MC(x) 2 Bg
Here, PB is a set of atoms which are true, NB is a set of atoms which are false. Atoms not in PB [ NB are assumed to be false.
De nition 18 (Objective Knowledge) Let B be a branch for KB . The ALC ObK(B) = hT ; fC(x) j KC(x) 2 PBg [ fRa(x; y) j KRa(x; y) 2 PBgi ObA(B) = hT ; fC(x) j AC(x) 2 PBg [ fRa(x; y) j ARa(x; y) 2 PBgi is called K-objective, resp. A-objective, knowledge for B.
The objective knowledge is an ALC KB passed to an underlying ALC reasoner to check a certain set of conditions.
De nition 19 (Open Branch) A branch B is open if all of the following conditions hold: (i) ObK(B) is satis able; (ii) ObA(B) is satis able; (iii) ObK(B) 6j= C(x) for each KC(x) 2 NB; (iv) ObA(B) 6j= C(x) for each AC(x) 2 NB.
De nition 20 (Pre-preferred Branch) A branch B is pre-preferred if all of the following conditions hold: (i) B is completed and open; (ii) ObK(B) j= ObA(B); (iii) ObK(B) 6j= C(x) for each AC(x) 2 NB.
If there is a pre-preferred branch B for , then there is an ALCKN F structure (M; M) that satis es .
The minimality condition below checks whether the set of interpretations M = fI j I j= ObK(B)g represents a model for . The minimality condition checks the minimality of a branch up to the renaming of individuals introduced by the 9-rule.
For a branch B and an injection f , the branch obtained from B by replacing each occurrence of individual x by f (x) for each x 2 O nOB, is called a renamed branch of B and denoted f (B).
De nition 21 (Minimality Condition) Let B be a completed branch for . B satis es the minimality condition if there does not exist a completed and open branch B0 for and an injection f : OB0 nO ! OB nO such that jOB0 j jOBj and all of the following conditions hold: (i) ObK(B) j= ObK(f (B0)); (ii) ObK(f (B0)) 6j= ObK(B); (iii) ObK(B) j= ObA(f (B0)); (iv) ObK(B) 6j= C(x) for each AC(x) 2 Nf(B0).
If minimality condition does not hold, there exists a structure (M0; M) such that M0 M and (M0; M) satis es . This implies that M is not a model for .
For the tableaux algorithm with this minimality condition to be complete
[
For example, KC v KD t 9AR:C is not minimality-proper, while KC v 9AR:C is.
The minimality-proper condition prevents 8AR:C(x) to appear in B0 of the minimality condition 21. The fact the branch B0 is open implies that (M0; M00) j= , where M0 = fI j I j= ObK(B0)) and M00 = fI j I j= ObA(B0)). The purpose of conditions (iii) and (iv) in De nition 21 is to imply that M = fI j I j= ObK(B)) can replace M00 to ensure that (M0; M) j= . This purpose would not be achieved if there were assertions of the form 8AR:C(x) 2 B0 because there could exist R(x; y) such that ObK(B) j= R(x; y) and ObA(f (B0)) 6j= R(x; y), which does not meet the requirement of \assuming as much as we know from B". Because of the tableaux expansion rules, the branch B0 does not contain AR(x; y); C(y) and all the assertions obtained from C(y). For analogous reason the minimality-proper KBs forbid 9AR:E in disjunctions. We prove later that for the minimality-proper KBs, the minimality check is correct.
De nition 23 (Preferred Branch) A branch B is preferred if all of the following conditions hold: (i) B is pre-preferred; (ii) B satis es the minimality condition.
If there is a preferred branch B for , then there is an ALCKN F structure (M; M) that satis es and for each set of interpretations M0, if M0 M then (M0; M) does not satisfy . We conclude that B is a model for . Lemma 24 (Termination) Let be a subjectively quanti ed and minimalityproper ALCKN F KB. Then the tableaux algorithm for checking satis ability of always terminates.
To state completeness we must de ne what it means for a branch to represent a model. Let B be a completed branch for and M a model for . We de ne that B represents M if B is preferred and there exists an injection f : OB nO ! n O such that M = fI j I j= ObK(f (B))g holds.
Theorem 25 (Soundness and completeness) Let be a subjectively quanti ed and minimality-proper ALCKN F KB. Then is satis able if and only if there exists a preferred branch B of the tableaux for .
If B is a preferred branch for , then M = fI j I j= ObK(B)g is a model for . If M is a model for , then there exists a completed branch B for that represents M.
Theorem 26 (Decidability) Let be a subjectively quanti ed minimality-proper ALCKN F KB. Then the satis ability problem of decidable. and is 4 For reasoning in ALCKN F we presented a tableaux algorithm with blocking. The blocking is employed to deal with modal part of MKNF-DL theory. This technique allows for reasoning about KBs which are both subjectively quanti ed and minimality-proper. This is a larger class of KBs than in previous approaches, which further restricted to simple KBs.