Recently, Description Logics (DL) are used to represent and reason about knowledge bases (KBs). In practical applications, the monotonic property of standard logics, which includes DLs, may be undesirable.

Hence, we introduce ALCK N F , the DL of minimal knowledge and negation as failure (MKNF-DL) as an extension of description logic (DL) with modal operators K and A. Advanced reasoning applications, including epistemic queries, integrity constraints and default rules can be represented by ALCK N F [4].

Next, we introduce a reasoning technique for ALCK N F . To this end the representation of ALCK N F models is crucial. The models of ALCK N F are not first-order representable. Hence, we define subjectively quantified KBs which are representable by ALC theory. However, this ALC theory may be infinite. Previous approaches [1,3] defined simple KBs, a subset of subjectively quantified KBs, which are representable by finite ALC theory. The intention of our research was an effective reasoning method for subjectively quantified KB. We achieved this by introducing a tableaux algorithm with blocking; however, for the algorithm to be complete, a further restriction to minimality-proper KBs is neccessary. Still, minimality-proper KBs include simple KBs.

We start with usual formalism of MKNF-DL, which roughly follow Donini [1].

Definition 1 (ALCK N F Syntax) The ALCK N F syntax is defined as follows:

where C a is an atomic concept, C, C 1 , C 2 are concept expressions, R a is an atomic role, R is a role, and K and A are modal operators.

Definition 2 An ALCK N F concept C is subjective if each ALC atomic subconcept of C is also a subconcept of a modal subconcept of C. An ALCK N F concept C is objective if C does not contain a modal role or a modal subconcept. An ALCK N F concept C is mixed if C is neither subjective nor objective.

Objective concepts are the ALC concepts. For example, concept ∃KR.C is neither subjective nor objective.

The ALCK N F knowledge base (KB) is an extension of ALC KB to which we add the modal formulae.

Definition 3 (ALCK N F Knowledge Base) The ALCK N F knowledge base Σ is a triple T , Γ, A , 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 simplification of notation. We assume an ALCK N F KB Σ = T , Γ, A . M denotes a modal operator, i.e., M ∈ {K, A}, N denotes a possibly negated modal operator, i.e., N ∈ {K, A, ¬K, ¬A}. R a denotes an atomic ALC role, C a , D a denote atomic ALC concepts, A, B, C, D (possibly with indices or primes) denote arbitrary ALCK N F concepts. The ALCK N F interpretation (I, M, N ) is extended to non-atomic and modal concepts and modal roles as follows: A TBox T is satisfied in (M, N ), denoted as (M, N ) |= T , iff all axioms in T are satisfied in (M, N ). An MBox Γ is satisfied in (M, N ), denoted as (M, N ) |= Γ , iff all axioms in Γ are satisfied in (M, N ). An ABox A is satisfied in (M, N ), denoted as (M, N ) |= A, iff all assertions in A are satisfied in (M, N ). A KB Σ is satisfied in (M, N ), denoted as (M, N ) |= Σ, iff all T , Γ and A are satisfied in (M, N ).

Up to now, the definition of modal operators K and A were the same. Their meaning is distinguished by imposing the maximality condition on K. Definition 7 (ALCK N F Model) A set of ALC interpretations M is a model for an ALCK N F KB Σ iff the following two conditions hold:

(i) the structure (M, M) satisfies Σ; and (ii) for each set of ALC interpretations M , if M ⊃ M then the structure (M , M) does not satisfy Σ.

Definition 9 (Satisfiability) A KB Σ is satisfiable if there is a model for Σ. Two KBs Σ and Σ are equivalent, denoted as Σ ≡ Σ , iff for every set of ALC interpretations M, M is model for

Our intention is to introduce a reasoning technique for ALCK N F . This will be attained in the next section. In this section, we discuss the representation of ALCK N F models.

In our treatment of representing and reasoning in ALCK N F we follow several approaches to reasoning in propositional modal logic [2,5,6].

The reasoning problem for ALCK N F is reduced to several reasoning problems in the underlying nonmodal logic ALC. Each model for an ALCK N 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 ALCK N F .

Recall that an ALCK N F model M is a set of ALC interpretations. The model M is first-order representable if there exists a first-order theory (resp. ALC KB)

Therefore the set of interpretations belonging to M can be represented by a first-order theory Σ M . Note that the theory Σ M may be either finite or infinite. Following the motivation of this approach, we consider only the case when the ALCK N F model M is ALC representable, i.e. there exists an ALC KB Σ M such that M = {I : I |= Σ M }. Moreover, we consider only the case when the corresponding Σ M is finite. Since ALC is a fragment of first-order logic, if M is ALC representable then M is also first-order representable.

To guarantee ALC representability of ALCK N F KB models, the KB is restricted to a subjectively quantified KB. In previous publications [1,3], a subjectively quantified KB is further restricted to simple KB whose models admit a representation in terms of finite ALC KB and guarantee decidability of reasoning (specifically termination of the tableaux algorithm). This progress is depicted in Figure 1.

The approach of subjectively quantified KBs and simple KBs was first introduced and extensively analysed in Donini et al. [1]. A further research was done by Ke et al. [3]. We now compare both papers and explain our approach.

First, Donini et al. [1] claim that the models of ALCK N F KBs cannot be characterized by first-order theories. In previous publications [1,3], to obtain a reasoning algorithm, the language of KBs was syntactically restricted to subjectively quantified and then to simple KB. In this thesis, we provide a reasoning algorithm that works with subjectively quantified KBs. Since our approach does not require the simple restriction, it allows reasoning over greater set of KBs.

Theorem 10 The models of ALCK N F are not first-order representable.

Briefly, the proof considers a carefully constructed ALCK N F KB Σ, shows a model M for Σ, and shows that M cannot be characterized in terms of firstorder theory.

Second, they identify a subset of ALCK N F KBs whose models are firstorder representable by means of (either finite or infinite) first-order theories. This is achieved by the notion of subjectively quantified KBs. We consider two definitions from previous papers [1,3].

Definition 11 (Subjectively Quantified KB) A subjectively quantified ALCK N F KB is an ALCK N F KB Σ such that each concept C of the form ∃R.D or ∀R.D satisfies one of the following conditions:

(i) R is an ALC role and D is an ALC concept; (ii) R is of the form MR a and D is subjective.

To summarize, the Definition 11 by [3] is more general than similar definition by [1], and we use it for the rest of this paper. However the difference between the definitions has no implications for the tableaux algorithm, since the algorithm considers the flatten normal forms of formulae (created in preprocessing stage).

Theorem 12 A subjectively quantified ALCK N F KB is representable by an (either finite or infinite) ALC theory.

Briefly, the proof shows that the models of a subjectively quantified ALCK N 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 quantified ALCK N F KB.

In previous publications [1,3], authors further restrict ALCK N F KBs to obtain a finite characterization of models (that are also first-order representable). This is achieved by the notion of simple KBs.

In the following, we say that an ALCK N F concept is simple if C is subjectively quantified and each quantified concept subexpression of the form ∃AR.ND, ∀AR.ND, where N ∈ {K, ¬K, A, ¬A}, occurring in C is such that in D there are no occurrences of role expressions of the form KR.

Definition 13 (Simple KB) A simple ALCK N F KB Σ = T , Γ, A is an ALCK N F KB that satisfies the following conditions:

(i) Γ is a set of ALCK N F simple inclusions, i.e. inclusions assertions of the form KC D, where C is an ALC-concept such that T |= C, and D is a subjectively quantified concept expression in which there are no occurrences of the operator K within the scope of quantifiers; and (ii) A is a set of instance assertions such that all concept subexpressions occurring in A are simple.

Ke et al. [3] significantly loosens the definition of a simple KB by allowing more concept assertions in A. Both [1,3] conclude with a proof of the following theorem.

Theorem 14 A simple ALCK N F KB is representable by a finite ALC theory.

We present a reasoning algorithm for deciding the satisfiability of a subjectively quantified ALCK N F KB. We use a novel tableaux algorithm with a blocking technique to deal with modal part of ALCK N F theory.

In standard DLs, the tableaux algorithm tests satisfiability 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 infinite and therefore the tableaux algorithm uses a blocking technique that identifies infinite branches. This allows to represent the infinite models by finitely-representable models.

The main motivation of our approach is analogous: the the infinite models of ALCK N F can be blocked and represented by finitely-representable ALCK N F models.

In our approach, we reduce the reasoning problem for ALCK N F to several reasoning problems in ALC. Since each model for a subjectively quantified ALCK N 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 ALCK N F .

In this section we define the tableaux algorithm that tests the satisfiability of a subjectively quantified ALCK N F KB Σ = T , Γ, A .

The reader is referred to Malenko et al. [4] for detailed treatment and proofs of theorems in this section.

Since every ALCK N F KB can be translated to flatten normal form, we assume w.l.o.g. the Σ to be in flatten normal form.

The satisfiability 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 finite subsets of modal atoms. A branch satisfying certain conditions corresponds to a model for Σ.

The ALCK N F tableaux algorithm is similar to a standard ALC tableaux algorithm. However, the are differences: Only modal assertions are decomposed by the ALCK N 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 ALCK N F concept description.

The tableaux starts with an initial branch B 0 = {KC(x) | C(x) ∈ A}. 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 O B .

We now briefly describe the ALCK N F expansion rules and compare them with standard DL tableaux rules [1]:

-The -rule is analogous to the the corresponding DL tableaux rule.

-The -rule adds both disjuncts (as they are or possibly negated) to the tableaux, because they are needed in the minimality check. The for parts of the rule consider all the cases that can happen; the part (d) detect and inconsistency and enforces a clash in the underlying DL reasoner. In the corresponding DL tableaux rule, either of the conjunct is added to the tableaux. -The ∃-rule is analogous to the the corresponding DL tableaux rule.

-The ∀-rule has two parts. The first part deals with modal roles and is analogous to DL tableaux rule. The second part deals with the relationship between KR(x, y) and AR(x, y). In the tableaux algorithm, the "value" of AR(x, y) is by default "false" until the appearance of KR(x, y) supporting it to be "true" (this is possible since AR(x, y)

-The trigger-rule takes Γ into account. The underlying DL reasoner is used to check that C(a) is entailed in K-objective knowledge, which represents "what is known so far" by T and B.

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 ∃-rule to individual x, the algorithm keeps track of the relationship and we define parent(y) = x. Then, predcessor is transitive closure of parent.

-rule:

and {C(x), D(x)} ⊆ B, then add C(x), D(x) to B.

-rule:

If C D(x) ∈ B we distinguish the following four cases:

∃-rule:

and {MR(x, y), C(y)} ⊆ B for any y ∈ OB, and x is not blocked by some y ∈ OB, then add MR(x, z), C(z) to B, for some z ∈ OB ∪ {i}, where i ∈ OB.

We distinguish the following two cases: 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 first 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 first individual. When no expansion rules are applicable the tableaux algorithm ends. An effective implementation of this strategy can be achieved by keeping track of tableaux changes and proper backtracking (backjumping).

Definition 16 (Completed Branch) We say a branch B is completed if no expansion rules from Figure 2 are applicable to B.

Definition 17 ((P B , N B )) The partition (P B , N B ) associated with a branch B is defined as follows:

Here, P B is a set of atoms which are true, N B is a set of atoms which are false. Atoms not in P B ∪ N B are assumed to be false.

Definition 18 (Objective Knowledge) Let B be a branch for Σ. The ALC KB

The objective knowledge is an ALC KB passed to an underlying ALC reasoner to check a certain set of conditions.

Definition 19 (Open Branch) A branch B is open if all of the following conditions hold:

If there is an open branch B for Σ, then there is an ALCK N F structure (M, N ) that satisfies Σ.

Definition 20 (Pre-preferred Branch) A branch B is pre-preferred if all of the following conditions hold:

If there is a pre-preferred branch B for Σ, then there is an ALCK N F structure (M, M) that satisfies Σ.

If minimality condition does not hold, there exists a structure (M , M) such that M ⊃ M and (M , M) satisfies Σ. This implies that M is not a model for Σ.

For the tableaux algorithm with this minimality condition to be complete [3], KBs must be restricted according to the following definition. ) can replace M to ensure that (M , M) |= Σ. This purpose would not be achieved if there were assertions of the form ∀AR.C(x) ∈ B because there could exist R(x, y) such that Ob K (B) |= R(x, y) and Ob A (f (B )) |= 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 B does not contain AR(x, y), C(y) and all the assertions obtained from C(y). For analogous reason the minimality-proper KBs forbid ∃AR.E in disjunctions. We prove later that for the minimality-proper KBs, the minimality check is correct.

Definition 23 (Preferred Branch) A branch B is preferred if all of the following conditions hold: (i) B is pre-preferred; (ii) B satisfies the minimality condition.

If there is a preferred branch B for Σ, then there is an ALCK N F structure (M, M) that satisfies Σ and for each set of interpretations M , if M ⊃ M then (M , M) does not satisfy Σ. We conclude that B is a model for Σ.

Lemma 24 (Termination) Let Σ be a subjectively quantified and minimalityproper ALCK N F KB. Then the tableaux algorithm for checking satisfiability of Σ always terminates. Theorem 26 (Decidability) Let Σ be a subjectively quantified and minimality-proper ALCK N F KB. Then the satisfiability problem of Σ is decidable.

For reasoning in ALCK N 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 quantified and minimality-proper. This is a larger class of KBs than in previous approaches, which further restricted to simple KBs.