=Paper=
{{Paper
|id=None
|storemode=property
|title=Nonmonotonic Reasoning in Description Logic by Tableaux Algorithm with Blocking
|pdfUrl=https://ceur-ws.org/Vol-846/paper_12.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/MalenkoS12
}}
==Nonmonotonic Reasoning in Description Logic by Tableaux Algorithm with Blocking==
https://ceur-ws.org/Vol-846/paper_12.pdf
Nonmonotonic Reasoning in Description Logic
by Tableaux Algorithm with Blocking
Jaromı́r Malenko and Petr Štěpánek
Charles University, Malostranske namesti 25, 11800 Prague, Czech Republic,
Jaromir.Malenko@mff.cuni.cz, Petr.Stepanek@mff.cuni.cz
Abstract. To support nonmonotonic reasoning we introduce the de-
scription 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 satisfiability 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 reason-
ing about a larger class of MKNF-DL theories than previous approaches.
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 ALCKN F , the DL of minimal knowledge and negation
as failure (MKNF-DL) as an extension of description logic (DL) with modal op-
erators K and A. Advanced reasoning applications, including epistemic queries,
integrity constraints and default rules can be represented by ALCKN F [4].
Next, we introduce a reasoning technique for ALCKN F . To this end the
representation of ALCKN F models is crucial. The models of ALCKN 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. Previ-
ous 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.
1 Basic Formalism
We start with usual formalism of MKNF-DL, which roughly follow Donini [1].
1.1 Syntax
Definition 1 (ALCKN F Syntax) The ALCKN F syntax is defined as follows:
C ::= > | ⊥ | Ca | ¬C | C1 u C2 | C1 t C2 | ∃R.C | ∀R.C | KC | AC
R ::= Ra | KR | 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.
Definition 2 An ALCKN F concept C is subjective if each ALC atomic subcon-
cept 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 ∃KR.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.
Definition 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 non-
objective) assertions.
In the remainder we consider the following simplification of notation. We
assume an ALCKN F KB Σ = hT , Γ, Ai. M denotes a modal operator, i.e.,
M ∈ {K, A}, N denotes a possibly negated modal operator, i.e., N ∈
{K, A, ¬K, ¬A}. 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 ∈ ∆.
The semantics of ALCKN F considers sets of ALC interpretations with the
following properties:
(i) The domain ∆ is a countable (possibly infinite) set.
(ii) All ALC interpretations are defined over the same domain ∆.
(iii) Each individual name in every interpretation maps to the same domain ele-
ment.
Definition 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 = ∆ \ (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
(∃R.C)I,M,N = {x ∈ ∆ | ∃y ∈ ∆ : (x, y) ∈ (R)I,M,N ∧ y ∈ (C)I,M,N }
(∀R.C)I,M,N = {xT ∈ ∆ | ∀y ∈ ∆ : (x, y) ∈ (R)I,M,N ⇒ y ∈ (C)I,M,N }
I,M,N J ,M,N
(KC) = TJ ∈M (C)
(AC)I,M,N = TJ ∈N (C)J ,M,N
(KRa )I,M,N = TJ ∈M (Ra )J ,M,N
(ARa )I,M,N = J ∈N (Ra )J ,M,N
Definition 5 (Satisfiability in (I, M, N )) A concept inclusion C v D is
satisfied in (I, M, N ), denoted as (I, M, N ) |= C v D, iff C I,M,N ⊆ DI,M,N .
A concept assertion C(a) is satisfied in (I, M, N ), denoted as (I, M, N ) |=
C(a), iff a ∈ C I,M,N . A role assertion R(a, b) is satisfied in (I, M, N ), denoted
as (I, M, N ) |= R(a, b), iff (a, b) ∈ RI,M,N .
Definition 6 (Satisfiability in (M, N )) A concept inclusion C v D is sat-
isfied in (M, N ), denoted as (M, N ) |= C v D, iff C I,M,N ⊆ DI,M,N for
each I ∈ M. A concept assertion C(a) is satisfied in (M, N ), denoted as
(M, N ) |= C(a), iff a ∈ C I,M,N for each I ∈ M. A role assertion R(a, b) is
satisfied in (M, N ), denoted as (M, N ) |= R(a, b), iff (a, b) ∈ RI,M,N for each
I ∈ M.
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 (ALCKN F Model) A set of ALC interpretations M is a model
for an ALCKN F KB Σ iff the following two conditions hold:
(i) the structure (M, M) satisfies Σ; and
(ii) for each set of ALC interpretations M0 , if M0 ⊃ M then the structure
(M0 , M) does not satisfy Σ.
Definition 8 (Entailment) A concept inclusion C v D is a consequence of
KB Σ, denoted as Σ |= C v D, iff (M, M) |= C v D for each model M
of Σ. A concept assertion C(a) is a consequence of KB Σ, denoted as Σ |=
C(a), iff (M, M) |= C(a) for each model M of Σ. A role assertion R(a, b) is a
consequence of KB Σ, denoted as Σ |= R(a, b), iff (M, M) |= R(a, b) for each
model M of Σ.
Definition 9 (Satisfiability) A KB Σ is satisfiable if there is a model for Σ.
Two KBs Σ and Σ 0 are equivalent, denoted as Σ ≡ Σ 0 , iff for every set of ALC
interpretations M, M is model for Σ iff M is model for Σ 0 . Two concepts C
and C 0 are equivalent in KB Σ, denoted as Σ |= C ≡ C 0 , iff for every set of
ALC interpretations M of Σ, M |= C v C 0 and M |= C 0 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
ALCKN F models.
In our treatment of representing and reasoning in ALCKN F we follow several
approaches to reasoning in propositional modal logic [2, 5, 6].
The reasoning problem for ALCKN F is reduced to several reasoning prob-
lems 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 repre-
sents 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 first-order representable if there exists a first-order theory (resp. ALC KB)
ΣM such that
M = {I : I |= ΣM }.
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 ALCKN 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 ALCKN F KB models, the KB is re-
stricted to a subjectively quantified KB. In previous publications [1, 3], a subjec-
tively 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 intro-
duced 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 ALCKN F KBs cannot be
characterized by first-order theories.
ALCKN F KBs - Subjectively quantified - Simple
to guarantee
ALC
ALCKN F KBs finite
representation
ALCKN F KBs
representability
not first-order representable representation by finite ALC KBs
decidable
Fig. 1. The structure of work on ALCKN F model representation. In previous publi-
cations [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 ALCKN F are not first-order representable.
Briefly, the proof considers a carefully constructed ALCKN F KB Σ, shows
a model M for Σ, and shows that M cannot be characterized in terms of first-
order theory.
Second, they identify a subset of ALCKN F KBs whose models are first-
order 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
ALCKN F KB is an ALCKN 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 MRa 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 ALCKN F KB is representable by an (ei-
ther finite or infinite) ALC theory.
Briefly, the proof shows that the models of a subjectively quantified 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 quantified ALCKN F KB.
2.1 Previous Work
In previous publications [1, 3], authors further restrict ALCKN 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 ALCKN F concept is simple if C is sub-
jectively 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 ALCKN F KB Σ = hT , Γ, Ai is an
ALCKN F KB that satisfies the following conditions:
(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 6|= > v 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 occur-
ring 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 ALCKN F KB is representable by a finite ALC theory.
2.2 Our Approach
We present a reasoning algorithm for deciding the satisfiability of a subjectively
quantified 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 satisfiability of a con-
cept 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 ALCKN F can be blocked and represented by finitely-representable ALCKN F
models.
3 Reasoning by Tableaux Algorithm with Blocking
In our approach, we reduce the reasoning problem for ALCKN F to several rea-
soning problems in ALC. Since each model for a subjectively quantified 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 define the tableaux algorithm that tests the satisfiability
of a subjectively quantified ALCKN F KB Σ = hT , Γ, Ai.
The reader is referred to Malenko et al. [4] for detailed treatment and proofs
of theorems in this section.
Since every ALCKN F KB can be translated to flatten normal form, we as-
sume 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 ALCKN F tableaux algorithm is similar to a standard ALC tableaux
algorithm. However, the are differences: 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 = {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 OB .
We now briefly describe the ALCKN F expansion rules and compare them
with standard DL tableaux rules [1]:
– The u-rule is analogous to the the corresponding DL tableaux rule.
– The t-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 cor-
responding 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 anal-
ogous to DL tableaux rule. The second part deals with the relationship be-
tween 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) ∈ M A∆ (Σ) it is supported
by ∀AR.C(x) ∈ M A∆ (Σ)).
– 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.
u-rule: If C u D(x) ∈ B,
and {C(x), D(x)} 6⊆ B,
then add C(x), D(x) to B.
t-rule: If C t D(x) ∈ B we distinguish the following four cases:
(a) if {C(x), ¬C(x),
˙ D(x), ¬D(x)}
˙ ∩ B = ∅,
then add either C(x), D(x) or C(x), ¬D(x)
˙ or ¬C(x),
˙ D(x) to B.
(b) if {C(x), ¬C(x)}
˙ ∩ B = ∅ and {D(x), ¬D(x)}
˙ ∩ B 6= ∅,
then add either C(x) or ¬C(x)
˙ to B.
(c) if {C(x), ¬C(x)}
˙ ∩ B 6= ∅ and {D(x), ¬D(x)}
˙ ∩ B = ∅,
then add either D(x) or ¬D(x)
˙ to B.
(d) if {¬C(x),
˙ ¬D(x)}
˙ ⊆ B,
then add C(x) to B.
∃-rule: If ∃MR.C(x) ∈ B,
and {MR(x, y), C(y)} 6⊆ 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 6∈ OB .
∀-rule: We distinguish the following two cases:
(a) if ∀MR.C(x) ∈ B,
then for each MR(x, y) ∈ B, if C(y) 6∈ B then add C(y) to B.
(b) if ∀AR.C(x) ∈ B,
then for each KR(x, y) ∈ B, if AR(x, y) 6∈ B then add AR(x, y) to B.
trigger -rule: If KCa v D ∈ Γ, x ∈ OB , ObK (B) |= Ca (x),
and {KCa (x), D(x)} 6⊆ B,
then add KCa (x), D(x) to B.
Fig. 2. Expansion rules for the tableaux algorithm of ALCKN F
Definition 15 (Blocking) The application of an expansion rule to an individ-
ual x is blocked in a branch B if there is a predecessor y of x and a predecessor
z of y such that {C | C(y) ∈ B} = {C | C(z) ∈ B}.
The idea behind blocking is that the blocked individual x can use role suc-
cessors 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 (back-
jumping).
Definition 16 (Completed Branch) We say a branch B is completed if no
expansion rules from Figure 2 are applicable to B.
Definition 17 ((PB , NB )) The partition (PB , NB ) associated with a branch B
is defined as follows:
PB = {MC(x) | MC(x) ∈ B} ∪ {MR(x, y) | MR(x, y) ∈ B}
NB = {MC(x) | ¬MC(x) ∈ B}
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.
Definition 18 (Objective Knowledge) Let B be a branch for Σ. The ALC
KB
ObK (B) = hT , {C(x) | KC(x) ∈ PB } ∪ {Ra (x, y) | KRa (x, y) ∈ PB }i
ObA (B) = hT , {C(x) | AC(x) ∈ PB } ∪ {Ra (x, y) | ARa (x, y) ∈ PB }i
is called K-objective, resp. A-objective, knowledge for B.
The objective knowledge is an ALC KB passed to an underlying ALC rea-
soner to check a certain set of conditions.
Definition 19 (Open Branch) A branch B is open if all of the following con-
ditions hold:
(i) ObK (B) is satisfiable;
(ii) ObA (B) is satisfiable;
(iii) ObK (B) 6|= C(x) for each KC(x) ∈ NB ;
(iv) ObA (B) 6|= C(x) for each AC(x) ∈ NB .
If there is an open branch B for Σ, then there is an ALCKN F structure
(M, N ) that satisfies Σ.
Definition 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) |= ObA (B);
(iii) ObK (B) 6|= C(x) for each AC(x) ∈ NB .
If there is a pre-preferred branch B for Σ, then there is an ALCKN F structure
(M, M) that satisfies Σ.
The minimality condition below checks whether the set of interpretations
M = {I | I |= ObK (B)} represents a model for Σ. The minimality condition
checks the minimality of a branch up to the renaming of individuals introduced
by the ∃-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 ∈ OΣ \OB , is called a renamed
branch of B and denoted f (B).
Definition 21 (Minimality Condition) Let B be a completed branch for Σ.
B satisfies the minimality condition if there does not exist a completed and open
branch B 0 for Σ and an injection f : OB0 \OΣ → OB \OΣ such that |OB0 | ≤ |OB |
and all of the following conditions hold:
(i) ObK (B) |= ObK (f (B 0 ));
(ii) ObK (f (B 0 )) 6|= ObK (B);
(iii) ObK (B) |= ObA (f (B 0 ));
(iv) ObK (B) 6|= C(x) for each AC(x) ∈ Nf (B0 ) .
If minimality condition does not hold, there exists a structure (M0 , M) such
that M0 ⊃ M and (M0 , 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.
Definition 22 (Minimality-proper KB) An ALCKN F KB is minimality-
proper if it satisfies the following condition: for each KC v D ∈ Γ and each
D(x) ∈ A
(i) D does not contain a subconcept of the form ∀AR.E; and
(ii) D does not contain a subconcept of the form ∃AR.E in a disjunction.
For example, KC v KD t ∃AR.C is not minimality-proper, while KC v
∃AR.C is.
The minimality-proper condition prevents ∀AR.C(x) to appear in B 0 of the
minimality condition 21. The fact the branch B 0 is open implies that (M0 , M00 ) |=
Σ, where M0 = {I | I |= ObK (B 0 )) and M00 = {I | I |= ObA (B 0 )). The purpose
of conditions (iii) and (iv) in Definition 21 is to imply that M = {I | I |=
ObK (B)) can replace M00 to ensure that (M0 , M) |= Σ. This purpose would not
be achieved if there were assertions of the form ∀AR.C(x) ∈ B 0 because there
could exist R(x, y) such that ObK (B) |= R(x, y) and ObA (f (B 0 )) 6|= 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 0 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 fol-
lowing 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 ALCKN F structure
(M, M) that satisfies Σ 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 quantified and minimality-
proper ALCKN F KB. Then the tableaux algorithm for checking satisfiability of
Σ always terminates.
To state completeness we must define what it means for a branch to represent
a model. Let B be a completed branch for Σ and M a model for Σ. We define
that B represents M if B is preferred and there exists an injection f : OB \OΣ →
∆ \ OΣ such that M = {I | I |= ObK (f (B))} holds.
Theorem 25 (Soundness and completeness) Let Σ be a subjectively quan-
tified and minimality-proper ALCKN F KB. Then Σ is satisfiable if and only if
there exists a preferred branch B of the tableaux for Σ.
If B is a preferred branch for Σ, then M = {I | I |= ObK (B)} 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 quantified and
minimality-proper ALCKN F KB. Then the satisfiability problem of Σ is
decidable.
4 Conclusion
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 quantified
and minimality-proper. This is a larger class of KBs than in previous approaches,
which further restricted to simple KBs.
References
1. Donini, F. M., Nardi, D., Rosati, R.: Description logics of minimal knowledge and
negation as failure. ACM Trans. Comput. Logic, 3(2):177–225, 2002.
2. Gottlob, G.: Complexity results for nonmonotonic logics. Journal of Logic and
Computation, (2):397–425, 1992.
3. Ke, P., Sattler, U.: Next steps for description logics of minimal knowledge and nega-
tion as failure. In Franz Baader, Carsten Lutz, and Boris Motik, editors, Description
Logics, volume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.
4. Malenko, J.: Reasoning in decription logics. Charles University in Prague, disser-
tation thesis, 2012.
5. Marek, V. W., Truszczynski, M.: Nonmonotonic logic: context-dependent reasoning.
Springer-Verlag, Berlin, 1993.
6. Niemela, I.: Autoepistemic logic as a unified basis for nonmonotonic reasoning.
1993.