# Optimised ExpTime Tableaux for𝒮

Authors: Jian Huang; Xinye Zhao; Jianxing Gong
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

This study proposes to adopt a novel tableau reasoning algorithm for the description logic𝒮
ℋ
ℐ
𝒩 with semantics based on a finite residuated De Morgan lattice. The syntax, semantics, and logical properties of this logic are given, and a sound, complete, and terminating tableaux algorithm for deciding fuzzy ABox consistency and concept satisfiability problem with respect to TBox is presented. Moreover, based on extended and/or completion-forest with a series of sound optimization technique for checking satisfiability with respect to a TBox in the logic, a new optimized ExpTime (complexity-optimal) tableau decision procedure is presented here. The experimental evaluation indicates that the optimization techniques we considered result in improved efficiency significantly.


---

## Body

## 1. Introduction

The fuzzy DL (Description Language) over lattice is a generalization of the crisp DL that uses the elements ofLas truth values, instead of just the Boolean true and false. Different to fuzzy DLs, elements of the rational unit interval provided a membership degree semantics for their concepts;Lis further generalized to address qualitative uncertainty reasoning (by relying, e.g., on {false,likelyfalse,unknown,likelytrue,true}) and quantitative uncertainty reasoning (by relying, e.g., on {
0
/
n
,
1
/
n
,
…
,
n
/
n
} (for an integern
>
1, in increasing order [1])).Several attempts have been made at usingL-fuzzy set semantics [2], but only a limited kind of semantics over lattices is considered, where conjunction and disjunction are interpreted through the lattice operatorsmeet andjoin, respectively. Borgwardt and Peñaloza considered the fuzzy logic 𝒜
ℒ
𝒞
ℐ with semantics based on a finite residuated lattice [3] and a complete De Morgan lattice equipped with at-norm operator [4]. Further, Borgwardt and Peñaloza analysed the consistency and satisfiability problems in the description logic 𝒮
ℋ
ℐ with semantics based on a complete residuated De Morgan lattice [5] and showed that concept satisfiability in 𝒜
ℒ
𝒞 under this semantics is undecidable, in general, even if a very simple class of infinite lattices is restricted.In this paper, we extend the more general description logicL-𝒮
ℋ
ℐ
𝒩, whereLis a complete De Morgan lattice equipped with at-norm operator. The fuzzy description logic L-𝒮
ℋ
ℐ
𝒩 is a generalization of the crisp description logic 𝒮
ℋ
ℐ
𝒩 that uses the elements of Las truth values instead of just the Boolean true and false. We study fuzzy variants of the standard reasoning problems like concept satisfiability and consistency with general concept inclusions (GCI) in this setting and proved that with the help of a tableaux-based algorithm satisfiability becomes decidable and the ExpTime complete if L is required to be finite.The main contributions of this work can be highlighted twofold as follows.(i)
It presented a novel tableau reasoning algorithm for the description logic𝒮
ℋ
ℐ
𝒩 with semantics based on a finite residuated De Morgan lattice.
(ii)
By combining a series of optimization techniques that can be applied to fuzzy DLL-𝒮
ℋ
ℐ
𝒩, our framework reduces the search space of the tableau algorithm more significantly to ExpTime complete.The paper is organized as follows. Section 2 introduces the syntax and semantics of the fuzzy description logic over latticesL-𝒮
ℋ
ℐ
𝒩 and discusses some logical properties of the logic. In Section 3, we give a detailed presentation of the reasoning algorithm for deciding the consistency and satisfiability of aL-𝒮
ℋ
ℐ
𝒩 ABox, provide the proofs for the termination, soundness, and completeness of the procedure, and address the computational aspect of reasoning in it. In Section 4 we extend the previous results by adding a wide variety of optimisations to achieving a high level of performance on tableau reasoning in expressive description logicL-𝒮
ℋ
ℐ
𝒩. Our empirical evaluation shows that the proposed optimisations result in significant performance improvements in Section 6. Finally, future research issues are outlined in Section 7.


## 2. The LogicL-𝒮
ℋ
ℐ
𝒩

In this section we introduce a residuated De Morgan lattice extension of theL-𝒮
ℋ
ℐ
𝒩 DL, creating theL-𝒮
ℋ
ℐ
𝒩 language. The fuzzy description logicL-𝒮
ℋ
ℐ
𝒩, which is the extension of 𝒜
ℒ
𝒞
L[4] andL-𝒮
ℋ
ℐ [5], withthe number restrictions constructor. AndL-𝒮
ℋ
ℐ
𝒩 is a generalization of the fuzzy description logicf-𝒮
ℋ
ℐ
𝒩.Definition 1 (syntax).
LetN
CandN
Rbe pairwise disjoint sets of concepts and role, and letN
R
+
⊆
N
R, N
R be a set of transitive role names. The complex roles areN
R
∪
{
R
-
∣
r
∈
N
R
}.L-𝒮
ℋ
ℐ
𝒩complex concepts are defined inductively by the following production rule, whereA
∈
N
Candsis a complex role:
(1)
C
:
=
A
∣
C
1
⊓
C
2
∣
C
1
⊔
C
2
∣
C
1
⟶
C
2
∣
¬
C
1
∣
∃
s
·
C
∣
∀
s
·
C
∣
⊤
∣
⊥
.A complex rolesistransitive if eithersor inverse ofsbelongs toN
R
+.Definition 2 (semantics).
For a residuated De Morgan latticeL, an L interpretation is now a pair ℐ
=
(
Δ
ℐ
,
·
ℐ
), whereΔ
ℐis the domain for the classical case and·
ℐis an interpretation function mapping: every concept name C a functionA
ℐ
:
Δ
ℐ
→
L and every role name r a functionr
ℐ
:
Δ
ℐ
×
Δ
ℐ
→
L. AnL-assertion is an expression 〈
a
:
C
⊳
ℓ
〉, a role assertion of the form〈
(
a
,
b
)
:
s
⊳
ℓ
〉, whereCis a concept,sis a complex role,a
,
bare individual names, ℓ
∈
L, and⊳
∈
{
≻
,
⪰
}.A finite set of assertions and terminological axioms is called aKnowledge Base (KB). A fuzzy knowledge baseΣconsists of a finite set of axioms organized in three parts: a fuzzy ABox 𝒜 (axioms about individuals), a fuzzy TBox 𝒯 (axioms about concepts), and a fuzzy RBox ℛ (axioms about roles); that is, Σ
=
(
𝒜
,
ℛ
,
𝒯
). An interpretation ℐ satisfies (is a model of) a KB Σ if and only if ℐ satisfies each element in Σ.An interpretationℐ satisfies the concept definition〈
A
≐
C
,
ℓ
〉 if and only if for all x
∈
Δ
ℐ,(
A
ℐ
(
x
)
⇒
C
ℐ
(
x
)
)
⊗
(
C
ℐ
(
x
)
⇒
A
ℐ
(
x
)
)
≥
ℓ. A general TBox is a finite set of GCIs.Σsatisfies the GCI〈
C
⊑
D
,
ℓ
〉 if and only if, for all x
∈
Δ
ℐ,C
ℐ
(
x
)
⇒
D
ℐ
(
x
)
≥
ℓ. An acyclic TBox is a finite set of concept definitions such that every concept name occurs at most once in the lefthand side of an axiom, and there is no cyclic dependency between definitions [6].The complete set of semantics is depicted in Table1. Particularly notice that existential and universal quantifiers are not dual to each other, and the implication constructor cannot be expressed in terms of the negation and conjunction.Table 1
Semantics ofL-𝒮
ℋ
ℐ
𝒩 concepts and L-𝒮
ℋ
ℐ
𝒩 roles.
Constructor
Syntax
Semantics
Top
⊤
⊤
ℐ
(
x
)
=
1
Bottom
⊥
⊥
ℐ
(
x
)
=
0
Conjunction
C
⊓
D
(
C
⊓
D
)
ℐ
(
x
)
=
C
ℐ
(
x
)
⊗
D
ℐ
(
x
)
Disjunction
C
⊔
D
(
C
⊔
D
)
ℐ
(
x
)
=
C
ℐ
(
x
)
⊕
D
ℐ
(
x
)
General negation
¬
C
(
¬
C
)
ℐ
(
x
)
=
~
C
ℐ
(
x
)
Implication
C
→
D
(
C
→
D
)
ℐ
(
x
)
=
C
ℐ
(
x
)
⇒
D
ℐ
(
x
)
Exists restriction
∃
s
·
C
∃
(
s
·
C
)
ℐ
(
x
)
=
∨
y
∈
△
ℐ
{
s
ℐ
(
x
,
y
)
⇒
C
ℐ
(
y
)
}
Value restriction
∀
s
·
C
∀
(
s
·
C
)
ℐ
(
x
)
=
∧
y
∈
△
ℐ
{
s
ℐ
(
x
,
y
)
⊗
C
ℐ
(
y
)
}
At-most restriction
(
≤
n
R
)
ℐ
(
x
)
(
≤
n
R
)
ℐ
(
x
)
=
∧
y
1
,
…
,
y
n
+
1
∨
i
=
1
n
+
1
{
~
R
ℐ
(
x
,
y
i
)
}
At-least restriction
(
≥
n
R
)
ℐ
(
x
)
(
≥
n
R
)
ℐ
(
x
)
=
∨
y
1
,
…
,
y
n
∧
i
=
1
n
{
R
ℐ
(
x
,
y
i
)
}Next, we will pay more attention to the problem of deciding satisfiability of a concept, especially computing the highest degree with which an individual may belong to a concept.Definition 3 (ℓ-satisfiable).
LetCbeL-𝒮
ℋ
ℐ
𝒩 concept descriptions, 𝒯 a TBox, and ℓ
∈
L. C is ℓ-satisfiable with respect to 𝒯 if there is a model ℐ of 𝒯such that∨
x
∈
Δ
ℐ
C
ℐ
(
x
)
≥
ℓ. The best satisfiability degree forCwith respect to 𝒯 is the largest ℓ such thatC is ℓ-satisfiable with respect to 𝒯.The notion of witnessed model for fuzzy DLs was first introduced by Hájek [7]. Witnessed models of fuzzy predicate logic are models in which each quantified formula is witnessed; that is, the truth value of a universally quantified formula is the minimum of the values of its instances and similarly for existential quantification (maximum) [8].Definition 4 (witnessed model).
Letn
∈
ℕ. A model I of an KBΣis n-witnessed if for everyx
∈
Δ
ℐ, every role s, and every concept C there are
(2)
∥
(
∀
s
·
C
)
ℐ
(
x
)
∥
M
=
in
f
b
∈
y
i
∥
s
ℐ
(
x
,
y
i
)
⊗
C
ℐ
(
y
i
)
∥
=
s
ℐ
(
x
,
b
)
⊗
C
ℐ
(
b
)
,
∥
(
∃
s
·
C
)
ℐ
(
x
)
∥
M
=
su
p
b
∈
y
i
∥
s
ℐ
(
x
,
y
i
)
⟹
C
ℐ
(
y
i
)
∥
=
s
ℐ
(
x
,
b
)
⟹
C
ℐ
(
b
)
.
The semantics of the quantifiers require the computation of a supremum or infimum of the membership degrees of a possibly infinite set of elements of the domain. Reasoning is usually restricted to witnessed models in order to obtain effective decision procedures [7]. SinceLis finite, we always have the n-witnessed model property for somen
∈
ℕ. On the basis of 𝒜
ℒ
𝒞
ℐ
L of [6], we have deduced Lemma 5.Lemma 5.
If the cardinality of the largest antichain of L is n, thenL-𝒮
ℋ
ℐ
𝒩has the n-witnessed model property.For simplification of the algorithm description, we considern
=
1. The algorithm and the proofs of correctness can easily be adapted for any othern
∈
ℕ.


## 3. Tableau Algorithm forL-𝒮
ℋ
ℐ
𝒩 DL

We assume that all concept descriptions are innegation normal form (NNF); that is, negation appears only in front of concept names. We will also abuse our notation by saying that a TBox 𝒯 is in NNF if all the concepts occurring in 𝒯 are in NNF. Moreover, we prove the decidability of theL-𝒮
ℋ
ℐ
𝒩 DL by providing a tableaux algorithm for deciding the standard DL inference problems.


### 3.1.L
-
𝒮
ℋ
ℐ
𝒩 Tableau

Since most of the inference services of fuzzy DLs can be reduced to the problem of consistency checking for ABoxes [9], here we discuss the approaches to deciding consistency of fuzzy DLs over finite residuated De Morgan lattices in the presence of GCIs. The algorithm we present can be seen as an extension of the tableau presented in [5] and is inspired by the well-known tableau algorithm forf-𝒮
ℋ
ℐ
𝒩 [10], which is the basis for several highly successful implementations.It is assumed thatLis finite, and we can accordingly restrict reasoning ton-witnessed models. In the lattice L
=
〈
ζ
,
⊲
,
⊳
〉,we employ the symbols⊲and⊳as a placeholder for the inequalities≺
,
⪯and≻
,
⪰ and the symbol ⋈ as a placeholder for all types of inequations. Furthermore we employ the symbols⊲
-
,
⊳
-and ⋈
-to denote their reflections.Definition 6.
For a fuzzy conceptC, we will denote bysub
(
C
)the set that containsCand it is closed under subconcepts ofC. The set of all subconcepts of concepts that appear within an ABox is denoted by sub(C). LetR
Abe the set of roles occurring in 𝒜 and ℛ together with their inverses, andI
𝒜is the set of individuals in 𝒜. A fuzzy tableauTforΣis a quadruple in(
S
,
𝒢
,
Υ
,
𝒱
), such that (i)
S is a nonempty set of individuals (nodes),
(ii)
𝒢:S
×
sub
(
A
)
→
ζmaps each element and concept, that is, a member ofsub
(
A
), to the degree of certainty of that element to the concept,
(iii)
Υ:R
Σ
×
S
×
S
→
ζmaps each role ofR
Aand pair of elements to the degree of certainty of the pair to the role,
(iv)
𝒱: maps individuals occurring inAto elements inS.
For alls
,
t
∈
S,C
,
D
∈
sub
(
A
), ℓ
∈
ζ, andR
∈
R
A,Tsatisfies the following. (1)
Σ
(
s
,
⊥
)
=
0,Σ
(
s
,
⊤
)
=
1for∀
s
∈
S.
(2)
If〈
¬
C
,
⋈
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⋈
-
,
~
ℓ
〉
∈
𝒢
(
s
).
(3)
If〈
C
⊓
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
).
(4)
If〈
C
⊔
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
).
(5)
If〈
C
⊔
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
).
(6)
If〈
C
⊓
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
).
(7)
If〈
∀
R
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
)and〈
〈
s
,
t
〉
,
⊳
′
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
〈
s
,
t
〉
,
⊳
-
,
~
ℓ
〉, then〈
∀
C
,
⊳
,
ℓ
〉
∈
𝒢
(
t
).
(8)
If〈
∀
R
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
)and〈
〈
s
,
t
〉
,
⊳
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
〈
s
,
t
〉
,
⊲
,
~
ℓ
〉, then〈
∀
C
,
⊲
,
ℓ
〉
∈
𝒢
(
t
).
(9)
If〈
∃
R
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), then there existst
∈
Ssuch that〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
R
)and〈
〈
s
,
t
〉
,
⊳
,
~
ℓ
〉, then〈
∀
C
,
⊳
,
ℓ
〉
∈
𝒢
(
t
).
(10)
If〈
∀
R
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), then there existst
∈
Ssuch that〈
〈
s
,
t
〉
,
⊲
-
,
~
ℓ
〉
∈
Υ
(
R
)and〈
〈
s
,
t
〉
,
⊲
,
~
ℓ
〉, then〈
∀
C
,
⊳
,
ℓ
〉
∈
𝒢
(
t
).
(11)
If〈
∃
s
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), and〈
〈
s
,
t
〉
,
⊳
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
s
·
C
,
⊲
,
ℓ
〉, for someR
⊑
*with  Trans(R), then〈
∃
s
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
).
(12)
If〈
∀
s
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), and〈
〈
s
,
t
〉
,
⊳
′
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
s
·
C
,
⊳
-
,
~
ℓ
〉, for someR
⊑
*with  Trans(R), then〈
∀
s
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
).
(13)
〈
〈
s
,
t
〉
,
⋈
,
ℓ
〉
∈
Υ
(
R
)if〈
〈
t
,
s
〉
,
⋈
,
ℓ
〉
∈
Υ
(
R
)
(
Inv
(
R
)
).
(14)
If〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
R
)andR
⊑
*
Sthen,〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
S
).
(15)
〈
≥
p
R
,
⊳
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
R
)
}
≥
p.
(16)
〈
≤
p
R
,
⊲
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊲
-
,
~
ℓ
〉
∈
Υ
(
R
)
}
≥
p
+
1.
(17)
〈
≥
p
R
,
⊲
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊳
,
ℓ
i
〉
∈
Υ
(
R
)
}
≤
p
-
1, conjugated with〈
〈
s
,
t
〉, ⊲
,
ℓ
〉.
(18)
〈
≤
p
R
,
⊳
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊳
′
,
ℓ
i
〉
∈
Υ
(
R
)
}
≤
p, conjugated with〈
〈
s
,
t
〉
,
⊳
-,~
ℓ
〉.
(19)
There do not exist two conjugated triples in any label of any individualx
∈
S.
(20)
If〈
a
:
C
⋈
ℓ
〉
∈
A, then〈
C
⋈
ℓ
〉
∈
𝒢
(
𝒱
(
a
)
).
(21)
If〈
(
a
,
b
)
:
R
⋈
ℓ
〉
∈
A, then〈
(
𝒱
(
a
)
,
(
𝒱
(
b
)
)
⋈
ℓ
〉
∈
Υ
(
R
).
(22)
Ifa
≠
b
∈
𝒜, then 𝒱
(
a
)
≠
𝒱
(
b
).Lemma 7.
AnL-𝒮
ℋ
ℐ
𝒩ABox 𝒜 is consistent with respect to ℛ if and only if there exists a fuzzy tableau for 𝒜 with respect to ℛ.Proof.
Similar to that of Lemma 6.5 of [11], here gives the proof of the Lemma 7. For the direction if T = (
S
,
𝒢
,
Υ
,
𝒱
) is a fuzzy tableau for an ABox 𝒜 with respect to ℛ, we can construct a fuzzy interpretation ℐ = (
Δ
ℐ
,
·
ℐ
)that is a model of 𝒜. Consider the following:
(3)
Δ
ℐ
=
S
,
a
ℐ
=
V
(
a
)
,
a
∈
ℐ
A
,
⊺
ℐ
=
𝒢
(
s
,
⊤
)
,
∀
s
∈
S
,
⊥
ℐ
=
𝒢
(
s
,
⊥
)
,
∀
s
∈
S
,
A
ℐ
=
𝒢
(
s
,
A
)
,
∀
s
∈
S
and
concept
names
A
.
For all roleR
∈
R
A,
(4)
R
ℐ
(
s
,
t
)
=
{
R
Υ
+
(
s
,
t
)
,
∀
〈
s
,
t
〉
∈
S
×
S
if
T
r
a
n
s
(
R
)
R
Υ
(
s
,
t
)
,
∀
〈
s
,
t
〉
∈
S
×
S
otherwise
,
whereR
Υ
(
s
,
t
)is a binary fuzzy relation defined asR
Υ
(
s
,
t
)
=
Υ
(
R
,
〈
s
,
t
〉
)for all∀
〈
s
,
t
〉
∈
S
×
S, andR
Υ
+
(
s
,
t
)represents its sup-min transitive closure [12]. The proof of this property is quite technical and omitted here. From all above properties, the interpretation of individuals and roles implies that ℐ satisfies each assertion in 𝒜 inductively.


### 3.2.  Constructing aL-𝒮
ℋ
ℐ
𝒩 Tableau

Like most of the tableaux algorithms, our algorithm works oncompletion forests rather than on completion trees which is applied in work [5]. As pointed out in [13], that is because an ABox might contain several individuals with arbitrary roles connecting them.Definition 8 (completion forest).
A completion forestℱ forΣis a collection of trees whose distinguished roots are arbitrarily connected by edges. Each nodexis labelled with a setΣ
(
x
)
=
{
〈
C
,
⋈
,
l
〉
}. Each edge〈
x
,
y
〉is labelled with a setΣ
(
〈
x
,
y
〉
)
=
{
〈
R
,
⋈
,
l
〉
}, whereR
∈
R
Aare roles and its inverse occurring in 𝒜. A completion forest comes with an explicit inequality relation≠on nodes and an explicit equality relation≐which are implicitly assumed to be symmetric. Given a completion forest, If nodesxandyare connected by an edge〈
v
,
w
〉with〈
R
,
l
〉occurring inΣ
(
〈
x
,
y
〉
), thenyis called anR-successorofxandxis called anR-predecessorofy. A nodexis a positive (resp., negative) successor (resp., predecessor or neighbour) ofy.A node is blocked if it is either directly or indirectly blocked. It is indirectly blocked if itsR-predecessor is either directly or indirectly blocked. A nodexis directly blocked if and only if none of its ancestors are blocked, and it has an ancestorysuch thatΣ
(
x
)
=
Σ
(
y
).A nodex is said to contain a clash satisfying one of the conditions such that if and only if there exist two conjugated triples inΣ
(
〈
x
,
y
〉
), or ifΣ
(
〈
x
,
y
〉
)
∪
{
〈
Inv
(
R
)
,
⋈
,
ℓ
〉
∣
〈
R
,
⋈
,
ℓ
〉
∈
Σ
(
〈
y
,
x
〉
)
} andx,y are root nodes, contains two conjugated triples. Table 2 shows all the entries under which condition the row column pair ofL-constraints is a
conjugated pair
(e.g.,
a
:
A
≻
uanda
:
A
⋡
vis a conjugated pair as¬
(
∃
v
·
v
≻
u
∧
v
⋡
v
)).Table 2
Conjugated pairs.
〈
α
⋡
l
′
〉
〈
α
≺
l
′
〉
〈
α
≻
l
〉
¬
(
∃
l
′
′
·
l
′
′
≻
l
∧
l
′
′
⋡
l
′
)
l
⊀
l
′
〈
α
⋠
l
〉
¬
(
∃
l
′
′
·
l
′
′
⋠
l
∧
l
′
′
⋡
l
′
)
¬
(
∃
l
′
′
·
l
′
′
⋠
l
∧
l
′
′
≺
l
′
)The calculus is based on a set of constraint propagation rules transforming a setSinto satisfiability preserving setsS
iuntil either one ofS
icontains an inconsistency (clash), or someS
iis completed and clash-free; that is, no rule can further be applied toS
iandS
icontains no clash (indicating that fromS
ia model ofScan be built).ℱ is then expanded by repeatedly applying the rules from Table 3. The notationR
*denotes either the roleRor the role returned byInv
(
R
), and the notation 〈
*
,
⋈
,
ℓ
〉 denotes any role that participates in such a triple.Table 3
Rule description.
Rule
Description
(
¬
⋈
)
If
〈
¬
C
,
⋈
,
l
〉
∈
Σ
(
x
)
and
〈
C
,
⋈
-
,
~
ℓ
〉
∉
Σ
(
x
), then
Σ
(
x
)
→
Σ
(
x
)
∪
〈
C
,
⋈
-
,
~
ℓ
〉
(
⊓
⊳
)
If
〈
C
1
⊓
C
2
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊳
,
ℓ
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
∉
Σ
(
x
), then
Σ
(
x
)
→
Σ
(
x
)
∪
{
〈
C
1
,
⊳
,
ℓ
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
(
⊔
⊲
)
If
〈
C
1
⊔
C
2
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
∉
Σ
(
x
), then
Σ
(
x
)
→
Σ
(
x
)
∪
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
(
⊔
⊳
)
If
〈
C
1
⊔
C
2
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊳
,
l
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
∩
Σ
(
x
)
=
∅, then
Σ
(
x
)
→
Σ
(
x
)
∪
{
C
} for some C
∈
{
〈
C
1
,
⊳
,
ℓ
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
(
⊓
⊲
)
If
〈
C
1
⊓
C
2
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
∩
Σ
(
x
)
=
∅, then
Σ
(
x
)
→
Σ
(
x
)
∪
{
C
} for some C
∈
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
(
∃
⊳
)
If
〈
∃
R
·
C
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked and
x has no R-neighbour y connected with a triple 〈
P
*
,
⊳
,
ℓ
〉
,
P
⊑
*
R and 〈
C
,
⊳
,
ℓ
〉
∈
Σ
(
y
)
, thencreate a new node y with Σ
(
〈
x
,
y
〉
)
=
{
〈
R
,
⊳
,
ℓ
〉
}, Σ
(
y
)
=
{
〈
C
,
⊳
,
ℓ
〉
}
(
∀
⊲
)
If
〈
∀
R
·
C
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked and
x has no R-neighbour y connected with a triple 〈
P
*
,
⊲
-
,
~
ℓ
〉
,
P
⊑
*
R and 〈
C
,
⊲
,
ℓ
〉
∈
Σ
(
y
)
, thencreate a new node y with Σ
(
〈
x
,
y
〉
)
=
{
〈
R
,
⊲
-
,
~
ℓ
〉
}, Σ
(
y
)
=
{
〈
C
,
⊲
,
ℓ
〉
}
(
∀
⊳
)
If
〈
∀
R
·
C
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked, and
x has an R-neighbour y with 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊳
-
,
~
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
C
,
⊳
,
ℓ
〉
(
∃
⊲
)
If
〈
∃
R
·
C
,
⊲
,
l
〉
∈
Σ
(
x
),  x is not indirectly blocked and
x has an R-neighbour y with 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊲
,
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
C
,
⊲
,
ℓ
〉
(
∀
+
)
If
〈
∀
R
·
C
,
→
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked, x has a P-neighbour y with, 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
), andthere is some P, with T
rans(P), and P
⊑
*
R, 〈
∀
P
·
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊳
-
,
~
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
∀
P
·
C
,
⊳
,
l
〉
(
∃
+
)
If
〈
∃
R
·
C
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked, x has a P-neighbour y with, 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
), andthere is some P, with Trans(P), and P
⊑
*
R, 〈
∃
P
·
C
,
⊲
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊲
,
~
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
∃
P
·
C
,
⊲
,
ℓ
〉
(
≥
⊳
)
If
〈
≥
p
·
R
,
⊳
,
l
〉
∈
Σ
(
x
),  x is not blocked, andthere are no p  R-neighbours y
1
,
…
,
ℓ
p, connected to x with a triple 〈
∃
P
*
,
⊳
,
l
〉
∉
Σ
(
y
), P
⊑
*
R, and
y
i
≠
y
j for 1
≤
i
≤
j
≤
p, thencreate p new nodes y
1
,
…
,
ℓ
p, with Σ
(
〈
x
,
y
i
〉
)
=
{
〈
R
,
⊳
,
ℓ
〉
} and y
i
≠
y
j for 1
≤
i
≤
j
≤
p
(
≤
⊲
)
If
〈
≤
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked, thenapply (
∃
+
) rule for the triple 〈
≥
(
p
+
1
)
R
,
⊲
-
,
~
ℓ
〉
(
≤
⊲
)
If
〈
≤
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked, thenapply (
∃
+
) rule for the triple 〈
≥
(
p
+
1
)
R
,
⊲
-
,
~
ℓ
〉
(
≤
⊳
)
If
〈
≤
p
·
R
,
⊳
,
l
〉
∈
Σ
(
x
),  x is not indirectly blocked, andthere are p
+
1  R-neighbours y
1
,
…
,
y
p
+
1 connected to x with a triple 〈
P
*
,
⊳
′
,
~
ℓ
i
〉, P
⊑
*
R, andwhich is conjugated with 〈
P
*
,
⊳
-
,
~
ℓ
〉, and there are two of them y, z, with no y
≠
z, and
y is neither a root node nor an ancestor of z, then
Σ
(
z
)
→
Σ
(
z
)
∪
Σ
(
y
), andif  z is an ancestor of x, then Σ
(
〈
z
,
x
〉
)
→
Σ
(
〈
z
,
x
〉
)
∪
I
n
v
(
Σ
(
〈
x
,
y
〉
)
) else Σ
(
〈
x
,
z
〉
)
→
Σ
(
〈
x
,
z
〉
)
∪
Σ
(
〈
x
,
y
〉
), and
Σ
(
〈
x
,
y
〉
)
→
∅, andSet u
≠
z for ∀
u with u
≠
y
(
≥
⊲
)
If
〈
≥
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
)
,
x is not indirectly blocked, thenapply (
≤
⊳
) rule for the triple 〈
≤
(
p
-
1
)
R
,
⊲
-
,
~
ℓ
〉
(
≤
r
⊳
)
If
〈
≤
p
·
R
,
⊳
,
ℓ
〉
∈
Σ
(
x
), andthere are p
+
1  R-neighbours y
1
,
…
,
y
p
+
1 connected to x with a triple 〈
P
*
,
⊳
′
,
~
ℓ
i
〉, P
⊑
*
R, andconjugated with 〈
P
*
,
⊳
-
,
~
ℓ
〉, and there are two of them y, z, both root nodes, with no y
≠
z, then
Σ
(
z
)
→
Σ
(
z
)
∪
Σ
(
y
), andfor all edges 〈
y
,
w
〉: (1) if  the edge 〈
z
,
w
〉 does not exist, create it with Σ
(
〈
z
,
w
〉
)
→
∅; (2) Σ
(
〈
z
,
w
〉
)
→
Σ
(
〈
z
,
w
〉
)
∪
Σ
(
〈
y
,
w
〉
), andfor all edges 〈
w
,
y
〉: (1) if  the edge 〈
w
,
z
〉 does not exist, create it with Σ
(
〈
w
,
z
〉
)
→
∅; (2) Σ
(
〈
w
,
z
〉
)
→
Σ
(
〈
w
,
z
〉
)
∪
Σ
(
〈
w
,
y
〉
)
andSet Σ
(
y
)
=
∅,   and remove all edges to/from y, andset u
≠
z for ∀
u with u
≠
y and set y
=
z
(
≥
r
⊲
)
〈
≥
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
), thenapply (
≤
r
⊳
) rule for the triple 〈
≤
(
p
-
1
)
R
,
⊲
-
,
~
ℓ
〉The completion forest is complete when for some nodex
:
Σ
(
x
) contains a clash, or none of the completion rules in Table 3 are applicable. The algorithm is correct in the sense that it produces a clash if and only if Σ is inconsistent. The expansion rules are based on the properties of the semantics presented in Definition 6.


### 3.3. Soundness and Completeness of theL-𝒮
ℋ
ℐ
𝒩 Tableaux Algorithm

Lemma 9 (termination, soundness, completeness).
For a given KBΣ: (i)
the tableau algorithm terminates;
(ii)
if the expansion rules can be applied toΣsuch that they yield a complete completion-forest ℱ such thatC
ℱhas a solution, thenΣhas a model;
(iii)
ifΣhas a model, then the expansion rules can be applied in such a way that the tableaux algorithm yields a complete completion forest forΣsuch thatC
ℱhas a solution.


### 3.4.  Computational Complexity of the Tableau Algorithm forL-𝒮
ℋ
ℐ
𝒩

We have described a tableau procedure for reasoning inL-𝒮
ℋ
ℐ
𝒩. Due to the tableau rules are nondeterministic, every application of expansion rules to a termination after at most exponentially many rule applications. So according to the theorem in [5] that the tableaux algorithm is NExpTime complete, we get the following proposition deciding the computational complexity of the tableau algorithm forL-𝒮
ℋ
ℐ
𝒩.Proposition 10.
The concept satisfiability checking problem inL-𝒮
ℋ
ℐ
𝒩 with respect to witnessed models can be decided in NExpTime.Proof (sketch).
It is assumed thatL-𝒮
ℋ
ℐ
𝒩 has then-witnessed model property for somen
≥
1, the completion forest has to generatendifferent successors for every existential(
∃
) and universal (
∀
) restriction to ensure that the degrees guessed for these complex concepts are indeed witnessed by the model. As stated by Table 1, we have to introduce n individuals {
y
1
,
…
,
y
n
} and 2
n values {
ℓ
1
1
,
…
,
ℓ
1
n
}
∈
L, {
ℓ
2
1
…
,
ℓ
2
n
}
∈
L, which satisfies ⋁
i
=
1
n
ℓ
1
i
⊗
ℓ
2
i
=
ℓ or ⋀
i
=
1
n
ℓ
1
i
⇒
ℓ
2
i
=
ℓ, respectively. In the following we let n
max
⁡ be the number that occurs in a number restriction, and let h be the number of different lattices appearing in 𝒜.Following [14] we set n
=
|
|
A
|
+
|
R
|
|
=
𝒪
(
|
A
|
+
|
R
|
)
=
𝒪
(
2
n
); in the meantime, we letm
=
|
sub
(
D
)
|
=
𝒪
(
2
|
A
|
|
R
|
)
=
𝒪
(
n
2
),k
=
|
R
A
|
=
𝒪
(
|
A
|
+
|
R
|
)
=
𝒪
(
2
n
),n
max
⁡
=
𝒪
(
2
|
A
|
)
=
𝒪
(
2
n
),h
=
𝒪
(
|
A
|
)
=
𝒪
(
n
), andq
=
max
⁡
{
D
ℒ
(
s
)
∣
∀
s
∈
𝒯
}. Then due to the proof of Lemma  6.9 in [11] and by the addition of the number of different lattices appearing in 𝒜-q: a completion forest for 𝒜 becomes no longer than2
8
·
m
·
h
·
k
·
qand that the outdegree is bounded by2
·
h
·
m
·
n
max
⁡. Consequently, theL-𝒮
ℋ
ℐ
𝒩 algorithm will construct a completion forest with no more than (
2
·
h
·
m
·
n
max
⁡
)
2
8
·
m
·
h
·
k
·
q
=
𝒪
(
(
2
·
n
·
n
2
·
2
n
)
2
8
·
n
2
·
n
·
n
·
q
)
=
𝒪
(
2
n
·
2
8
·
n
4
·
q
)
=
𝒪
(
2
2
q
·
n
4
) nodes.For fuzzy description logics with semantics based on complete residuated De Morgan lattices (e.g.,L-𝒜
ℒ
𝒞
ℐ), strong satisfiability with respect to general TBoxes is undecidable for some infinite lattices while, for finite lattices, decidability is regained [5]. If one considers the 𝒜
ℒ
𝒞 without terminological axioms, concept satisfiability is ExpTime complete as in the crisp case [15]. The problem with respect to general TBoxes becomes ExpTime complete matching the complexity of the crisp case, though arbitrary (finite) lattices and t-norms are allowed [4]. Besides, strong concept satisfiability is in NExpTime L-𝒮
ℋ
ℐ.When we consider finite De Morgan latticesL, then satisfiability problem can be effectively decided. We guess that the computational complexity of it can be improved to ExpTime either by an ABox partitioning [16] or with the help of global caching and other techniques [17].


## 3.1.L
-
𝒮
ℋ
ℐ
𝒩 Tableau

Since most of the inference services of fuzzy DLs can be reduced to the problem of consistency checking for ABoxes [9], here we discuss the approaches to deciding consistency of fuzzy DLs over finite residuated De Morgan lattices in the presence of GCIs. The algorithm we present can be seen as an extension of the tableau presented in [5] and is inspired by the well-known tableau algorithm forf-𝒮
ℋ
ℐ
𝒩 [10], which is the basis for several highly successful implementations.It is assumed thatLis finite, and we can accordingly restrict reasoning ton-witnessed models. In the lattice L
=
〈
ζ
,
⊲
,
⊳
〉,we employ the symbols⊲and⊳as a placeholder for the inequalities≺
,
⪯and≻
,
⪰ and the symbol ⋈ as a placeholder for all types of inequations. Furthermore we employ the symbols⊲
-
,
⊳
-and ⋈
-to denote their reflections.Definition 6.
For a fuzzy conceptC, we will denote bysub
(
C
)the set that containsCand it is closed under subconcepts ofC. The set of all subconcepts of concepts that appear within an ABox is denoted by sub(C). LetR
Abe the set of roles occurring in 𝒜 and ℛ together with their inverses, andI
𝒜is the set of individuals in 𝒜. A fuzzy tableauTforΣis a quadruple in(
S
,
𝒢
,
Υ
,
𝒱
), such that (i)
S is a nonempty set of individuals (nodes),
(ii)
𝒢:S
×
sub
(
A
)
→
ζmaps each element and concept, that is, a member ofsub
(
A
), to the degree of certainty of that element to the concept,
(iii)
Υ:R
Σ
×
S
×
S
→
ζmaps each role ofR
Aand pair of elements to the degree of certainty of the pair to the role,
(iv)
𝒱: maps individuals occurring inAto elements inS.
For alls
,
t
∈
S,C
,
D
∈
sub
(
A
), ℓ
∈
ζ, andR
∈
R
A,Tsatisfies the following. (1)
Σ
(
s
,
⊥
)
=
0,Σ
(
s
,
⊤
)
=
1for∀
s
∈
S.
(2)
If〈
¬
C
,
⋈
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⋈
-
,
~
ℓ
〉
∈
𝒢
(
s
).
(3)
If〈
C
⊓
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
).
(4)
If〈
C
⊔
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
).
(5)
If〈
C
⊔
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊳
,
ℓ
〉
∈
𝒢
(
s
).
(6)
If〈
C
⊓
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), then〈
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
)and〈
D
,
⊲
,
ℓ
〉
∈
𝒢
(
s
).
(7)
If〈
∀
R
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
)and〈
〈
s
,
t
〉
,
⊳
′
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
〈
s
,
t
〉
,
⊳
-
,
~
ℓ
〉, then〈
∀
C
,
⊳
,
ℓ
〉
∈
𝒢
(
t
).
(8)
If〈
∀
R
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
)and〈
〈
s
,
t
〉
,
⊳
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
〈
s
,
t
〉
,
⊲
,
~
ℓ
〉, then〈
∀
C
,
⊲
,
ℓ
〉
∈
𝒢
(
t
).
(9)
If〈
∃
R
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), then there existst
∈
Ssuch that〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
R
)and〈
〈
s
,
t
〉
,
⊳
,
~
ℓ
〉, then〈
∀
C
,
⊳
,
ℓ
〉
∈
𝒢
(
t
).
(10)
If〈
∀
R
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), then there existst
∈
Ssuch that〈
〈
s
,
t
〉
,
⊲
-
,
~
ℓ
〉
∈
Υ
(
R
)and〈
〈
s
,
t
〉
,
⊲
,
~
ℓ
〉, then〈
∀
C
,
⊳
,
ℓ
〉
∈
𝒢
(
t
).
(11)
If〈
∃
s
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
), and〈
〈
s
,
t
〉
,
⊳
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
s
·
C
,
⊲
,
ℓ
〉, for someR
⊑
*with  Trans(R), then〈
∃
s
·
C
,
⊲
,
ℓ
〉
∈
𝒢
(
s
).
(12)
If〈
∀
s
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
), and〈
〈
s
,
t
〉
,
⊳
′
,
ℓ
1
〉
∈
Υ
(
R
)is conjugated with〈
s
·
C
,
⊳
-
,
~
ℓ
〉, for someR
⊑
*with  Trans(R), then〈
∀
s
·
C
,
⊳
,
ℓ
〉
∈
𝒢
(
s
).
(13)
〈
〈
s
,
t
〉
,
⋈
,
ℓ
〉
∈
Υ
(
R
)if〈
〈
t
,
s
〉
,
⋈
,
ℓ
〉
∈
Υ
(
R
)
(
Inv
(
R
)
).
(14)
If〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
R
)andR
⊑
*
Sthen,〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
S
).
(15)
〈
≥
p
R
,
⊳
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊳
,
ℓ
〉
∈
Υ
(
R
)
}
≥
p.
(16)
〈
≤
p
R
,
⊲
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊲
-
,
~
ℓ
〉
∈
Υ
(
R
)
}
≥
p
+
1.
(17)
〈
≥
p
R
,
⊲
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊳
,
ℓ
i
〉
∈
Υ
(
R
)
}
≤
p
-
1, conjugated with〈
〈
s
,
t
〉, ⊲
,
ℓ
〉.
(18)
〈
≤
p
R
,
⊳
,
ℓ
〉
∈
Υ
(
R
), then{
t
∈
S
∣
〈
〈
s
,
t
〉
,
⊳
′
,
ℓ
i
〉
∈
Υ
(
R
)
}
≤
p, conjugated with〈
〈
s
,
t
〉
,
⊳
-,~
ℓ
〉.
(19)
There do not exist two conjugated triples in any label of any individualx
∈
S.
(20)
If〈
a
:
C
⋈
ℓ
〉
∈
A, then〈
C
⋈
ℓ
〉
∈
𝒢
(
𝒱
(
a
)
).
(21)
If〈
(
a
,
b
)
:
R
⋈
ℓ
〉
∈
A, then〈
(
𝒱
(
a
)
,
(
𝒱
(
b
)
)
⋈
ℓ
〉
∈
Υ
(
R
).
(22)
Ifa
≠
b
∈
𝒜, then 𝒱
(
a
)
≠
𝒱
(
b
).Lemma 7.
AnL-𝒮
ℋ
ℐ
𝒩ABox 𝒜 is consistent with respect to ℛ if and only if there exists a fuzzy tableau for 𝒜 with respect to ℛ.Proof.
Similar to that of Lemma 6.5 of [11], here gives the proof of the Lemma 7. For the direction if T = (
S
,
𝒢
,
Υ
,
𝒱
) is a fuzzy tableau for an ABox 𝒜 with respect to ℛ, we can construct a fuzzy interpretation ℐ = (
Δ
ℐ
,
·
ℐ
)that is a model of 𝒜. Consider the following:
(3)
Δ
ℐ
=
S
,
a
ℐ
=
V
(
a
)
,
a
∈
ℐ
A
,
⊺
ℐ
=
𝒢
(
s
,
⊤
)
,
∀
s
∈
S
,
⊥
ℐ
=
𝒢
(
s
,
⊥
)
,
∀
s
∈
S
,
A
ℐ
=
𝒢
(
s
,
A
)
,
∀
s
∈
S
and
concept
names
A
.
For all roleR
∈
R
A,
(4)
R
ℐ
(
s
,
t
)
=
{
R
Υ
+
(
s
,
t
)
,
∀
〈
s
,
t
〉
∈
S
×
S
if
T
r
a
n
s
(
R
)
R
Υ
(
s
,
t
)
,
∀
〈
s
,
t
〉
∈
S
×
S
otherwise
,
whereR
Υ
(
s
,
t
)is a binary fuzzy relation defined asR
Υ
(
s
,
t
)
=
Υ
(
R
,
〈
s
,
t
〉
)for all∀
〈
s
,
t
〉
∈
S
×
S, andR
Υ
+
(
s
,
t
)represents its sup-min transitive closure [12]. The proof of this property is quite technical and omitted here. From all above properties, the interpretation of individuals and roles implies that ℐ satisfies each assertion in 𝒜 inductively.


## 3.2.  Constructing aL-𝒮
ℋ
ℐ
𝒩 Tableau

Like most of the tableaux algorithms, our algorithm works oncompletion forests rather than on completion trees which is applied in work [5]. As pointed out in [13], that is because an ABox might contain several individuals with arbitrary roles connecting them.Definition 8 (completion forest).
A completion forestℱ forΣis a collection of trees whose distinguished roots are arbitrarily connected by edges. Each nodexis labelled with a setΣ
(
x
)
=
{
〈
C
,
⋈
,
l
〉
}. Each edge〈
x
,
y
〉is labelled with a setΣ
(
〈
x
,
y
〉
)
=
{
〈
R
,
⋈
,
l
〉
}, whereR
∈
R
Aare roles and its inverse occurring in 𝒜. A completion forest comes with an explicit inequality relation≠on nodes and an explicit equality relation≐which are implicitly assumed to be symmetric. Given a completion forest, If nodesxandyare connected by an edge〈
v
,
w
〉with〈
R
,
l
〉occurring inΣ
(
〈
x
,
y
〉
), thenyis called anR-successorofxandxis called anR-predecessorofy. A nodexis a positive (resp., negative) successor (resp., predecessor or neighbour) ofy.A node is blocked if it is either directly or indirectly blocked. It is indirectly blocked if itsR-predecessor is either directly or indirectly blocked. A nodexis directly blocked if and only if none of its ancestors are blocked, and it has an ancestorysuch thatΣ
(
x
)
=
Σ
(
y
).A nodex is said to contain a clash satisfying one of the conditions such that if and only if there exist two conjugated triples inΣ
(
〈
x
,
y
〉
), or ifΣ
(
〈
x
,
y
〉
)
∪
{
〈
Inv
(
R
)
,
⋈
,
ℓ
〉
∣
〈
R
,
⋈
,
ℓ
〉
∈
Σ
(
〈
y
,
x
〉
)
} andx,y are root nodes, contains two conjugated triples. Table 2 shows all the entries under which condition the row column pair ofL-constraints is a
conjugated pair
(e.g.,
a
:
A
≻
uanda
:
A
⋡
vis a conjugated pair as¬
(
∃
v
·
v
≻
u
∧
v
⋡
v
)).Table 2
Conjugated pairs.
〈
α
⋡
l
′
〉
〈
α
≺
l
′
〉
〈
α
≻
l
〉
¬
(
∃
l
′
′
·
l
′
′
≻
l
∧
l
′
′
⋡
l
′
)
l
⊀
l
′
〈
α
⋠
l
〉
¬
(
∃
l
′
′
·
l
′
′
⋠
l
∧
l
′
′
⋡
l
′
)
¬
(
∃
l
′
′
·
l
′
′
⋠
l
∧
l
′
′
≺
l
′
)The calculus is based on a set of constraint propagation rules transforming a setSinto satisfiability preserving setsS
iuntil either one ofS
icontains an inconsistency (clash), or someS
iis completed and clash-free; that is, no rule can further be applied toS
iandS
icontains no clash (indicating that fromS
ia model ofScan be built).ℱ is then expanded by repeatedly applying the rules from Table 3. The notationR
*denotes either the roleRor the role returned byInv
(
R
), and the notation 〈
*
,
⋈
,
ℓ
〉 denotes any role that participates in such a triple.Table 3
Rule description.
Rule
Description
(
¬
⋈
)
If
〈
¬
C
,
⋈
,
l
〉
∈
Σ
(
x
)
and
〈
C
,
⋈
-
,
~
ℓ
〉
∉
Σ
(
x
), then
Σ
(
x
)
→
Σ
(
x
)
∪
〈
C
,
⋈
-
,
~
ℓ
〉
(
⊓
⊳
)
If
〈
C
1
⊓
C
2
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊳
,
ℓ
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
∉
Σ
(
x
), then
Σ
(
x
)
→
Σ
(
x
)
∪
{
〈
C
1
,
⊳
,
ℓ
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
(
⊔
⊲
)
If
〈
C
1
⊔
C
2
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
∉
Σ
(
x
), then
Σ
(
x
)
→
Σ
(
x
)
∪
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
(
⊔
⊳
)
If
〈
C
1
⊔
C
2
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊳
,
l
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
∩
Σ
(
x
)
=
∅, then
Σ
(
x
)
→
Σ
(
x
)
∪
{
C
} for some C
∈
{
〈
C
1
,
⊳
,
ℓ
〉
,
〈
C
2
,
⊳
,
ℓ
〉
}
(
⊓
⊲
)
If
〈
C
1
⊓
C
2
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked and
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
∩
Σ
(
x
)
=
∅, then
Σ
(
x
)
→
Σ
(
x
)
∪
{
C
} for some C
∈
{
〈
C
1
,
⊲
,
ℓ
〉
,
〈
C
2
,
⊲
,
ℓ
〉
}
(
∃
⊳
)
If
〈
∃
R
·
C
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked and
x has no R-neighbour y connected with a triple 〈
P
*
,
⊳
,
ℓ
〉
,
P
⊑
*
R and 〈
C
,
⊳
,
ℓ
〉
∈
Σ
(
y
)
, thencreate a new node y with Σ
(
〈
x
,
y
〉
)
=
{
〈
R
,
⊳
,
ℓ
〉
}, Σ
(
y
)
=
{
〈
C
,
⊳
,
ℓ
〉
}
(
∀
⊲
)
If
〈
∀
R
·
C
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked and
x has no R-neighbour y connected with a triple 〈
P
*
,
⊲
-
,
~
ℓ
〉
,
P
⊑
*
R and 〈
C
,
⊲
,
ℓ
〉
∈
Σ
(
y
)
, thencreate a new node y with Σ
(
〈
x
,
y
〉
)
=
{
〈
R
,
⊲
-
,
~
ℓ
〉
}, Σ
(
y
)
=
{
〈
C
,
⊲
,
ℓ
〉
}
(
∀
⊳
)
If
〈
∀
R
·
C
,
⊳
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked, and
x has an R-neighbour y with 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊳
-
,
~
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
C
,
⊳
,
ℓ
〉
(
∃
⊲
)
If
〈
∃
R
·
C
,
⊲
,
l
〉
∈
Σ
(
x
),  x is not indirectly blocked and
x has an R-neighbour y with 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊲
,
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
C
,
⊲
,
ℓ
〉
(
∀
+
)
If
〈
∀
R
·
C
,
→
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked, x has a P-neighbour y with, 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
), andthere is some P, with T
rans(P), and P
⊑
*
R, 〈
∀
P
·
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊳
-
,
~
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
∀
P
·
C
,
⊳
,
l
〉
(
∃
+
)
If
〈
∃
R
·
C
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not indirectly blocked, x has a P-neighbour y with, 〈
C
,
⊳
,
ℓ
〉
∉
Σ
(
y
), andthere is some P, with Trans(P), and P
⊑
*
R, 〈
∃
P
·
C
,
⊲
,
ℓ
〉
∉
Σ
(
y
)
and
〈
*
,
⊲
,
~
ℓ
〉 is conjugated with the positive triple that connects x and y, then
Σ
(
y
)
→
Σ
(
y
)
∪
〈
∃
P
·
C
,
⊲
,
ℓ
〉
(
≥
⊳
)
If
〈
≥
p
·
R
,
⊳
,
l
〉
∈
Σ
(
x
),  x is not blocked, andthere are no p  R-neighbours y
1
,
…
,
ℓ
p, connected to x with a triple 〈
∃
P
*
,
⊳
,
l
〉
∉
Σ
(
y
), P
⊑
*
R, and
y
i
≠
y
j for 1
≤
i
≤
j
≤
p, thencreate p new nodes y
1
,
…
,
ℓ
p, with Σ
(
〈
x
,
y
i
〉
)
=
{
〈
R
,
⊳
,
ℓ
〉
} and y
i
≠
y
j for 1
≤
i
≤
j
≤
p
(
≤
⊲
)
If
〈
≤
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked, thenapply (
∃
+
) rule for the triple 〈
≥
(
p
+
1
)
R
,
⊲
-
,
~
ℓ
〉
(
≤
⊲
)
If
〈
≤
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
),  x is not blocked, thenapply (
∃
+
) rule for the triple 〈
≥
(
p
+
1
)
R
,
⊲
-
,
~
ℓ
〉
(
≤
⊳
)
If
〈
≤
p
·
R
,
⊳
,
l
〉
∈
Σ
(
x
),  x is not indirectly blocked, andthere are p
+
1  R-neighbours y
1
,
…
,
y
p
+
1 connected to x with a triple 〈
P
*
,
⊳
′
,
~
ℓ
i
〉, P
⊑
*
R, andwhich is conjugated with 〈
P
*
,
⊳
-
,
~
ℓ
〉, and there are two of them y, z, with no y
≠
z, and
y is neither a root node nor an ancestor of z, then
Σ
(
z
)
→
Σ
(
z
)
∪
Σ
(
y
), andif  z is an ancestor of x, then Σ
(
〈
z
,
x
〉
)
→
Σ
(
〈
z
,
x
〉
)
∪
I
n
v
(
Σ
(
〈
x
,
y
〉
)
) else Σ
(
〈
x
,
z
〉
)
→
Σ
(
〈
x
,
z
〉
)
∪
Σ
(
〈
x
,
y
〉
), and
Σ
(
〈
x
,
y
〉
)
→
∅, andSet u
≠
z for ∀
u with u
≠
y
(
≥
⊲
)
If
〈
≥
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
)
,
x is not indirectly blocked, thenapply (
≤
⊳
) rule for the triple 〈
≤
(
p
-
1
)
R
,
⊲
-
,
~
ℓ
〉
(
≤
r
⊳
)
If
〈
≤
p
·
R
,
⊳
,
ℓ
〉
∈
Σ
(
x
), andthere are p
+
1  R-neighbours y
1
,
…
,
y
p
+
1 connected to x with a triple 〈
P
*
,
⊳
′
,
~
ℓ
i
〉, P
⊑
*
R, andconjugated with 〈
P
*
,
⊳
-
,
~
ℓ
〉, and there are two of them y, z, both root nodes, with no y
≠
z, then
Σ
(
z
)
→
Σ
(
z
)
∪
Σ
(
y
), andfor all edges 〈
y
,
w
〉: (1) if  the edge 〈
z
,
w
〉 does not exist, create it with Σ
(
〈
z
,
w
〉
)
→
∅; (2) Σ
(
〈
z
,
w
〉
)
→
Σ
(
〈
z
,
w
〉
)
∪
Σ
(
〈
y
,
w
〉
), andfor all edges 〈
w
,
y
〉: (1) if  the edge 〈
w
,
z
〉 does not exist, create it with Σ
(
〈
w
,
z
〉
)
→
∅; (2) Σ
(
〈
w
,
z
〉
)
→
Σ
(
〈
w
,
z
〉
)
∪
Σ
(
〈
w
,
y
〉
)
andSet Σ
(
y
)
=
∅,   and remove all edges to/from y, andset u
≠
z for ∀
u with u
≠
y and set y
=
z
(
≥
r
⊲
)
〈
≥
p
·
R
,
⊲
,
ℓ
〉
∈
Σ
(
x
), thenapply (
≤
r
⊳
) rule for the triple 〈
≤
(
p
-
1
)
R
,
⊲
-
,
~
ℓ
〉The completion forest is complete when for some nodex
:
Σ
(
x
) contains a clash, or none of the completion rules in Table 3 are applicable. The algorithm is correct in the sense that it produces a clash if and only if Σ is inconsistent. The expansion rules are based on the properties of the semantics presented in Definition 6.


## 3.3. Soundness and Completeness of theL-𝒮
ℋ
ℐ
𝒩 Tableaux Algorithm

Lemma 9 (termination, soundness, completeness).
For a given KBΣ: (i)
the tableau algorithm terminates;
(ii)
if the expansion rules can be applied toΣsuch that they yield a complete completion-forest ℱ such thatC
ℱhas a solution, thenΣhas a model;
(iii)
ifΣhas a model, then the expansion rules can be applied in such a way that the tableaux algorithm yields a complete completion forest forΣsuch thatC
ℱhas a solution.


## 3.4.  Computational Complexity of the Tableau Algorithm forL-𝒮
ℋ
ℐ
𝒩

We have described a tableau procedure for reasoning inL-𝒮
ℋ
ℐ
𝒩. Due to the tableau rules are nondeterministic, every application of expansion rules to a termination after at most exponentially many rule applications. So according to the theorem in [5] that the tableaux algorithm is NExpTime complete, we get the following proposition deciding the computational complexity of the tableau algorithm forL-𝒮
ℋ
ℐ
𝒩.Proposition 10.
The concept satisfiability checking problem inL-𝒮
ℋ
ℐ
𝒩 with respect to witnessed models can be decided in NExpTime.Proof (sketch).
It is assumed thatL-𝒮
ℋ
ℐ
𝒩 has then-witnessed model property for somen
≥
1, the completion forest has to generatendifferent successors for every existential(
∃
) and universal (
∀
) restriction to ensure that the degrees guessed for these complex concepts are indeed witnessed by the model. As stated by Table 1, we have to introduce n individuals {
y
1
,
…
,
y
n
} and 2
n values {
ℓ
1
1
,
…
,
ℓ
1
n
}
∈
L, {
ℓ
2
1
…
,
ℓ
2
n
}
∈
L, which satisfies ⋁
i
=
1
n
ℓ
1
i
⊗
ℓ
2
i
=
ℓ or ⋀
i
=
1
n
ℓ
1
i
⇒
ℓ
2
i
=
ℓ, respectively. In the following we let n
max
⁡ be the number that occurs in a number restriction, and let h be the number of different lattices appearing in 𝒜.Following [14] we set n
=
|
|
A
|
+
|
R
|
|
=
𝒪
(
|
A
|
+
|
R
|
)
=
𝒪
(
2
n
); in the meantime, we letm
=
|
sub
(
D
)
|
=
𝒪
(
2
|
A
|
|
R
|
)
=
𝒪
(
n
2
),k
=
|
R
A
|
=
𝒪
(
|
A
|
+
|
R
|
)
=
𝒪
(
2
n
),n
max
⁡
=
𝒪
(
2
|
A
|
)
=
𝒪
(
2
n
),h
=
𝒪
(
|
A
|
)
=
𝒪
(
n
), andq
=
max
⁡
{
D
ℒ
(
s
)
∣
∀
s
∈
𝒯
}. Then due to the proof of Lemma  6.9 in [11] and by the addition of the number of different lattices appearing in 𝒜-q: a completion forest for 𝒜 becomes no longer than2
8
·
m
·
h
·
k
·
qand that the outdegree is bounded by2
·
h
·
m
·
n
max
⁡. Consequently, theL-𝒮
ℋ
ℐ
𝒩 algorithm will construct a completion forest with no more than (
2
·
h
·
m
·
n
max
⁡
)
2
8
·
m
·
h
·
k
·
q
=
𝒪
(
(
2
·
n
·
n
2
·
2
n
)
2
8
·
n
2
·
n
·
n
·
q
)
=
𝒪
(
2
n
·
2
8
·
n
4
·
q
)
=
𝒪
(
2
2
q
·
n
4
) nodes.For fuzzy description logics with semantics based on complete residuated De Morgan lattices (e.g.,L-𝒜
ℒ
𝒞
ℐ), strong satisfiability with respect to general TBoxes is undecidable for some infinite lattices while, for finite lattices, decidability is regained [5]. If one considers the 𝒜
ℒ
𝒞 without terminological axioms, concept satisfiability is ExpTime complete as in the crisp case [15]. The problem with respect to general TBoxes becomes ExpTime complete matching the complexity of the crisp case, though arbitrary (finite) lattices and t-norms are allowed [4]. Besides, strong concept satisfiability is in NExpTime L-𝒮
ℋ
ℐ.When we consider finite De Morgan latticesL, then satisfiability problem can be effectively decided. We guess that the computational complexity of it can be improved to ExpTime either by an ABox partitioning [16] or with the help of global caching and other techniques [17].


## 4. Optimization Techniques Employed in Tableau Algorithm forL-𝒮
ℋ
ℐ
𝒩

From Proposition10, it is obvious that the theoretical complexity of the tableau reasoning algorithm forL-𝒮
ℋ
ℐ
𝒩 is 2-NExptime, which is too expensive for a reasoner to deal with. So we plan to investigate some optimizations [18] developed for tableaux algorithms for crisp DLs, which can be transferred to our setting to reduce the search space created by the choice of lattice values. By using these techniques, a theoretically expensive computation could be converted to an equivalent of practically lower complexity.In this section we describe in detail the optimisation techniques employed in tableau algorithm forL-𝒮
ℋ
ℐ
𝒩. Not only focusing mainly on novel techniques and significant refinements and extensions of previously known techniques such as global caching, we also apply some simple but often very effective optimisations to our implement. First of all, we perform some preprocessing optimisations directly on the syntax of the input. Then in virtue of the ideas of both backjumping and global caching, we investigate an optimized tableau-based reasoning algorithm and prove its ExpTime complete.


### 4.1. Preprocessing Optimisations

In case of obvious clash detection or cycle via concept names, preprocessing optimisations (e.g.,absorption ortold cycle elimination) can lead to important speedup of the subsequent reasoning process. These optimisations serve to preprocess and simplify the input into a form more amenable to later processing [18]. Furthermore, these optimisations are not specific to tableau-based fuzzy reasoners and may also be useful with other kinds of fuzzy DL reasoners. Herein on the basis ofL-𝒮
ℋ
ℐ
𝒩, we apply two striking optimizations techniques to our design and implement.


#### 4.1.1. Partition Based on Connectivity

Partition based on connectivity is a quite effective optimization technique to boost up the performance of reasoning, which can be applied to any fuzzy DL without nominals independently of the fuzzy operators used to provide the interpretations [17]. Termination of the expansion of the completion forest is a result of the properties of the expansion rules in Table 3, and a tableau expansion rule can either add (i) a new neighbour node to the node of examination, (ii) new membership triples in this node, or (iii) new membership triples to neighbouring nodes. The expansion rule will examine the different ways that the tableau expansion rules affect this completion forest, with the respect of different connectivity circumstances. Inspired by the work in [17], we have the following definitions.Definition 11.
Leta, b, c
∈
I, ℓ
∈
L. The connection relation between two individualsa, bin an ABox 𝒜 is inductively defined through role R
A:
(5)
a
↭
𝒜
b
⟺
{
R
A
(
a
,
b
)
⋈
l
∈
𝒜
derectly
connected
(
a
↭
𝒜
c
)
∪
(
b
↭
𝒜
c
)
inderectly
connected
.Note thatcmay be run into an iterative process for connecting indirectly. The individuals in the ABox 𝒜 may be divided into one or more individual groups. Then individual group is partitioned into one or more independent subsets calledAssertion Groups (
A
G
) [16]. For instance, two assertionsA
1andA
2are in the same A
G ifA
1is directly or indirectly inferred fromA
2(through the application of completion rules), orA
1andA
2differ only in terms of their certainty values and/or conjunction and disjunction functions. Each group is composed of individuals that are connected to each other through role assertionsR
A.Definition 12.
We denoteA
G
[
a
]with the partition of the ABox 𝒜 that contains only connected individuals in 𝒜
(6)
A
G
[
a
]
=
{
a
}
∪
{
x
∣
∀
x
∈
I
,
a
↭
𝒜
x
}
.Proposition 13.
It holds that
(1)
∪
A
G
i
=
𝒜,
(2)
A
G
i
∩
A
G
j
=
∅,for each pair
A
G
i
,
A
G
j
∈
A
such that
A
G
i
=
A
G
j,
(3)
𝒜
is consistent with respect to a TBox
𝒯
if and only if each
A
G
i
is consistent with respect to a TBox
𝒯.Partition based on connectivity optimization technique has several advantages. First, it is of polynomial complexity and it can be applied to any fuzzy DL. In addition, If anyA
G is found to be inconsistent, this implies that the whole 𝒜 is inconsistent. A related benefit is to more precisely identify the assertions that cause the inconsistency. Finally, the speed of solving a few small constraint sets would be faster than solving one large constraint set.


#### 4.1.2. Dealt with TBox Axioms

If dealt with axioms of TBox𝒯 naively, which maybe lead to a serious degradation in reasoning performance, as each such axiom would cause a disjunction to be added to every node of the completion forest, leading to potentially enormous amounts on nondeterministic expansion [18].Givenς
∈
𝒯, withς
=
(
(
C
1
∨
D
1
)
∧
⋯
∧
(
C
n
∨
D
n
)
), testing the satisfiability ofςleads to the construction of a completion forest containingknodes, then there are2
k
ndifferent ways to apply the ⊓- and ⊔-rules to the resultingkcopies ofA, which leads to the explosion in the size of the search space. Fortunately, some notable works of optimisations known aslazy unfolding andabsorption had been used to identifying these problems [19]. Herein we chooselazy unfolding optimisation to address this issue. Due to the limitation of the paper, detailed definition oflazy unfolding is omitted here, and we refer the reader to the above literatures.


### 4.2.  Core Satisfiability Optimisations

In the following, we present core reasoning ofL-𝒮
ℋ
ℐ
𝒩, a satisfiability checking algorithm, which implements a highly optimised version on the basis of the tableau algorithm described in Section 3. Before introducing the optimisations extended to the naive tableau algorithm, we present a brief introduction tobackjumpingandglobal cachingand show how such algorithms are implemented in practice.


#### 4.2.1. Dependency Directed Backtracking (Backjumping)

Backjumping is an optimisation that is crucial for effective tableau based reasoning. Inherent unsatisfiability concealed in subformulae can lead to large amounts of unproductive backtracking search known as thrashing, especially if the unsatisfiability caused by the modal subformulae had been slightly less trivial [20]. Consider the following modified formulaς:
(7)
ς
=
(
p
1
∨
q
1
)
∧
⋯
∧
(
p
n
∨
q
n
)
∧
(
¬
∃
R
·
(
A
,
B
)
)
∧
(
∀
R
·
(
¬
A
)
)
.To avoid an exponential (2
n) search in the case ofς, a form ofdependency directed backtracking calledbackjumping can be adapted, which has also been used, for example, in solving constraint satisfiability problems [21] and (in a slightly different form) in the HARP theorem prover [22]. The arithmetic labels each formulaςin a nodevwith a dependency setdep
(
ς
,
v
)indicating the branching points on which it depends.In case nodev is with dep
(
ς
,
¬
ς
)
∈
Σ
(
v
), dep
(
ς
,
v
) and dep
(
¬
ς
,
v
) are used to identify the most recent branching point b on which ς or ¬
ς depends. If the dependance exists, the algorithm can then jump back tobover intervening branching points without exploring any alternative branches (nondeterministic choices) and make a different nondeterministic choice which might not lead to the same closure condition being encountered. Figure 1 illustrates how the expansion belowvis pruned by backjumping, with the number ofR-s
u
c
c
e
s
s
o
r
sexplored being reduced by2
n
-
1. We will go into particulars in Algorithm 2. In case no suchbexists, the clash did not depend on any nondeterministic choice, and the algorithm stops, reporting the unsatisfiability of the TBox [20].Figure 1
Runing the search using backjumping.


#### 4.2.2. Global Caching

In order to avoid the same subproblem being solved again and again, it is possible to cache and reuse the results of such subproblems. The usual technique is to use a hash table to store the satisfiability status of node labels (i.e., sets of concepts treated as a conjunction). At present, there are various caching methods briefly outlined in [23]:(i)
no caching DFS (NC),
(ii)
unsat caching DFS (UC),
(iii)
mixed caching DFS (MC),
(iv)
unrestricted global caching and propagation (GC-NonDFS),
(v)
global caching DFS with propagation (GC-DFS).Global caching means that each possible set of concepts/formulas is expanded at most once. With respect to the size of the given problem, the notion of global caching is an ExpTime complexity procedure if the search space contains at most an exponential number of different nodes and as long as the extension of each node requires at most exponential time.


#### 4.2.3.  Optimized GLB

From Table2, we can conclude that an L-𝒮
ℋ
ℐ
𝒩 ABox 𝒜 can contain a number of positive or negative assertions without forming a contradiction. Therefore, it is useful to compute lower and upper bounds of finite lattice degree.Given a fuzzy KBΣ and an assertionα, it is absorbing to compute best lower and upper truth-value bounds ofα. To this end we define thegreatest lower bound ofαwith respect to Σ(denoted byglb
(
Σ
,
α
)
)to be⊕
{
l
∣
Σ
⊨
〈
α
⪰
l
〉
}. Similarly, we define theleast upper bound ofαwith respect to Σ (denoted bylub
(
Σ
,
α
)
) to be⊗
{
l
∣
Σ
⊨
〈
α
⪯
l
〉
}. lub
(
Σ
,
α
)
)could be computed from theglbaslub
(
Σ
,
α
)
) = ~
glb
(
Σ
,
~
α
)
) because~
lub
(
Σ
,
α
)
) = ~
⊗
{
l
∣
Σ
⊨
〈
α
⪯
l
〉
}=⊗
{
~
l
∣
Σ
⊨
〈
α
⪯
l
〉
} = ⊗
{
l
∣
Σ
⊨
〈
α
⪯
~
l
〉
} = ⊕
{
l
∣
Σ
⊨
〈
~
α
⪰
l
〉
} = ~
glb
(
Σ
,
~
α
)
). Determining theluband theglbis called theBest Lattice Degree Bound (BLDB) problem.Concerning the BCVB problem, we may have a similar algorithm as for fuzzy𝒜
ℒ
𝒞 [9], and an optimization in the search space is to use binary search algorithm reducing in that way the satisfiability checks required. Let glb
(
Σ
,
α
)
∈
N
Σ and lub
(
Σ
,
α
)
∈
1
-
N
Σ, where N
Σ
=
{
0,0.5,1
}
∪
{
l
:
〈
α
≥
c
〉
∈
Σ
}
∪
{
1
-
l
:
〈
α
≤
l
〉
∈
Σ
} and1
-
N
Σ
=
{
(
1
-
l
)
:
l
∈
N
Σ
}. We employ the binary search algorithm, assuming that0.5is the middle if we sort the elements ofN
Σ. We evaluate if Σ
⊨
(
x
:
C
)
≥
0.5is satisfied, in case it is we move on to higher degree until Σ
⊭
(
x
:
C
)
≥
n, indicating that the previous degree is theglb
(
Σ
,
(
x
:
C
)
).Let us assume thatℒ
=
〈
l
,
⪯
〉is a linear order,N
Σis ordered by ascending linear order, and∥
N
Σ
∥is the numbers of lattice degrees. A simple iterative approximation algorithm computing glb
(
Σ
,
α
)is described in Algorithm 1. The similar algorithm can be easily constructed for thelub.Algorithm 1:Calculate glb.
Data: Let t
∈
ℕ
+, t
≈
m
/
2, d
¯
,
d
t
∈
N
Σ, d
¯
=
d
t.
Result:  glb
(
Σ
,
α
)
=
d
¯.
begin
while  ∥
N
Σ
∥
>
1  do
if  Σ
⊨
〈
α
⪰
d
t
〉  then
d
¯
=
d
t
N
Σ
←
N
Σ
∖
{
d
′: d
′
⋡
d
¯
∪
{
d
¯
}
}
d
t
←
d
t
+
1
else
N
Σ
←
N
Σ
∖
{
d
′: d
′
⪰
d
¯
}
d
t
←
d
t
-
1Algorithm 2:A optimized decision procedure for checking satisfiability in L-𝒮
ℋ
ℐ
𝒩.
Input: A TBox 𝒯 in NNF and a finite set of concepts X in NNF
Output: an and-or forest G
=
〈
V
,
E
〉, with σ
∈
V as the initial node such that σ
.
s
t
a
t
u
s
=
{
s
at, unsat}
begin
create a new node σ with Σ
(
σ
)
:
=
X
∪
𝒯 and σ
.
s
t
a
t
u
s = unexpanded;
let V
:
=
{
σ
}, E
:
=
∅;
(a)  while  v
.
status
∉{sat, unsat}  do
(b)choose an node v
∈
V, v
.
s
t
a
t
u
s  := unexpanded;
if no L-𝒮
ℋ
ℐ
𝒩-tableau  rule  is  applicable  to Σ
(
v
)  then
v
.
s
t
a
t
u
s
=
{
sat};
else if  ⊥ is applicable to Σ
(
v
)  then
v
.
s
t
a
t
u
s
=
{
unsat};
else if  γ  (
γ
∈
γ
1
) is  applicable  to Σ
(
v
) giving  concept Y  then
v
.
k
i
n
d:= and-node, Θ
:
=
{
Y
};
else if  γ  (
γ
∈
γ
2
) is  applicable  to Σ
(
v
) giving  concepts Y
1 and Y
2  then
v
.
k
i
n
d:= or-node, Θ
:
=
{
Y
1
,
Y
2
};
else
(i)v
.
k
i
n
d:= and-node;
(ii) for every∃
R
·
C
∈
ℒ
(
v
), apply γ  (
γ
∈
γ
3
) to Σ
(
v
) giving concept t
r
a
n
s
R
(
Σ
(
v
)
,
R
)
∪
{
C
}
∪
𝒯 and add this
concept toΘ;
(c)for  ∀
Y
∈
Θ  do
(i)if  s
o
m
e  w
∈
V has Σ
(
w
)
=
Y  then
then add edge (v
,
w) to E;
(ii) letw be a new node, set Σ
(
w
)
:
=
Y, w
.
s
t
a
t
u
s:= unexpanded, add w to V, and add edge (v
,
w) to E;
(d)if (v.kind = or-node and  one  of  the  successors  of v has  status sat) or (v.kind = and-node and all the
successors ofv have status sat) then
v
.
s
t
a
t
u
s:= sat, propagate(v);
else if (v.kind = and-node and  one  of  the  successors  of v has  status unsat) or (v.kind = or-node and all the
successors ofv have status unsat) then
v
.
s
t
a
t
u
s
≔
unsat, propagate(v);
else
v
.
s
t
a
t
u
s:= expanded;
(e)if  v
.
s
t
a
t
u
s = unsat  and  v in 𝒯, {
κ
,
¬
κ
}
∈
Σ
(
v
)  then
dep
(
κ
,
v
)
∪
dep
(
¬
κ
,
v
);
else if  v
.
s
t
a
t
u
s:= unexpanded  then
if  Σ
(
v
) is of the form κ
1
∨
κ
2  then
save(T
s);
addκ
1 to Σ
(
v
) with dep
(
κ
1
,
v
)
=
{
b
}
∪
dep
(
Σ
(
v
)
,
v
);
(f)if  b
∈
S  then
addκ
2 to Σ
(
v
) with dep
(
κ
2
,
v
)
=
b
∪
d;
else
break;
(g)  If  σ
.
s
t
a
t
u
s = unsat  then
return false;
else
return true;The described optimizations in Algorithm1 for glb are very effective since they reduce the search space of tableau independently ofΣused. Based on the previous partition based on connectivity optimization, we could select a partition𝒜
′where the individual of assertionαis contained. Thus a new set of membership degrees only for it withN
𝒜
′
⊆
N
Σis evaluated, resulting to greatly less satisfiability checks.Proposition 14.
By using a binary search onN
Σ, theglb
(
Σ
,
α
)problem inL-𝒮
ℋ
ℐ
𝒩 with respect to witnessed models can be decided in 𝒪
(
log
⁡
|
N
Σ
|
).Proof.
The complexity of ordering and determiningN
Σare 𝒪
(
|
N
Σ
|
·
log
⁡
|
Σ
|
)and 𝒪
(
Σ
), respectively. Hence, the value ofglb
(
Σ
,
α
)can be determined in at most 𝒪
(
log
⁡
|
N
Σ
|
)fuzzy entailment tests.
Moreover, the performance of calculatingglbcan be further improved by preventing recurrent expansion of the expansion rules in 𝒯. When ℱ in which no expansion rule can apply, which is then added to the cached completion-forest.


## 4.1. Preprocessing Optimisations

In case of obvious clash detection or cycle via concept names, preprocessing optimisations (e.g.,absorption ortold cycle elimination) can lead to important speedup of the subsequent reasoning process. These optimisations serve to preprocess and simplify the input into a form more amenable to later processing [18]. Furthermore, these optimisations are not specific to tableau-based fuzzy reasoners and may also be useful with other kinds of fuzzy DL reasoners. Herein on the basis ofL-𝒮
ℋ
ℐ
𝒩, we apply two striking optimizations techniques to our design and implement.


### 4.1.1. Partition Based on Connectivity

Partition based on connectivity is a quite effective optimization technique to boost up the performance of reasoning, which can be applied to any fuzzy DL without nominals independently of the fuzzy operators used to provide the interpretations [17]. Termination of the expansion of the completion forest is a result of the properties of the expansion rules in Table 3, and a tableau expansion rule can either add (i) a new neighbour node to the node of examination, (ii) new membership triples in this node, or (iii) new membership triples to neighbouring nodes. The expansion rule will examine the different ways that the tableau expansion rules affect this completion forest, with the respect of different connectivity circumstances. Inspired by the work in [17], we have the following definitions.Definition 11.
Leta, b, c
∈
I, ℓ
∈
L. The connection relation between two individualsa, bin an ABox 𝒜 is inductively defined through role R
A:
(5)
a
↭
𝒜
b
⟺
{
R
A
(
a
,
b
)
⋈
l
∈
𝒜
derectly
connected
(
a
↭
𝒜
c
)
∪
(
b
↭
𝒜
c
)
inderectly
connected
.Note thatcmay be run into an iterative process for connecting indirectly. The individuals in the ABox 𝒜 may be divided into one or more individual groups. Then individual group is partitioned into one or more independent subsets calledAssertion Groups (
A
G
) [16]. For instance, two assertionsA
1andA
2are in the same A
G ifA
1is directly or indirectly inferred fromA
2(through the application of completion rules), orA
1andA
2differ only in terms of their certainty values and/or conjunction and disjunction functions. Each group is composed of individuals that are connected to each other through role assertionsR
A.Definition 12.
We denoteA
G
[
a
]with the partition of the ABox 𝒜 that contains only connected individuals in 𝒜
(6)
A
G
[
a
]
=
{
a
}
∪
{
x
∣
∀
x
∈
I
,
a
↭
𝒜
x
}
.Proposition 13.
It holds that
(1)
∪
A
G
i
=
𝒜,
(2)
A
G
i
∩
A
G
j
=
∅,for each pair
A
G
i
,
A
G
j
∈
A
such that
A
G
i
=
A
G
j,
(3)
𝒜
is consistent with respect to a TBox
𝒯
if and only if each
A
G
i
is consistent with respect to a TBox
𝒯.Partition based on connectivity optimization technique has several advantages. First, it is of polynomial complexity and it can be applied to any fuzzy DL. In addition, If anyA
G is found to be inconsistent, this implies that the whole 𝒜 is inconsistent. A related benefit is to more precisely identify the assertions that cause the inconsistency. Finally, the speed of solving a few small constraint sets would be faster than solving one large constraint set.


### 4.1.2. Dealt with TBox Axioms

If dealt with axioms of TBox𝒯 naively, which maybe lead to a serious degradation in reasoning performance, as each such axiom would cause a disjunction to be added to every node of the completion forest, leading to potentially enormous amounts on nondeterministic expansion [18].Givenς
∈
𝒯, withς
=
(
(
C
1
∨
D
1
)
∧
⋯
∧
(
C
n
∨
D
n
)
), testing the satisfiability ofςleads to the construction of a completion forest containingknodes, then there are2
k
ndifferent ways to apply the ⊓- and ⊔-rules to the resultingkcopies ofA, which leads to the explosion in the size of the search space. Fortunately, some notable works of optimisations known aslazy unfolding andabsorption had been used to identifying these problems [19]. Herein we chooselazy unfolding optimisation to address this issue. Due to the limitation of the paper, detailed definition oflazy unfolding is omitted here, and we refer the reader to the above literatures.


## 4.1.1. Partition Based on Connectivity

Partition based on connectivity is a quite effective optimization technique to boost up the performance of reasoning, which can be applied to any fuzzy DL without nominals independently of the fuzzy operators used to provide the interpretations [17]. Termination of the expansion of the completion forest is a result of the properties of the expansion rules in Table 3, and a tableau expansion rule can either add (i) a new neighbour node to the node of examination, (ii) new membership triples in this node, or (iii) new membership triples to neighbouring nodes. The expansion rule will examine the different ways that the tableau expansion rules affect this completion forest, with the respect of different connectivity circumstances. Inspired by the work in [17], we have the following definitions.Definition 11.
Leta, b, c
∈
I, ℓ
∈
L. The connection relation between two individualsa, bin an ABox 𝒜 is inductively defined through role R
A:
(5)
a
↭
𝒜
b
⟺
{
R
A
(
a
,
b
)
⋈
l
∈
𝒜
derectly
connected
(
a
↭
𝒜
c
)
∪
(
b
↭
𝒜
c
)
inderectly
connected
.Note thatcmay be run into an iterative process for connecting indirectly. The individuals in the ABox 𝒜 may be divided into one or more individual groups. Then individual group is partitioned into one or more independent subsets calledAssertion Groups (
A
G
) [16]. For instance, two assertionsA
1andA
2are in the same A
G ifA
1is directly or indirectly inferred fromA
2(through the application of completion rules), orA
1andA
2differ only in terms of their certainty values and/or conjunction and disjunction functions. Each group is composed of individuals that are connected to each other through role assertionsR
A.Definition 12.
We denoteA
G
[
a
]with the partition of the ABox 𝒜 that contains only connected individuals in 𝒜
(6)
A
G
[
a
]
=
{
a
}
∪
{
x
∣
∀
x
∈
I
,
a
↭
𝒜
x
}
.Proposition 13.
It holds that
(1)
∪
A
G
i
=
𝒜,
(2)
A
G
i
∩
A
G
j
=
∅,for each pair
A
G
i
,
A
G
j
∈
A
such that
A
G
i
=
A
G
j,
(3)
𝒜
is consistent with respect to a TBox
𝒯
if and only if each
A
G
i
is consistent with respect to a TBox
𝒯.Partition based on connectivity optimization technique has several advantages. First, it is of polynomial complexity and it can be applied to any fuzzy DL. In addition, If anyA
G is found to be inconsistent, this implies that the whole 𝒜 is inconsistent. A related benefit is to more precisely identify the assertions that cause the inconsistency. Finally, the speed of solving a few small constraint sets would be faster than solving one large constraint set.


## 4.1.2. Dealt with TBox Axioms

If dealt with axioms of TBox𝒯 naively, which maybe lead to a serious degradation in reasoning performance, as each such axiom would cause a disjunction to be added to every node of the completion forest, leading to potentially enormous amounts on nondeterministic expansion [18].Givenς
∈
𝒯, withς
=
(
(
C
1
∨
D
1
)
∧
⋯
∧
(
C
n
∨
D
n
)
), testing the satisfiability ofςleads to the construction of a completion forest containingknodes, then there are2
k
ndifferent ways to apply the ⊓- and ⊔-rules to the resultingkcopies ofA, which leads to the explosion in the size of the search space. Fortunately, some notable works of optimisations known aslazy unfolding andabsorption had been used to identifying these problems [19]. Herein we chooselazy unfolding optimisation to address this issue. Due to the limitation of the paper, detailed definition oflazy unfolding is omitted here, and we refer the reader to the above literatures.


## 4.2.  Core Satisfiability Optimisations

In the following, we present core reasoning ofL-𝒮
ℋ
ℐ
𝒩, a satisfiability checking algorithm, which implements a highly optimised version on the basis of the tableau algorithm described in Section 3. Before introducing the optimisations extended to the naive tableau algorithm, we present a brief introduction tobackjumpingandglobal cachingand show how such algorithms are implemented in practice.


### 4.2.1. Dependency Directed Backtracking (Backjumping)

Backjumping is an optimisation that is crucial for effective tableau based reasoning. Inherent unsatisfiability concealed in subformulae can lead to large amounts of unproductive backtracking search known as thrashing, especially if the unsatisfiability caused by the modal subformulae had been slightly less trivial [20]. Consider the following modified formulaς:
(7)
ς
=
(
p
1
∨
q
1
)
∧
⋯
∧
(
p
n
∨
q
n
)
∧
(
¬
∃
R
·
(
A
,
B
)
)
∧
(
∀
R
·
(
¬
A
)
)
.To avoid an exponential (2
n) search in the case ofς, a form ofdependency directed backtracking calledbackjumping can be adapted, which has also been used, for example, in solving constraint satisfiability problems [21] and (in a slightly different form) in the HARP theorem prover [22]. The arithmetic labels each formulaςin a nodevwith a dependency setdep
(
ς
,
v
)indicating the branching points on which it depends.In case nodev is with dep
(
ς
,
¬
ς
)
∈
Σ
(
v
), dep
(
ς
,
v
) and dep
(
¬
ς
,
v
) are used to identify the most recent branching point b on which ς or ¬
ς depends. If the dependance exists, the algorithm can then jump back tobover intervening branching points without exploring any alternative branches (nondeterministic choices) and make a different nondeterministic choice which might not lead to the same closure condition being encountered. Figure 1 illustrates how the expansion belowvis pruned by backjumping, with the number ofR-s
u
c
c
e
s
s
o
r
sexplored being reduced by2
n
-
1. We will go into particulars in Algorithm 2. In case no suchbexists, the clash did not depend on any nondeterministic choice, and the algorithm stops, reporting the unsatisfiability of the TBox [20].Figure 1
Runing the search using backjumping.


### 4.2.2. Global Caching

In order to avoid the same subproblem being solved again and again, it is possible to cache and reuse the results of such subproblems. The usual technique is to use a hash table to store the satisfiability status of node labels (i.e., sets of concepts treated as a conjunction). At present, there are various caching methods briefly outlined in [23]:(i)
no caching DFS (NC),
(ii)
unsat caching DFS (UC),
(iii)
mixed caching DFS (MC),
(iv)
unrestricted global caching and propagation (GC-NonDFS),
(v)
global caching DFS with propagation (GC-DFS).Global caching means that each possible set of concepts/formulas is expanded at most once. With respect to the size of the given problem, the notion of global caching is an ExpTime complexity procedure if the search space contains at most an exponential number of different nodes and as long as the extension of each node requires at most exponential time.


### 4.2.3.  Optimized GLB

From Table2, we can conclude that an L-𝒮
ℋ
ℐ
𝒩 ABox 𝒜 can contain a number of positive or negative assertions without forming a contradiction. Therefore, it is useful to compute lower and upper bounds of finite lattice degree.Given a fuzzy KBΣ and an assertionα, it is absorbing to compute best lower and upper truth-value bounds ofα. To this end we define thegreatest lower bound ofαwith respect to Σ(denoted byglb
(
Σ
,
α
)
)to be⊕
{
l
∣
Σ
⊨
〈
α
⪰
l
〉
}. Similarly, we define theleast upper bound ofαwith respect to Σ (denoted bylub
(
Σ
,
α
)
) to be⊗
{
l
∣
Σ
⊨
〈
α
⪯
l
〉
}. lub
(
Σ
,
α
)
)could be computed from theglbaslub
(
Σ
,
α
)
) = ~
glb
(
Σ
,
~
α
)
) because~
lub
(
Σ
,
α
)
) = ~
⊗
{
l
∣
Σ
⊨
〈
α
⪯
l
〉
}=⊗
{
~
l
∣
Σ
⊨
〈
α
⪯
l
〉
} = ⊗
{
l
∣
Σ
⊨
〈
α
⪯
~
l
〉
} = ⊕
{
l
∣
Σ
⊨
〈
~
α
⪰
l
〉
} = ~
glb
(
Σ
,
~
α
)
). Determining theluband theglbis called theBest Lattice Degree Bound (BLDB) problem.Concerning the BCVB problem, we may have a similar algorithm as for fuzzy𝒜
ℒ
𝒞 [9], and an optimization in the search space is to use binary search algorithm reducing in that way the satisfiability checks required. Let glb
(
Σ
,
α
)
∈
N
Σ and lub
(
Σ
,
α
)
∈
1
-
N
Σ, where N
Σ
=
{
0,0.5,1
}
∪
{
l
:
〈
α
≥
c
〉
∈
Σ
}
∪
{
1
-
l
:
〈
α
≤
l
〉
∈
Σ
} and1
-
N
Σ
=
{
(
1
-
l
)
:
l
∈
N
Σ
}. We employ the binary search algorithm, assuming that0.5is the middle if we sort the elements ofN
Σ. We evaluate if Σ
⊨
(
x
:
C
)
≥
0.5is satisfied, in case it is we move on to higher degree until Σ
⊭
(
x
:
C
)
≥
n, indicating that the previous degree is theglb
(
Σ
,
(
x
:
C
)
).Let us assume thatℒ
=
〈
l
,
⪯
〉is a linear order,N
Σis ordered by ascending linear order, and∥
N
Σ
∥is the numbers of lattice degrees. A simple iterative approximation algorithm computing glb
(
Σ
,
α
)is described in Algorithm 1. The similar algorithm can be easily constructed for thelub.Algorithm 1:Calculate glb.
Data: Let t
∈
ℕ
+, t
≈
m
/
2, d
¯
,
d
t
∈
N
Σ, d
¯
=
d
t.
Result:  glb
(
Σ
,
α
)
=
d
¯.
begin
while  ∥
N
Σ
∥
>
1  do
if  Σ
⊨
〈
α
⪰
d
t
〉  then
d
¯
=
d
t
N
Σ
←
N
Σ
∖
{
d
′: d
′
⋡
d
¯
∪
{
d
¯
}
}
d
t
←
d
t
+
1
else
N
Σ
←
N
Σ
∖
{
d
′: d
′
⪰
d
¯
}
d
t
←
d
t
-
1Algorithm 2:A optimized decision procedure for checking satisfiability in L-𝒮
ℋ
ℐ
𝒩.
Input: A TBox 𝒯 in NNF and a finite set of concepts X in NNF
Output: an and-or forest G
=
〈
V
,
E
〉, with σ
∈
V as the initial node such that σ
.
s
t
a
t
u
s
=
{
s
at, unsat}
begin
create a new node σ with Σ
(
σ
)
:
=
X
∪
𝒯 and σ
.
s
t
a
t
u
s = unexpanded;
let V
:
=
{
σ
}, E
:
=
∅;
(a)  while  v
.
status
∉{sat, unsat}  do
(b)choose an node v
∈
V, v
.
s
t
a
t
u
s  := unexpanded;
if no L-𝒮
ℋ
ℐ
𝒩-tableau  rule  is  applicable  to Σ
(
v
)  then
v
.
s
t
a
t
u
s
=
{
sat};
else if  ⊥ is applicable to Σ
(
v
)  then
v
.
s
t
a
t
u
s
=
{
unsat};
else if  γ  (
γ
∈
γ
1
) is  applicable  to Σ
(
v
) giving  concept Y  then
v
.
k
i
n
d:= and-node, Θ
:
=
{
Y
};
else if  γ  (
γ
∈
γ
2
) is  applicable  to Σ
(
v
) giving  concepts Y
1 and Y
2  then
v
.
k
i
n
d:= or-node, Θ
:
=
{
Y
1
,
Y
2
};
else
(i)v
.
k
i
n
d:= and-node;
(ii) for every∃
R
·
C
∈
ℒ
(
v
), apply γ  (
γ
∈
γ
3
) to Σ
(
v
) giving concept t
r
a
n
s
R
(
Σ
(
v
)
,
R
)
∪
{
C
}
∪
𝒯 and add this
concept toΘ;
(c)for  ∀
Y
∈
Θ  do
(i)if  s
o
m
e  w
∈
V has Σ
(
w
)
=
Y  then
then add edge (v
,
w) to E;
(ii) letw be a new node, set Σ
(
w
)
:
=
Y, w
.
s
t
a
t
u
s:= unexpanded, add w to V, and add edge (v
,
w) to E;
(d)if (v.kind = or-node and  one  of  the  successors  of v has  status sat) or (v.kind = and-node and all the
successors ofv have status sat) then
v
.
s
t
a
t
u
s:= sat, propagate(v);
else if (v.kind = and-node and  one  of  the  successors  of v has  status unsat) or (v.kind = or-node and all the
successors ofv have status unsat) then
v
.
s
t
a
t
u
s
≔
unsat, propagate(v);
else
v
.
s
t
a
t
u
s:= expanded;
(e)if  v
.
s
t
a
t
u
s = unsat  and  v in 𝒯, {
κ
,
¬
κ
}
∈
Σ
(
v
)  then
dep
(
κ
,
v
)
∪
dep
(
¬
κ
,
v
);
else if  v
.
s
t
a
t
u
s:= unexpanded  then
if  Σ
(
v
) is of the form κ
1
∨
κ
2  then
save(T
s);
addκ
1 to Σ
(
v
) with dep
(
κ
1
,
v
)
=
{
b
}
∪
dep
(
Σ
(
v
)
,
v
);
(f)if  b
∈
S  then
addκ
2 to Σ
(
v
) with dep
(
κ
2
,
v
)
=
b
∪
d;
else
break;
(g)  If  σ
.
s
t
a
t
u
s = unsat  then
return false;
else
return true;The described optimizations in Algorithm1 for glb are very effective since they reduce the search space of tableau independently ofΣused. Based on the previous partition based on connectivity optimization, we could select a partition𝒜
′where the individual of assertionαis contained. Thus a new set of membership degrees only for it withN
𝒜
′
⊆
N
Σis evaluated, resulting to greatly less satisfiability checks.Proposition 14.
By using a binary search onN
Σ, theglb
(
Σ
,
α
)problem inL-𝒮
ℋ
ℐ
𝒩 with respect to witnessed models can be decided in 𝒪
(
log
⁡
|
N
Σ
|
).Proof.
The complexity of ordering and determiningN
Σare 𝒪
(
|
N
Σ
|
·
log
⁡
|
Σ
|
)and 𝒪
(
Σ
), respectively. Hence, the value ofglb
(
Σ
,
α
)can be determined in at most 𝒪
(
log
⁡
|
N
Σ
|
)fuzzy entailment tests.
Moreover, the performance of calculatingglbcan be further improved by preventing recurrent expansion of the expansion rules in 𝒯. When ℱ in which no expansion rule can apply, which is then added to the cached completion-forest.


## 4.2.1. Dependency Directed Backtracking (Backjumping)

Backjumping is an optimisation that is crucial for effective tableau based reasoning. Inherent unsatisfiability concealed in subformulae can lead to large amounts of unproductive backtracking search known as thrashing, especially if the unsatisfiability caused by the modal subformulae had been slightly less trivial [20]. Consider the following modified formulaς:
(7)
ς
=
(
p
1
∨
q
1
)
∧
⋯
∧
(
p
n
∨
q
n
)
∧
(
¬
∃
R
·
(
A
,
B
)
)
∧
(
∀
R
·
(
¬
A
)
)
.To avoid an exponential (2
n) search in the case ofς, a form ofdependency directed backtracking calledbackjumping can be adapted, which has also been used, for example, in solving constraint satisfiability problems [21] and (in a slightly different form) in the HARP theorem prover [22]. The arithmetic labels each formulaςin a nodevwith a dependency setdep
(
ς
,
v
)indicating the branching points on which it depends.In case nodev is with dep
(
ς
,
¬
ς
)
∈
Σ
(
v
), dep
(
ς
,
v
) and dep
(
¬
ς
,
v
) are used to identify the most recent branching point b on which ς or ¬
ς depends. If the dependance exists, the algorithm can then jump back tobover intervening branching points without exploring any alternative branches (nondeterministic choices) and make a different nondeterministic choice which might not lead to the same closure condition being encountered. Figure 1 illustrates how the expansion belowvis pruned by backjumping, with the number ofR-s
u
c
c
e
s
s
o
r
sexplored being reduced by2
n
-
1. We will go into particulars in Algorithm 2. In case no suchbexists, the clash did not depend on any nondeterministic choice, and the algorithm stops, reporting the unsatisfiability of the TBox [20].Figure 1
Runing the search using backjumping.


## 4.2.2. Global Caching

In order to avoid the same subproblem being solved again and again, it is possible to cache and reuse the results of such subproblems. The usual technique is to use a hash table to store the satisfiability status of node labels (i.e., sets of concepts treated as a conjunction). At present, there are various caching methods briefly outlined in [23]:(i)
no caching DFS (NC),
(ii)
unsat caching DFS (UC),
(iii)
mixed caching DFS (MC),
(iv)
unrestricted global caching and propagation (GC-NonDFS),
(v)
global caching DFS with propagation (GC-DFS).Global caching means that each possible set of concepts/formulas is expanded at most once. With respect to the size of the given problem, the notion of global caching is an ExpTime complexity procedure if the search space contains at most an exponential number of different nodes and as long as the extension of each node requires at most exponential time.


## 4.2.3.  Optimized GLB

From Table2, we can conclude that an L-𝒮
ℋ
ℐ
𝒩 ABox 𝒜 can contain a number of positive or negative assertions without forming a contradiction. Therefore, it is useful to compute lower and upper bounds of finite lattice degree.Given a fuzzy KBΣ and an assertionα, it is absorbing to compute best lower and upper truth-value bounds ofα. To this end we define thegreatest lower bound ofαwith respect to Σ(denoted byglb
(
Σ
,
α
)
)to be⊕
{
l
∣
Σ
⊨
〈
α
⪰
l
〉
}. Similarly, we define theleast upper bound ofαwith respect to Σ (denoted bylub
(
Σ
,
α
)
) to be⊗
{
l
∣
Σ
⊨
〈
α
⪯
l
〉
}. lub
(
Σ
,
α
)
)could be computed from theglbaslub
(
Σ
,
α
)
) = ~
glb
(
Σ
,
~
α
)
) because~
lub
(
Σ
,
α
)
) = ~
⊗
{
l
∣
Σ
⊨
〈
α
⪯
l
〉
}=⊗
{
~
l
∣
Σ
⊨
〈
α
⪯
l
〉
} = ⊗
{
l
∣
Σ
⊨
〈
α
⪯
~
l
〉
} = ⊕
{
l
∣
Σ
⊨
〈
~
α
⪰
l
〉
} = ~
glb
(
Σ
,
~
α
)
). Determining theluband theglbis called theBest Lattice Degree Bound (BLDB) problem.Concerning the BCVB problem, we may have a similar algorithm as for fuzzy𝒜
ℒ
𝒞 [9], and an optimization in the search space is to use binary search algorithm reducing in that way the satisfiability checks required. Let glb
(
Σ
,
α
)
∈
N
Σ and lub
(
Σ
,
α
)
∈
1
-
N
Σ, where N
Σ
=
{
0,0.5,1
}
∪
{
l
:
〈
α
≥
c
〉
∈
Σ
}
∪
{
1
-
l
:
〈
α
≤
l
〉
∈
Σ
} and1
-
N
Σ
=
{
(
1
-
l
)
:
l
∈
N
Σ
}. We employ the binary search algorithm, assuming that0.5is the middle if we sort the elements ofN
Σ. We evaluate if Σ
⊨
(
x
:
C
)
≥
0.5is satisfied, in case it is we move on to higher degree until Σ
⊭
(
x
:
C
)
≥
n, indicating that the previous degree is theglb
(
Σ
,
(
x
:
C
)
).Let us assume thatℒ
=
〈
l
,
⪯
〉is a linear order,N
Σis ordered by ascending linear order, and∥
N
Σ
∥is the numbers of lattice degrees. A simple iterative approximation algorithm computing glb
(
Σ
,
α
)is described in Algorithm 1. The similar algorithm can be easily constructed for thelub.Algorithm 1:Calculate glb.
Data: Let t
∈
ℕ
+, t
≈
m
/
2, d
¯
,
d
t
∈
N
Σ, d
¯
=
d
t.
Result:  glb
(
Σ
,
α
)
=
d
¯.
begin
while  ∥
N
Σ
∥
>
1  do
if  Σ
⊨
〈
α
⪰
d
t
〉  then
d
¯
=
d
t
N
Σ
←
N
Σ
∖
{
d
′: d
′
⋡
d
¯
∪
{
d
¯
}
}
d
t
←
d
t
+
1
else
N
Σ
←
N
Σ
∖
{
d
′: d
′
⪰
d
¯
}
d
t
←
d
t
-
1Algorithm 2:A optimized decision procedure for checking satisfiability in L-𝒮
ℋ
ℐ
𝒩.
Input: A TBox 𝒯 in NNF and a finite set of concepts X in NNF
Output: an and-or forest G
=
〈
V
,
E
〉, with σ
∈
V as the initial node such that σ
.
s
t
a
t
u
s
=
{
s
at, unsat}
begin
create a new node σ with Σ
(
σ
)
:
=
X
∪
𝒯 and σ
.
s
t
a
t
u
s = unexpanded;
let V
:
=
{
σ
}, E
:
=
∅;
(a)  while  v
.
status
∉{sat, unsat}  do
(b)choose an node v
∈
V, v
.
s
t
a
t
u
s  := unexpanded;
if no L-𝒮
ℋ
ℐ
𝒩-tableau  rule  is  applicable  to Σ
(
v
)  then
v
.
s
t
a
t
u
s
=
{
sat};
else if  ⊥ is applicable to Σ
(
v
)  then
v
.
s
t
a
t
u
s
=
{
unsat};
else if  γ  (
γ
∈
γ
1
) is  applicable  to Σ
(
v
) giving  concept Y  then
v
.
k
i
n
d:= and-node, Θ
:
=
{
Y
};
else if  γ  (
γ
∈
γ
2
) is  applicable  to Σ
(
v
) giving  concepts Y
1 and Y
2  then
v
.
k
i
n
d:= or-node, Θ
:
=
{
Y
1
,
Y
2
};
else
(i)v
.
k
i
n
d:= and-node;
(ii) for every∃
R
·
C
∈
ℒ
(
v
), apply γ  (
γ
∈
γ
3
) to Σ
(
v
) giving concept t
r
a
n
s
R
(
Σ
(
v
)
,
R
)
∪
{
C
}
∪
𝒯 and add this
concept toΘ;
(c)for  ∀
Y
∈
Θ  do
(i)if  s
o
m
e  w
∈
V has Σ
(
w
)
=
Y  then
then add edge (v
,
w) to E;
(ii) letw be a new node, set Σ
(
w
)
:
=
Y, w
.
s
t
a
t
u
s:= unexpanded, add w to V, and add edge (v
,
w) to E;
(d)if (v.kind = or-node and  one  of  the  successors  of v has  status sat) or (v.kind = and-node and all the
successors ofv have status sat) then
v
.
s
t
a
t
u
s:= sat, propagate(v);
else if (v.kind = and-node and  one  of  the  successors  of v has  status unsat) or (v.kind = or-node and all the
successors ofv have status unsat) then
v
.
s
t
a
t
u
s
≔
unsat, propagate(v);
else
v
.
s
t
a
t
u
s:= expanded;
(e)if  v
.
s
t
a
t
u
s = unsat  and  v in 𝒯, {
κ
,
¬
κ
}
∈
Σ
(
v
)  then
dep
(
κ
,
v
)
∪
dep
(
¬
κ
,
v
);
else if  v
.
s
t
a
t
u
s:= unexpanded  then
if  Σ
(
v
) is of the form κ
1
∨
κ
2  then
save(T
s);
addκ
1 to Σ
(
v
) with dep
(
κ
1
,
v
)
=
{
b
}
∪
dep
(
Σ
(
v
)
,
v
);
(f)if  b
∈
S  then
addκ
2 to Σ
(
v
) with dep
(
κ
2
,
v
)
=
b
∪
d;
else
break;
(g)  If  σ
.
s
t
a
t
u
s = unsat  then
return false;
else
return true;The described optimizations in Algorithm1 for glb are very effective since they reduce the search space of tableau independently ofΣused. Based on the previous partition based on connectivity optimization, we could select a partition𝒜
′where the individual of assertionαis contained. Thus a new set of membership degrees only for it withN
𝒜
′
⊆
N
Σis evaluated, resulting to greatly less satisfiability checks.Proposition 14.
By using a binary search onN
Σ, theglb
(
Σ
,
α
)problem inL-𝒮
ℋ
ℐ
𝒩 with respect to witnessed models can be decided in 𝒪
(
log
⁡
|
N
Σ
|
).Proof.
The complexity of ordering and determiningN
Σare 𝒪
(
|
N
Σ
|
·
log
⁡
|
Σ
|
)and 𝒪
(
Σ
), respectively. Hence, the value ofglb
(
Σ
,
α
)can be determined in at most 𝒪
(
log
⁡
|
N
Σ
|
)fuzzy entailment tests.
Moreover, the performance of calculatingglbcan be further improved by preventing recurrent expansion of the expansion rules in 𝒯. When ℱ in which no expansion rule can apply, which is then added to the cached completion-forest.


## 5. The Optimized Algorithm

### 5.1. Algorithm Overview

Our optimized algorithm builds a completion forestℱ consisting of a collection of trees whose distinguished roots are arbitrarily connected by edges. We firstly explain the structure of ℱ in more detail.Definition 15.
A nodevin the completion forest ℱ
=
〈
V
,
E
〉extends an and/or node which is a record with extra two attributes:s
t
s
v
∈
℘
?,kin
d
v
∈
ℑ
?, where℘:={
unexpanded
,
expanded
,
sat
⁡
,
unsat
}, ℑ:={
and-node
,
or-node
}The status of a non-leaf-node is computed from the status of itsR-s
u
c
c
e
s
s
o
rusing its kind (and-node/or-node) and treating satisfiability with respect to the TBox 𝒯 (i.e., sat) as true and unsatisfiability with respect to the 𝒯 (i.e. unsat) as false. When a node gets status  sat or unsat, the status can be propagated to itsR-p
r
e
d
e
c
e
s
s
o
rin a way appropriate to the forest and/or structure if desired.Anand-node (resp., or-node) becomes  unsat (resp., sat) if one of itsR-s
u
c
c
e
s
s
o
r
s becomes  unsat (resp.,sat). For the remaining case, an  and-node (resp.,  or-node) becomes  sat (resp.,   unsat) if the number of itsR-s
u
c
c
e
s
s
o
r
s withs
t
a
t
u
s
≠
s
a
t(resp.,≠
u
n
s
a
t) reduces to0.It is well known that different orders of expanding nondeterministic rules can result in huge (up to several orders of magnitude) differences in reasoning performance [24]. According to empirical analysis in [24], we have the definition as below.Definition 16.
In our terminology, the following ordering would be optimal for extending: the⊔-rule has the lowest priority, the generating rules (like the⩾-rule and the∃-rule) have the second-lowest priority, all other rules except for⩽
*have the second-highest priority, and the other rules have the highest priority.Instead of a top-down approach to most systems used for ordering expansion rules, we use a new ordering heuristic rule by anOrderedRule list to control the application of the expansion rules. The fundamental idea is that expansion rules may become applicable whenever a concept is added to a node label, then the node/concept pair is added to theOrderedRule list.Definition 17.
Granting the demand of Algorithm2, the tableau expansion rules in Table 3 are divided into three parts{
γ
1
,
γ
2
,
γ
3
}:γ
1:= {
⊓
⊳
,
⊓
⊲
,
∀
⊲
,
∀
⊳
,
∀
+
},
γ
2:= {
≤
⊲
,
≤
⊲
,
≤
⊳
,
≥
⊲
,
≤
r
⊳
,
≥
r
⊲
,
¬
⋈
,
⊔
⊲
,
⊓
⊳
},
γ
3:= {
∃
⊳
,
∃
⊲
,
∃
+
}.Additionally, we use aOrderedRule list to control the application of the expansion rules{
γ
1
,
γ
2
,
γ
3
}. TheOrderedRule list sorts all these entries according to the descending order queued above and gives access to the first element in the list. The strategy for rule applications given above is the standard one, by applying γ
1 and γ
2 rules as much as possible and then applying γ
3 rules to realise existential concepts. Besides, the strategy for choosing which node in the γ
i to expand next is in the descending order, and that means that,for example, ⊓
⊳ inγ
1 will be the first applied rule. The set Θ contains the contents of the resultingΣ
(
v
). If the applied tableau rule is inγ
1, then v has one formula in Θ; if the applied rule is in γ
2 then v has two formulae in Θ; otherwise, ∃
* supply one appropriate formula for Θ.


### 5.2.  The Optimized Algorithm Design

In the following, assumevis current expanded node,bis a nonnegative integer indicating the bth-∨rule application in the run of the tableau algorithm,dep
(
ς
,
v
)is a formulaςin the label of a nodevwith a dependency set if a nodevcontains both{
κ
,
¬
κ
}
∈
Σ
(
v
),Yis finite sets of concepts, and the setΛcontains the contents of the resultingY.To check whether a given finite setX is satisfiable in 𝒯, where 𝒯 is a Box, the content of the initial nodeσwith status unexpanded isX
∪
T. Initially, the queue of nodesVset covers initially only root nodeσbut can grow as the algorithm proceeds. Next, we present an Exptime decision procedure forL-𝒮
ℋ
ℐ
𝒩 to create a completion forest and/or structure.We comment on Algorithm2 given in pseudocode, which determines whether a concept X
∈
𝒜 is satisfiable with respect to a TBox 𝒯, both in NNF. The main while-loop (at line (a)) continues processing nodes until the status ofσis determined to be in{
s
a
t
,
unsat
}, or until every node is expanded, whichever happens first.Inside the main loop, we choose an unexpanded node (at line (b)) and try to apply one and only one of the tableau rules in the orderγ
1, γ
2, γ
3to the current nodev. If the applied tableau rule is withinγ
1, thenvhas oneY; or, if the applied rule is withinγ
2, thenvhasY
1, Y
2; otherwise, apply(
∃
⊳
)and(
∃
⊲
)toΣ
(
v
)giving concept t
r
a
n
s
R
(
Σ
(
v
)
,
R
)
∪
{
C
}
∪
𝒯 and add this concept toΘ.After that, for everyY inΘ(at line (c)), we create the required successor in the ℱ only if it does not yet exist. Then, the procedure attempts to compute the status of such a non-leaf-nodevemploying the kind (or-node/and-node) ofvand the status of theR-s
u
c
c
e
s
s
o
rofv, regarding u
n
s
a
t as irrevocably false and s
a
t as irrevocably true.On the condition that previous two steps cannot determine the status ofvass
a
t or u
n
s
a
t, then its status is set to be expanded. On the other side, if so (at line (d)), this information is itself propagated toR-p
r
e
d
e
c
e
s
s
o
rofvin the ℱ via the routine p
r
o
p
a
g
a
t
e
(
v
).Sequentially, ifv
.
s
t
a
t
u
s
=
u
n
s
a
t andv in 𝒯 (at line (e)),{
κ
,
¬
κ
}
∈
Σ
(
v
), then the closure dependency setS
:
=
dep
(
κ
,
v
)
∪
dep
(
¬
κ
,
v
), and the algorithm backtracks to thenth branching point bto apply bth-*-rule application. 𝒯 would be restored to its state prior to addingκ
1toΣ
(
v
), and the rule would be applied again such thatκ
2was added toΣ
(
v
).Using backjumping, the algorithm will return without expanding the completion trees obtained by adding the variousκ
2toΣ
(
v
)immediately (at line (f)) becauseb
∉
S. Satisfiable will eventually return∅, concluding thatXis unsatisfiable.Ifσ
.
s
t
a
t
u
s
=
unsat(at line (g)), the result isfalse, otherwisetrue.Proposition 18.
Letℱ be constructed by Algorithm 2 for Σ
(
v
)andΓ, withσas the initial node. Then Σ
(
v
)is satisfiable with respect toΓif and only ifσ.status =  sat.Lemma 19.
Algorithm2 assumes that Σ
(
v
)is consistent and constructs a model ofΓthat satisfies Σ
(
v
). Let ℱ
=
〈
V
,
E
〉be the completion forest constructed by the algorithm for Σ
(
v
)
∪
Γ. Suppose the set of concepts carried by the nodev
∈
Visℏ
(
v
), for everyv
∈
V, ifv.status =  unsat, thenℏ
(
v
)is inconsistent with respect toΓ.Proof (sketch)..
Sincevonly depends on its successors and by copying nodes to ensure that the resulting structure is a completion-tree tableau, we can construct a closed tableau with respect toΓfor the set of concepts carried by the nodevby induction.


### 5.3.  Computational Complexity of the Optimized Algorithm

We proceed to analyse the runtime of the global caching algorithm, under suitable sanity assumptions on the set of modal rules. Specifically, in order to ensure that executions of the algorithm run in exponential time, we need to assumenis the size of input, that is, the sum of the size of Σ
(
v
)
∪
Γ. This construction uses bothcaching andbackjumping techniques.Proposition 20.
Algorithm2 runs in ExpTime.Proof (sketch)..
Sinceℏ
(
v
)
⊆
S
(
Σ
(
v
)
∪
Γ
), so the set contains2
𝒪
(
n
)concepts. Omitting the execution time of procedurepropagate, everyv
∈
Vis expanded only once and every expansion takes2
𝒪
(
n
)time units.
Whenv
.
s
t
a
t
u
sbecomes  sat or  unsat, thepropagate procedure executes2
𝒪
(
n
)basic steps directly involved withv, so the total time of the executions ofpropagate is of rank2
2
·
𝒪
(
n
).
Using backjumping, the algorithm returns frombth branching point immediately becauseb
∉
S. This is obviously true for all of the preceding branching points, so all calls tob-th branching point will return without expanding the completion trees toΣ
(
v
). So that the size of Σ
(
v
)
∪
Γcan be further reduced.


## 5.1. Algorithm Overview

Our optimized algorithm builds a completion forestℱ consisting of a collection of trees whose distinguished roots are arbitrarily connected by edges. We firstly explain the structure of ℱ in more detail.Definition 15.
A nodevin the completion forest ℱ
=
〈
V
,
E
〉extends an and/or node which is a record with extra two attributes:s
t
s
v
∈
℘
?,kin
d
v
∈
ℑ
?, where℘:={
unexpanded
,
expanded
,
sat
⁡
,
unsat
}, ℑ:={
and-node
,
or-node
}The status of a non-leaf-node is computed from the status of itsR-s
u
c
c
e
s
s
o
rusing its kind (and-node/or-node) and treating satisfiability with respect to the TBox 𝒯 (i.e., sat) as true and unsatisfiability with respect to the 𝒯 (i.e. unsat) as false. When a node gets status  sat or unsat, the status can be propagated to itsR-p
r
e
d
e
c
e
s
s
o
rin a way appropriate to the forest and/or structure if desired.Anand-node (resp., or-node) becomes  unsat (resp., sat) if one of itsR-s
u
c
c
e
s
s
o
r
s becomes  unsat (resp.,sat). For the remaining case, an  and-node (resp.,  or-node) becomes  sat (resp.,   unsat) if the number of itsR-s
u
c
c
e
s
s
o
r
s withs
t
a
t
u
s
≠
s
a
t(resp.,≠
u
n
s
a
t) reduces to0.It is well known that different orders of expanding nondeterministic rules can result in huge (up to several orders of magnitude) differences in reasoning performance [24]. According to empirical analysis in [24], we have the definition as below.Definition 16.
In our terminology, the following ordering would be optimal for extending: the⊔-rule has the lowest priority, the generating rules (like the⩾-rule and the∃-rule) have the second-lowest priority, all other rules except for⩽
*have the second-highest priority, and the other rules have the highest priority.Instead of a top-down approach to most systems used for ordering expansion rules, we use a new ordering heuristic rule by anOrderedRule list to control the application of the expansion rules. The fundamental idea is that expansion rules may become applicable whenever a concept is added to a node label, then the node/concept pair is added to theOrderedRule list.Definition 17.
Granting the demand of Algorithm2, the tableau expansion rules in Table 3 are divided into three parts{
γ
1
,
γ
2
,
γ
3
}:γ
1:= {
⊓
⊳
,
⊓
⊲
,
∀
⊲
,
∀
⊳
,
∀
+
},
γ
2:= {
≤
⊲
,
≤
⊲
,
≤
⊳
,
≥
⊲
,
≤
r
⊳
,
≥
r
⊲
,
¬
⋈
,
⊔
⊲
,
⊓
⊳
},
γ
3:= {
∃
⊳
,
∃
⊲
,
∃
+
}.Additionally, we use aOrderedRule list to control the application of the expansion rules{
γ
1
,
γ
2
,
γ
3
}. TheOrderedRule list sorts all these entries according to the descending order queued above and gives access to the first element in the list. The strategy for rule applications given above is the standard one, by applying γ
1 and γ
2 rules as much as possible and then applying γ
3 rules to realise existential concepts. Besides, the strategy for choosing which node in the γ
i to expand next is in the descending order, and that means that,for example, ⊓
⊳ inγ
1 will be the first applied rule. The set Θ contains the contents of the resultingΣ
(
v
). If the applied tableau rule is inγ
1, then v has one formula in Θ; if the applied rule is in γ
2 then v has two formulae in Θ; otherwise, ∃
* supply one appropriate formula for Θ.


## 5.2.  The Optimized Algorithm Design

In the following, assumevis current expanded node,bis a nonnegative integer indicating the bth-∨rule application in the run of the tableau algorithm,dep
(
ς
,
v
)is a formulaςin the label of a nodevwith a dependency set if a nodevcontains both{
κ
,
¬
κ
}
∈
Σ
(
v
),Yis finite sets of concepts, and the setΛcontains the contents of the resultingY.To check whether a given finite setX is satisfiable in 𝒯, where 𝒯 is a Box, the content of the initial nodeσwith status unexpanded isX
∪
T. Initially, the queue of nodesVset covers initially only root nodeσbut can grow as the algorithm proceeds. Next, we present an Exptime decision procedure forL-𝒮
ℋ
ℐ
𝒩 to create a completion forest and/or structure.We comment on Algorithm2 given in pseudocode, which determines whether a concept X
∈
𝒜 is satisfiable with respect to a TBox 𝒯, both in NNF. The main while-loop (at line (a)) continues processing nodes until the status ofσis determined to be in{
s
a
t
,
unsat
}, or until every node is expanded, whichever happens first.Inside the main loop, we choose an unexpanded node (at line (b)) and try to apply one and only one of the tableau rules in the orderγ
1, γ
2, γ
3to the current nodev. If the applied tableau rule is withinγ
1, thenvhas oneY; or, if the applied rule is withinγ
2, thenvhasY
1, Y
2; otherwise, apply(
∃
⊳
)and(
∃
⊲
)toΣ
(
v
)giving concept t
r
a
n
s
R
(
Σ
(
v
)
,
R
)
∪
{
C
}
∪
𝒯 and add this concept toΘ.After that, for everyY inΘ(at line (c)), we create the required successor in the ℱ only if it does not yet exist. Then, the procedure attempts to compute the status of such a non-leaf-nodevemploying the kind (or-node/and-node) ofvand the status of theR-s
u
c
c
e
s
s
o
rofv, regarding u
n
s
a
t as irrevocably false and s
a
t as irrevocably true.On the condition that previous two steps cannot determine the status ofvass
a
t or u
n
s
a
t, then its status is set to be expanded. On the other side, if so (at line (d)), this information is itself propagated toR-p
r
e
d
e
c
e
s
s
o
rofvin the ℱ via the routine p
r
o
p
a
g
a
t
e
(
v
).Sequentially, ifv
.
s
t
a
t
u
s
=
u
n
s
a
t andv in 𝒯 (at line (e)),{
κ
,
¬
κ
}
∈
Σ
(
v
), then the closure dependency setS
:
=
dep
(
κ
,
v
)
∪
dep
(
¬
κ
,
v
), and the algorithm backtracks to thenth branching point bto apply bth-*-rule application. 𝒯 would be restored to its state prior to addingκ
1toΣ
(
v
), and the rule would be applied again such thatκ
2was added toΣ
(
v
).Using backjumping, the algorithm will return without expanding the completion trees obtained by adding the variousκ
2toΣ
(
v
)immediately (at line (f)) becauseb
∉
S. Satisfiable will eventually return∅, concluding thatXis unsatisfiable.Ifσ
.
s
t
a
t
u
s
=
unsat(at line (g)), the result isfalse, otherwisetrue.Proposition 18.
Letℱ be constructed by Algorithm 2 for Σ
(
v
)andΓ, withσas the initial node. Then Σ
(
v
)is satisfiable with respect toΓif and only ifσ.status =  sat.Lemma 19.
Algorithm2 assumes that Σ
(
v
)is consistent and constructs a model ofΓthat satisfies Σ
(
v
). Let ℱ
=
〈
V
,
E
〉be the completion forest constructed by the algorithm for Σ
(
v
)
∪
Γ. Suppose the set of concepts carried by the nodev
∈
Visℏ
(
v
), for everyv
∈
V, ifv.status =  unsat, thenℏ
(
v
)is inconsistent with respect toΓ.Proof (sketch)..
Sincevonly depends on its successors and by copying nodes to ensure that the resulting structure is a completion-tree tableau, we can construct a closed tableau with respect toΓfor the set of concepts carried by the nodevby induction.


## 5.3.  Computational Complexity of the Optimized Algorithm

We proceed to analyse the runtime of the global caching algorithm, under suitable sanity assumptions on the set of modal rules. Specifically, in order to ensure that executions of the algorithm run in exponential time, we need to assumenis the size of input, that is, the sum of the size of Σ
(
v
)
∪
Γ. This construction uses bothcaching andbackjumping techniques.Proposition 20.
Algorithm2 runs in ExpTime.Proof (sketch)..
Sinceℏ
(
v
)
⊆
S
(
Σ
(
v
)
∪
Γ
), so the set contains2
𝒪
(
n
)concepts. Omitting the execution time of procedurepropagate, everyv
∈
Vis expanded only once and every expansion takes2
𝒪
(
n
)time units.
Whenv
.
s
t
a
t
u
sbecomes  sat or  unsat, thepropagate procedure executes2
𝒪
(
n
)basic steps directly involved withv, so the total time of the executions ofpropagate is of rank2
2
·
𝒪
(
n
).
Using backjumping, the algorithm returns frombth branching point immediately becauseb
∉
S. This is obviously true for all of the preceding branching points, so all calls tob-th branching point will return without expanding the completion trees toΣ
(
v
). So that the size of Σ
(
v
)
∪
Γcan be further reduced.


## 6. Evaluation

In this section, we provide test results about the usefulness of the optimizations of our algorithm on the test from revised LogicsWork Bench (LWB) benchmarks [25] and the DL98 benchmarks (http://dL.kr.org/dl98/comparison/). All the experiments were conducted under Ubuntu 12.04 on a PC with 2.40 GHz Intel Core 2 CPU Q8300 and 2 GB RAM, using the 1s time limit for each test problem. We consider only the number of solved problems instead of the used CPU time.


### 6.1. Programming Language

The problem we are dealing with in this work is whether the optimized tableau algorithm proposed by us can be implemented to give an efficient prover forL-𝒮
ℋ
ℐ
𝒩. This problem can be raised as what optimization techniques can be implemented to obtain a prover forL-𝒮
ℋ
ℐ
𝒩 that is both optimal from the theoretical point of view and efficient in practice. To the best of our knowledge, there is no DL/uncertainty prover/reasoner forL-𝒮
ℋ
ℐ
𝒩. Thus we have developed in C++ a tableau prover forL-𝒮
ℋ
ℐ
𝒩, which uses serial of optimization methods described above.C++ is chosen to implement tableau prover because of its increase efficiency, portability, and extendibility. Pointers are intensively used for the data structures of the tableau prover to reduce memory use and to allow caching objects like formulas, sets of formulas, and nodes of a completion forest. Advanced data structures of C++ with low complexity like thetemplates set, map, multimap, and priority queue are also intensively used. And it is more convenient to extending it for other description logics in a modular way [26].


### 6.2.  Experimental Results on Usefulness of the Optimizations

Because neither do good benchmarks forL-𝒮
ℋ
ℐ
𝒩 seem to exist, so we found it hard to compile a good set of test problems. Although the Tableaux’98 and random test suites could show how optimisations perform on propositional modal logics, neither is very good for our purposes.We therefore recast the K, KT, and S4 problem sets from the LogicsWork Bench (LWB) benchmarks and theT98-sat problem set from the DL98 benchmarks (there are 4 sets of DL98 test suite, and onlyconcept satisfiability tests are employed) to be compatible with the fuzzy logicL-𝒮
ℋ
ℐ
𝒩 over finite lattices. Due to the space limit, we omit the detailed process of transformation. The three anterior benchmarks measure the performance of the system when testing the satisfiability of large concept expressions without reference to a Tbox. Moreover, DL98 TBox problem set textttT98-sat test is added to contain TBox axioms. The correctness of the system is also tested by checking that the answer is as expected.Our algorithm is fairly detailed, so a naive implementation should be straightforward. The preprocessing optimisations (“partition based on connectivity" and “dealting with TBox axioms”) described in Section4.1 take at most polynomial time to run and reduce the search space more significantly than the extended framework of Donini and Massacci [27]. So it is sensible to use them in almost every case in our tableau prover. After preprocessing, it is crucial to employ core satisfiability optimisations presented in Section 4.2 that try to improve the performance of the core satisfiability tester.We intend to show which of the optimisations are most effective, so we have had compile-time configuration options included that can be used to turn on and off or vary the previous optimisations. We chose to test various combinations with all the other optimisations enabled and then to test the same optimisations options, with each of the optimisations turned off one by one. The optimisations that were removed are as follows.(i)
ALL: turn on all the optimizations.
(ii)
No partition based on connectivity (NP): turn off ABox partition.
(iii)
No dealing with TBox axioms (ND): turn off dealing with TBox axioms.
(iv)
No backjumping (NB): turn off backjumping.
(v)
No global caching (NC): turn off global caching.We end up with 5 configurations and ran each of these configurations over the nine test suites from satisfiability checking problems. For the corresponding subset of tests and the corresponding set of options, each table cell includes the number of solved problems, where the diamond symbol denotes 21 (the number of test problems in the subset). For each configuration, there are five entries corresponding to timeouts of 1 second, 2 seconds, 4 seconds, 8 seconds, and 16 seconds.


#### 6.2.1. K(ℒ) Tests

Table4 obviously reveals that, amongst the tested configurations, turning on all the optimizations provides the most effective method. These two other optimisations are the most effective, whose absence in the experiments has made them unacceptably slow. For k_lin_n(ℒ) and k_lin_p(ℒ), the methods of global caching significantly outperform backjumping. There is a nice distinction between the two preprocessing optimisations methods. Partition based on connectivity and dealing with TBox axioms is less important at least within our set of test cases. For k_lin_n(ℒ), k_path_n(ℒ), and k_path_p(ℒ), “dealing with TBox axioms" significantly outperforms “partition based on connectivity," and for the other problems, “partition based on connectivity" outperforms “dealing with TBox axioms."Table 4
Results for K(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
k_branch_n(ℒ)
18⋄  ⋄  ⋄  ⋄
15  16  18  19⋄
17  20⋄  ⋄  ⋄
14  16  19  20⋄
7  9  10  12  15
k_branch_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
17  18  20⋄  ⋄
18  20⋄  ⋄  ⋄
17  19⋄  ⋄  ⋄
8  10  10  13  16
k_d4_n(ℒ)
10  11  12  14  14
5  6  6  7  7
7  7  8  8  9
4  4  5  6  6
3  4  4  5  6
k_d4_p(ℒ)
17  20⋄  ⋄  ⋄
6  6  7  7  7
8  8  9  9  9
3  4  5  6  8
4  4  4  5  5
k_dum_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
k_dum_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
18⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
k_lin_n(ℒ)
19⋄  ⋄  ⋄  ⋄
6  8  10  13  17
4  7  9  13  16
16  18  20⋄  ⋄
15  17  19  20⋄
k_lin_p(ℒ)
6  8  10  12  15
6  8  11  14  16
7  10  13  16  19
17  19⋄  ⋄  ⋄
15  17  19  20⋄
k_path_n(ℒ)
11  11  13  14  14
5  5  6  6  7
4  4  4  5  6
3  3  3  4  4
2  2  3  3  3
k_path_p(ℒ)
12  12  13  14  15
5  5  6  7  8
4  4  4  4  6
3  3  4  4  5
3  3  3  3  4
k_ph_n(ℒ)
8  8  9  10  10
8  8  8  8  9
8  8  8  9  10
8  8  8  8  8
7  7  7  7  8
k_ph_p(ℒ)
8  8  9  9  10
7  8  8  8  8
8  8  9  9  10
7  8  8  8  8
7  7  7  7  8
k_ploy_n(ℒ)
20⋄  ⋄  ⋄  ⋄
17  18  20⋄  ⋄
18  20⋄  ⋄  ⋄
11  12  13  14  16
8  9  9  10  11
k_ploy_p(ℒ)
19⋄  ⋄  ⋄  ⋄
18  19⋄  ⋄  ⋄
19  20⋄  ⋄  ⋄
11  12  14  15  17
9  10  11  12  14
k_t4p_n(ℒ)
20⋄  ⋄  ⋄  ⋄
11  12  14  16  17
12  14  16  17  19
6  7  8  8  10
4  5  5  6  7
k_t4p_p(ℒ)
20⋄  ⋄  ⋄  ⋄
11  13  15  17  18
12  15  17  18  20
6  7  9  10  12
4  4  5  5  6


#### 6.2.2. KT(ℒ) Tests

Similar testing was performed on KT(ℒ) tests, and results are showed in Table 5. Again, there is too much data to present it that global caching significantly outperforms other optimization methods in both of its incarnations. Particularly, we have undergone an increase of memory usage by a worst-case factor of two in case of backjumping in comparison to no backjumping. This time, for the most problems, the “partition based on connectivity” method is on par with “dealing with TBox axioms.”Table 5
Results for KT(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
kt_branch_n(ℒ)
10  11  12  14  14
5  6  6  7  7
7  7  8  8  9
4  4  5  6  6
3  4  4  5  6
kt_branch_p(ℒ)
17  20⋄  ⋄  ⋄
6  6  7  7  7
8  8  9  9  9
3  4  5  6  8
4  4  4  5  5
kt_45_n(ℒ)
8  9  10  11  12
8  9  10  11  12
8  9  10  11  12
8  9  10  11  13
8  9  10  11  12
kt_45_p(ℒ)
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
k_dum_n(ℒ)
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
17  19⋄  ⋄  ⋄
13  15  16  18  19
k_dum_p(ℒ)
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
18  20⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_md_n(ℒ)
8  8  8  9  9
8  8  8  8  9
7  7  7  7  8
6  6  7  7  7
4  4  4  4  5
k_md_p(ℒ)
7  7  7  7  8
8  8  9  9  9
6  7  7  7  7
6  7  7  7  7
3  3  3  4  4
k_path_n(ℒ)
4  4  4  5  5
4  4  4  5  5
4  4  4  4  5
3  4  4  4  4
3  3  3  4  4
k_path_p(ℒ)
4  5  5  5  6
4  4  5  5  5
4  4  4  5  5
3  3  4  4  4
3  3  4  4  4
k_ph_n(ℒ)
7  7  8  8  9
6  7  7  8  8
7  7  8  8  8
6  6  7  7  8
5  5  6  6  7
k_ph_p(ℒ)
6  7  7  8  8
6  6  7  7  8
6  6  7  7  8
6  7  7  8  8
5  6  6  7  7
k_ploy_n(ℒ)
4  4  5  6  6
4  4  5  5  6
4  5  5  5  6
3  3  5  5  5
2  2  4  4  4
k_ploy_p(ℒ)
8  8  10  10  11
8  8  10  10  10
8  8  9  10  10
6  6  9  9  10
4  4  6  6  7
k_t4p_n(ℒ)
3  3  5  5  6
3  3  4  5  6
3  3  4  4  6
2  2  3  4  4
1  1  3  3  3
k_t4p_p(ℒ)
5  5  7  7  7
5  5  6  7  7
5  5  7  7  7
1  2  2  4  4
1  1  2  2  3


#### 6.2.3. S4(ℒ) Tests

The results of S4(ℒ) tests, given in Table 6, show that backjumping performs very well compared to other methods. This result is surprising; global caching is less effective at almost all in this test suite. The probable reason for the ineffectiveness of the method is that, with such a small number of literals in the successor nodes, the purely propositional problems can always be worked out deterministically, while the performance is contingent on the efficiency of propositional reasoning at the root node.Table 6
Results for S4(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
s4_branch_n(ℒ)
10  11  12  13  15
9  10  11  12  14
8  9  10  11  12
8  9  10  12  13
8  9  10  11  13
s4_branch_p(ℒ)
12  13  14  16  17
11  12  13  14  15
10  11  12  13  14
10  11  13  14  16
10  11  13  14  16
s4_45_n(ℒ)
12  15  19⋄  ⋄
10  13  16  20⋄
9  12  15  18⋄
6  9  11  14  17
7  9  12  15  18
s4_45_p(ℒ)
15  19⋄  ⋄  ⋄
13  16  19⋄  ⋄
12  15  18  20⋄
9  12  16  20⋄
10  13  17  20⋄
s4_ipc_n(ℒ)
9  11  12  15  16
11  13  15  16  18
10  12  14  16  17
10  12  12  14  15
10  12  12  15  15
s4_ipc_p(ℒ)
16  19⋄  ⋄  ⋄
14  16  18  19⋄
15  17  19  20⋄
18⋄  ⋄  ⋄  ⋄
17  20⋄  ⋄  ⋄
s4_grz_n(ℒ)
18⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
s4_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
s4_md_n(ℒ)
8  8  9  9  10
7  8  8  9  9
6  6  7  7  8
5  6  6  7  7
6  6  7  7  8
s4_md_p(ℒ)
7  7  8  8  9
6  6  7  8  8
6  7  7  8  8
4  4  5  5  5
5  5  6  6  7
s4_path_n(ℒ)
3  3  3  3  4
2  3  3  3  3
2  3  3  3  3
3  4  4  4  4
3  3  3  3  3
s4_path_p(ℒ)
4  4  4  4  4
3  3  4  4  4
3  4  4  4  4
4  4  5  5  5
3  4  4  4  4
k_ph_n(ℒ)
9  9  9  10  10
8  9  9  9  10
8  8  9  9  10
8  8  8  9  9
10  10  10  10  11
k_ph_p(ℒ)
11  11  11  11  12
10  10  10  10  11
9  10  10  10  10
7  8  8  8  8
12  12  12  13  13
s4_s5_n(ℒ)
7  7  8  8  8
7  7  7  8  8
7  7  7  7  8
6  7  7  7  7
6  6  6  6  7
s4_s5_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
s4_t4p_n(ℒ)
3  4  4  6  7
3  3  4  6  7
3  3  4  6  6
2  2  3  3  4
1  1  3  3  4
s4_t4p_p(ℒ)
5  7  7  9  10
5  7  8  9  10
5  7  8  8  10
4  4  6  6  8
3  4  4  6  6There appears to be no clear winner between the two methods “partition based on connectivity” and “dealing with TBox axioms.” “Dealing with TBox axioms" method outperforms the “partition based on connectivity” method for most problems, and for the problems s4_ipc_p(ℒ) and s4_path_p(ℒ), “dealing with TBox axioms” method beats the “partition based on connectivity" method. However, the differences are not great.


#### 6.2.4. K(ℒ) TBox Tests

Due to latticed LWB benchmarks not covering TBox problem, so test on the test set DL’98 T98 kb is employed. As shown in Table7, in this test, “dealing with TBox axioms" is by far the most important optimisation. The next most important optimisations are global caching and backjumping. That is because of explosion in the large size of the search space (2
k
n) in the problems, which results in a destructive degradation in performance, even when optimisations such as global caching and backjumping are used. “Partition based on connectivity" method is almost totally ineffective.Table 7
Results for K(ℒ) TBox tests.
Problem
ALL
NP
ND
NB
NC
k_branch_n(ℒ)
5  5  6  6  7
5  5  5  6  7
4  5  5  6  6
4  4  5  5  6
5  5  6  6  7
k_branch_p(ℒ)
8  8  9  9  10
8  8  9  9  9
7  7  8  8  9
6  7  7  8  8
8  8  9  9  10
k_d4_n(ℒ)
4  5  5  5  6
4  4  5  5  6
3  3  4  5  6
3  3  4  4  5
4  5  5  5  5
k_d4_p(ℒ)
16  18  19  20⋄
15  18  19  20  20
13  15  17  18  18
14  14  15  16  17
13  15  16  17  18
k_dum_n(ℒ)
17  19  20⋄  ⋄
17  18  20⋄  ⋄
10  12  15  17  20
8  10  13  16  19
16  18  19  20⋄
k_dum_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
13  15  17  19⋄
12  14  16  18⋄
11  13  14  17  20
10  12  14  17  19
13  15  17  18  20
k_grz_p(ℒ)
6  9  11  14  16
5  8  10  13  15
5  7  9  11  15
4  6  9  11  13
4  7  10  12  14
k_lin_n(ℒ)
10  10  11  11  12
10  10  10  11  11
9  10  10  10  11
9  9  10  10  10
9  10  10  11  11
k_lin_p(ℒ)
7  7  7  8  8
7  7  7  7  8
6  6  7  7  8
6  6  7  7  7
6  6  7  7  7
k_path_n(ℒ)
12  12  13  14  14
11  12  13  13  14
6  6  9  10  10
5  5  7  7  7
11  12  13  13  14
k_path_p(ℒ)
14  14  15  15  16
13  14  14  15  15  11  11
9  9  11  12  12
7  7  8  9  9
10  10  11
k_ph_n(ℒ)
10  10  13  13  15
9  10  12  12  15
9  10  13  13  15
6  7  7  8  8
10  10  12  13  14
k_ph_p(ℒ)
12  12  16  16  19
11  12  15  16  18
10  11  14  14  14
8  8  10  10  11
10  10  12  12  13
k_ploy_n(ℒ)
16  19⋄  ⋄  ⋄
17  18  20⋄  ⋄
12  16  20⋄  ⋄
11  15  19  20⋄
12  16  20⋄  ⋄
k_ploy_p(ℒ)
18⋄  ⋄  ⋄  ⋄
17  20⋄  ⋄  ⋄
15  18⋄  ⋄  ⋄
14  17  20⋄  ⋄
14  17  19⋄  ⋄
k_t4p_n(ℒ)
7  9  11  14  17
7  9  11  15  17
6  8  10  13  15
4  7  9  13  16
5  7  9  12  15
k_t4p_p(ℒ)
10  13  15  17  20
10  12  15  17  19
7  11  14  16  18
6  10  13  15  18
6  10  13  15  17The results reveal that, amongst the tested configurations, global caching is more efficient over the other methods in most but not all cases. Since global caching severely prunes the search space by avoiding multiple expansions of the same node, by enabling greater propagation ofsat   and  unsat  via subset checking and hence allowing more cutoffs to be done [28]. Backjumping approach can be applied together with global caching well, which reduces the number of tested nondeterministic branches largely especially for S4(ℒ) Tests, while in particular, the method may increase memory usage. When considering TBox problem, “dealing with TBox axioms” is the most important optimisation. Sometimes “partition based on connectivity" method is very effective but not all the time.As shown in the test results, the difference between using preprocessing optimizations or not is less significant than the core satisfiability optimization at least within our set of test cases. Furthermore, preprocessing optimizations cooperates very well with core satisfiability optimization techniques in most of the time.


## 6.1. Programming Language

The problem we are dealing with in this work is whether the optimized tableau algorithm proposed by us can be implemented to give an efficient prover forL-𝒮
ℋ
ℐ
𝒩. This problem can be raised as what optimization techniques can be implemented to obtain a prover forL-𝒮
ℋ
ℐ
𝒩 that is both optimal from the theoretical point of view and efficient in practice. To the best of our knowledge, there is no DL/uncertainty prover/reasoner forL-𝒮
ℋ
ℐ
𝒩. Thus we have developed in C++ a tableau prover forL-𝒮
ℋ
ℐ
𝒩, which uses serial of optimization methods described above.C++ is chosen to implement tableau prover because of its increase efficiency, portability, and extendibility. Pointers are intensively used for the data structures of the tableau prover to reduce memory use and to allow caching objects like formulas, sets of formulas, and nodes of a completion forest. Advanced data structures of C++ with low complexity like thetemplates set, map, multimap, and priority queue are also intensively used. And it is more convenient to extending it for other description logics in a modular way [26].


## 6.2.  Experimental Results on Usefulness of the Optimizations

Because neither do good benchmarks forL-𝒮
ℋ
ℐ
𝒩 seem to exist, so we found it hard to compile a good set of test problems. Although the Tableaux’98 and random test suites could show how optimisations perform on propositional modal logics, neither is very good for our purposes.We therefore recast the K, KT, and S4 problem sets from the LogicsWork Bench (LWB) benchmarks and theT98-sat problem set from the DL98 benchmarks (there are 4 sets of DL98 test suite, and onlyconcept satisfiability tests are employed) to be compatible with the fuzzy logicL-𝒮
ℋ
ℐ
𝒩 over finite lattices. Due to the space limit, we omit the detailed process of transformation. The three anterior benchmarks measure the performance of the system when testing the satisfiability of large concept expressions without reference to a Tbox. Moreover, DL98 TBox problem set textttT98-sat test is added to contain TBox axioms. The correctness of the system is also tested by checking that the answer is as expected.Our algorithm is fairly detailed, so a naive implementation should be straightforward. The preprocessing optimisations (“partition based on connectivity" and “dealting with TBox axioms”) described in Section4.1 take at most polynomial time to run and reduce the search space more significantly than the extended framework of Donini and Massacci [27]. So it is sensible to use them in almost every case in our tableau prover. After preprocessing, it is crucial to employ core satisfiability optimisations presented in Section 4.2 that try to improve the performance of the core satisfiability tester.We intend to show which of the optimisations are most effective, so we have had compile-time configuration options included that can be used to turn on and off or vary the previous optimisations. We chose to test various combinations with all the other optimisations enabled and then to test the same optimisations options, with each of the optimisations turned off one by one. The optimisations that were removed are as follows.(i)
ALL: turn on all the optimizations.
(ii)
No partition based on connectivity (NP): turn off ABox partition.
(iii)
No dealing with TBox axioms (ND): turn off dealing with TBox axioms.
(iv)
No backjumping (NB): turn off backjumping.
(v)
No global caching (NC): turn off global caching.We end up with 5 configurations and ran each of these configurations over the nine test suites from satisfiability checking problems. For the corresponding subset of tests and the corresponding set of options, each table cell includes the number of solved problems, where the diamond symbol denotes 21 (the number of test problems in the subset). For each configuration, there are five entries corresponding to timeouts of 1 second, 2 seconds, 4 seconds, 8 seconds, and 16 seconds.


### 6.2.1. K(ℒ) Tests

Table4 obviously reveals that, amongst the tested configurations, turning on all the optimizations provides the most effective method. These two other optimisations are the most effective, whose absence in the experiments has made them unacceptably slow. For k_lin_n(ℒ) and k_lin_p(ℒ), the methods of global caching significantly outperform backjumping. There is a nice distinction between the two preprocessing optimisations methods. Partition based on connectivity and dealing with TBox axioms is less important at least within our set of test cases. For k_lin_n(ℒ), k_path_n(ℒ), and k_path_p(ℒ), “dealing with TBox axioms" significantly outperforms “partition based on connectivity," and for the other problems, “partition based on connectivity" outperforms “dealing with TBox axioms."Table 4
Results for K(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
k_branch_n(ℒ)
18⋄  ⋄  ⋄  ⋄
15  16  18  19⋄
17  20⋄  ⋄  ⋄
14  16  19  20⋄
7  9  10  12  15
k_branch_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
17  18  20⋄  ⋄
18  20⋄  ⋄  ⋄
17  19⋄  ⋄  ⋄
8  10  10  13  16
k_d4_n(ℒ)
10  11  12  14  14
5  6  6  7  7
7  7  8  8  9
4  4  5  6  6
3  4  4  5  6
k_d4_p(ℒ)
17  20⋄  ⋄  ⋄
6  6  7  7  7
8  8  9  9  9
3  4  5  6  8
4  4  4  5  5
k_dum_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
k_dum_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
18⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
k_lin_n(ℒ)
19⋄  ⋄  ⋄  ⋄
6  8  10  13  17
4  7  9  13  16
16  18  20⋄  ⋄
15  17  19  20⋄
k_lin_p(ℒ)
6  8  10  12  15
6  8  11  14  16
7  10  13  16  19
17  19⋄  ⋄  ⋄
15  17  19  20⋄
k_path_n(ℒ)
11  11  13  14  14
5  5  6  6  7
4  4  4  5  6
3  3  3  4  4
2  2  3  3  3
k_path_p(ℒ)
12  12  13  14  15
5  5  6  7  8
4  4  4  4  6
3  3  4  4  5
3  3  3  3  4
k_ph_n(ℒ)
8  8  9  10  10
8  8  8  8  9
8  8  8  9  10
8  8  8  8  8
7  7  7  7  8
k_ph_p(ℒ)
8  8  9  9  10
7  8  8  8  8
8  8  9  9  10
7  8  8  8  8
7  7  7  7  8
k_ploy_n(ℒ)
20⋄  ⋄  ⋄  ⋄
17  18  20⋄  ⋄
18  20⋄  ⋄  ⋄
11  12  13  14  16
8  9  9  10  11
k_ploy_p(ℒ)
19⋄  ⋄  ⋄  ⋄
18  19⋄  ⋄  ⋄
19  20⋄  ⋄  ⋄
11  12  14  15  17
9  10  11  12  14
k_t4p_n(ℒ)
20⋄  ⋄  ⋄  ⋄
11  12  14  16  17
12  14  16  17  19
6  7  8  8  10
4  5  5  6  7
k_t4p_p(ℒ)
20⋄  ⋄  ⋄  ⋄
11  13  15  17  18
12  15  17  18  20
6  7  9  10  12
4  4  5  5  6


### 6.2.2. KT(ℒ) Tests

Similar testing was performed on KT(ℒ) tests, and results are showed in Table 5. Again, there is too much data to present it that global caching significantly outperforms other optimization methods in both of its incarnations. Particularly, we have undergone an increase of memory usage by a worst-case factor of two in case of backjumping in comparison to no backjumping. This time, for the most problems, the “partition based on connectivity” method is on par with “dealing with TBox axioms.”Table 5
Results for KT(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
kt_branch_n(ℒ)
10  11  12  14  14
5  6  6  7  7
7  7  8  8  9
4  4  5  6  6
3  4  4  5  6
kt_branch_p(ℒ)
17  20⋄  ⋄  ⋄
6  6  7  7  7
8  8  9  9  9
3  4  5  6  8
4  4  4  5  5
kt_45_n(ℒ)
8  9  10  11  12
8  9  10  11  12
8  9  10  11  12
8  9  10  11  13
8  9  10  11  12
kt_45_p(ℒ)
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
k_dum_n(ℒ)
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
17  19⋄  ⋄  ⋄
13  15  16  18  19
k_dum_p(ℒ)
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
18  20⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_md_n(ℒ)
8  8  8  9  9
8  8  8  8  9
7  7  7  7  8
6  6  7  7  7
4  4  4  4  5
k_md_p(ℒ)
7  7  7  7  8
8  8  9  9  9
6  7  7  7  7
6  7  7  7  7
3  3  3  4  4
k_path_n(ℒ)
4  4  4  5  5
4  4  4  5  5
4  4  4  4  5
3  4  4  4  4
3  3  3  4  4
k_path_p(ℒ)
4  5  5  5  6
4  4  5  5  5
4  4  4  5  5
3  3  4  4  4
3  3  4  4  4
k_ph_n(ℒ)
7  7  8  8  9
6  7  7  8  8
7  7  8  8  8
6  6  7  7  8
5  5  6  6  7
k_ph_p(ℒ)
6  7  7  8  8
6  6  7  7  8
6  6  7  7  8
6  7  7  8  8
5  6  6  7  7
k_ploy_n(ℒ)
4  4  5  6  6
4  4  5  5  6
4  5  5  5  6
3  3  5  5  5
2  2  4  4  4
k_ploy_p(ℒ)
8  8  10  10  11
8  8  10  10  10
8  8  9  10  10
6  6  9  9  10
4  4  6  6  7
k_t4p_n(ℒ)
3  3  5  5  6
3  3  4  5  6
3  3  4  4  6
2  2  3  4  4
1  1  3  3  3
k_t4p_p(ℒ)
5  5  7  7  7
5  5  6  7  7
5  5  7  7  7
1  2  2  4  4
1  1  2  2  3


### 6.2.3. S4(ℒ) Tests

The results of S4(ℒ) tests, given in Table 6, show that backjumping performs very well compared to other methods. This result is surprising; global caching is less effective at almost all in this test suite. The probable reason for the ineffectiveness of the method is that, with such a small number of literals in the successor nodes, the purely propositional problems can always be worked out deterministically, while the performance is contingent on the efficiency of propositional reasoning at the root node.Table 6
Results for S4(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
s4_branch_n(ℒ)
10  11  12  13  15
9  10  11  12  14
8  9  10  11  12
8  9  10  12  13
8  9  10  11  13
s4_branch_p(ℒ)
12  13  14  16  17
11  12  13  14  15
10  11  12  13  14
10  11  13  14  16
10  11  13  14  16
s4_45_n(ℒ)
12  15  19⋄  ⋄
10  13  16  20⋄
9  12  15  18⋄
6  9  11  14  17
7  9  12  15  18
s4_45_p(ℒ)
15  19⋄  ⋄  ⋄
13  16  19⋄  ⋄
12  15  18  20⋄
9  12  16  20⋄
10  13  17  20⋄
s4_ipc_n(ℒ)
9  11  12  15  16
11  13  15  16  18
10  12  14  16  17
10  12  12  14  15
10  12  12  15  15
s4_ipc_p(ℒ)
16  19⋄  ⋄  ⋄
14  16  18  19⋄
15  17  19  20⋄
18⋄  ⋄  ⋄  ⋄
17  20⋄  ⋄  ⋄
s4_grz_n(ℒ)
18⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
s4_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
s4_md_n(ℒ)
8  8  9  9  10
7  8  8  9  9
6  6  7  7  8
5  6  6  7  7
6  6  7  7  8
s4_md_p(ℒ)
7  7  8  8  9
6  6  7  8  8
6  7  7  8  8
4  4  5  5  5
5  5  6  6  7
s4_path_n(ℒ)
3  3  3  3  4
2  3  3  3  3
2  3  3  3  3
3  4  4  4  4
3  3  3  3  3
s4_path_p(ℒ)
4  4  4  4  4
3  3  4  4  4
3  4  4  4  4
4  4  5  5  5
3  4  4  4  4
k_ph_n(ℒ)
9  9  9  10  10
8  9  9  9  10
8  8  9  9  10
8  8  8  9  9
10  10  10  10  11
k_ph_p(ℒ)
11  11  11  11  12
10  10  10  10  11
9  10  10  10  10
7  8  8  8  8
12  12  12  13  13
s4_s5_n(ℒ)
7  7  8  8  8
7  7  7  8  8
7  7  7  7  8
6  7  7  7  7
6  6  6  6  7
s4_s5_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
s4_t4p_n(ℒ)
3  4  4  6  7
3  3  4  6  7
3  3  4  6  6
2  2  3  3  4
1  1  3  3  4
s4_t4p_p(ℒ)
5  7  7  9  10
5  7  8  9  10
5  7  8  8  10
4  4  6  6  8
3  4  4  6  6There appears to be no clear winner between the two methods “partition based on connectivity” and “dealing with TBox axioms.” “Dealing with TBox axioms" method outperforms the “partition based on connectivity” method for most problems, and for the problems s4_ipc_p(ℒ) and s4_path_p(ℒ), “dealing with TBox axioms” method beats the “partition based on connectivity" method. However, the differences are not great.


### 6.2.4. K(ℒ) TBox Tests

Due to latticed LWB benchmarks not covering TBox problem, so test on the test set DL’98 T98 kb is employed. As shown in Table7, in this test, “dealing with TBox axioms" is by far the most important optimisation. The next most important optimisations are global caching and backjumping. That is because of explosion in the large size of the search space (2
k
n) in the problems, which results in a destructive degradation in performance, even when optimisations such as global caching and backjumping are used. “Partition based on connectivity" method is almost totally ineffective.Table 7
Results for K(ℒ) TBox tests.
Problem
ALL
NP
ND
NB
NC
k_branch_n(ℒ)
5  5  6  6  7
5  5  5  6  7
4  5  5  6  6
4  4  5  5  6
5  5  6  6  7
k_branch_p(ℒ)
8  8  9  9  10
8  8  9  9  9
7  7  8  8  9
6  7  7  8  8
8  8  9  9  10
k_d4_n(ℒ)
4  5  5  5  6
4  4  5  5  6
3  3  4  5  6
3  3  4  4  5
4  5  5  5  5
k_d4_p(ℒ)
16  18  19  20⋄
15  18  19  20  20
13  15  17  18  18
14  14  15  16  17
13  15  16  17  18
k_dum_n(ℒ)
17  19  20⋄  ⋄
17  18  20⋄  ⋄
10  12  15  17  20
8  10  13  16  19
16  18  19  20⋄
k_dum_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
13  15  17  19⋄
12  14  16  18⋄
11  13  14  17  20
10  12  14  17  19
13  15  17  18  20
k_grz_p(ℒ)
6  9  11  14  16
5  8  10  13  15
5  7  9  11  15
4  6  9  11  13
4  7  10  12  14
k_lin_n(ℒ)
10  10  11  11  12
10  10  10  11  11
9  10  10  10  11
9  9  10  10  10
9  10  10  11  11
k_lin_p(ℒ)
7  7  7  8  8
7  7  7  7  8
6  6  7  7  8
6  6  7  7  7
6  6  7  7  7
k_path_n(ℒ)
12  12  13  14  14
11  12  13  13  14
6  6  9  10  10
5  5  7  7  7
11  12  13  13  14
k_path_p(ℒ)
14  14  15  15  16
13  14  14  15  15  11  11
9  9  11  12  12
7  7  8  9  9
10  10  11
k_ph_n(ℒ)
10  10  13  13  15
9  10  12  12  15
9  10  13  13  15
6  7  7  8  8
10  10  12  13  14
k_ph_p(ℒ)
12  12  16  16  19
11  12  15  16  18
10  11  14  14  14
8  8  10  10  11
10  10  12  12  13
k_ploy_n(ℒ)
16  19⋄  ⋄  ⋄
17  18  20⋄  ⋄
12  16  20⋄  ⋄
11  15  19  20⋄
12  16  20⋄  ⋄
k_ploy_p(ℒ)
18⋄  ⋄  ⋄  ⋄
17  20⋄  ⋄  ⋄
15  18⋄  ⋄  ⋄
14  17  20⋄  ⋄
14  17  19⋄  ⋄
k_t4p_n(ℒ)
7  9  11  14  17
7  9  11  15  17
6  8  10  13  15
4  7  9  13  16
5  7  9  12  15
k_t4p_p(ℒ)
10  13  15  17  20
10  12  15  17  19
7  11  14  16  18
6  10  13  15  18
6  10  13  15  17The results reveal that, amongst the tested configurations, global caching is more efficient over the other methods in most but not all cases. Since global caching severely prunes the search space by avoiding multiple expansions of the same node, by enabling greater propagation ofsat   and  unsat  via subset checking and hence allowing more cutoffs to be done [28]. Backjumping approach can be applied together with global caching well, which reduces the number of tested nondeterministic branches largely especially for S4(ℒ) Tests, while in particular, the method may increase memory usage. When considering TBox problem, “dealing with TBox axioms” is the most important optimisation. Sometimes “partition based on connectivity" method is very effective but not all the time.As shown in the test results, the difference between using preprocessing optimizations or not is less significant than the core satisfiability optimization at least within our set of test cases. Furthermore, preprocessing optimizations cooperates very well with core satisfiability optimization techniques in most of the time.


## 6.2.1. K(ℒ) Tests

Table4 obviously reveals that, amongst the tested configurations, turning on all the optimizations provides the most effective method. These two other optimisations are the most effective, whose absence in the experiments has made them unacceptably slow. For k_lin_n(ℒ) and k_lin_p(ℒ), the methods of global caching significantly outperform backjumping. There is a nice distinction between the two preprocessing optimisations methods. Partition based on connectivity and dealing with TBox axioms is less important at least within our set of test cases. For k_lin_n(ℒ), k_path_n(ℒ), and k_path_p(ℒ), “dealing with TBox axioms" significantly outperforms “partition based on connectivity," and for the other problems, “partition based on connectivity" outperforms “dealing with TBox axioms."Table 4
Results for K(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
k_branch_n(ℒ)
18⋄  ⋄  ⋄  ⋄
15  16  18  19⋄
17  20⋄  ⋄  ⋄
14  16  19  20⋄
7  9  10  12  15
k_branch_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
17  18  20⋄  ⋄
18  20⋄  ⋄  ⋄
17  19⋄  ⋄  ⋄
8  10  10  13  16
k_d4_n(ℒ)
10  11  12  14  14
5  6  6  7  7
7  7  8  8  9
4  4  5  6  6
3  4  4  5  6
k_d4_p(ℒ)
17  20⋄  ⋄  ⋄
6  6  7  7  7
8  8  9  9  9
3  4  5  6  8
4  4  4  5  5
k_dum_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
k_dum_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
18⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
k_lin_n(ℒ)
19⋄  ⋄  ⋄  ⋄
6  8  10  13  17
4  7  9  13  16
16  18  20⋄  ⋄
15  17  19  20⋄
k_lin_p(ℒ)
6  8  10  12  15
6  8  11  14  16
7  10  13  16  19
17  19⋄  ⋄  ⋄
15  17  19  20⋄
k_path_n(ℒ)
11  11  13  14  14
5  5  6  6  7
4  4  4  5  6
3  3  3  4  4
2  2  3  3  3
k_path_p(ℒ)
12  12  13  14  15
5  5  6  7  8
4  4  4  4  6
3  3  4  4  5
3  3  3  3  4
k_ph_n(ℒ)
8  8  9  10  10
8  8  8  8  9
8  8  8  9  10
8  8  8  8  8
7  7  7  7  8
k_ph_p(ℒ)
8  8  9  9  10
7  8  8  8  8
8  8  9  9  10
7  8  8  8  8
7  7  7  7  8
k_ploy_n(ℒ)
20⋄  ⋄  ⋄  ⋄
17  18  20⋄  ⋄
18  20⋄  ⋄  ⋄
11  12  13  14  16
8  9  9  10  11
k_ploy_p(ℒ)
19⋄  ⋄  ⋄  ⋄
18  19⋄  ⋄  ⋄
19  20⋄  ⋄  ⋄
11  12  14  15  17
9  10  11  12  14
k_t4p_n(ℒ)
20⋄  ⋄  ⋄  ⋄
11  12  14  16  17
12  14  16  17  19
6  7  8  8  10
4  5  5  6  7
k_t4p_p(ℒ)
20⋄  ⋄  ⋄  ⋄
11  13  15  17  18
12  15  17  18  20
6  7  9  10  12
4  4  5  5  6


## 6.2.2. KT(ℒ) Tests

Similar testing was performed on KT(ℒ) tests, and results are showed in Table 5. Again, there is too much data to present it that global caching significantly outperforms other optimization methods in both of its incarnations. Particularly, we have undergone an increase of memory usage by a worst-case factor of two in case of backjumping in comparison to no backjumping. This time, for the most problems, the “partition based on connectivity” method is on par with “dealing with TBox axioms.”Table 5
Results for KT(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
kt_branch_n(ℒ)
10  11  12  14  14
5  6  6  7  7
7  7  8  8  9
4  4  5  6  6
3  4  4  5  6
kt_branch_p(ℒ)
17  20⋄  ⋄  ⋄
6  6  7  7  7
8  8  9  9  9
3  4  5  6  8
4  4  4  5  5
kt_45_n(ℒ)
8  9  10  11  12
8  9  10  11  12
8  9  10  11  12
8  9  10  11  13
8  9  10  11  12
kt_45_p(ℒ)
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
17  18  19  20⋄
k_dum_n(ℒ)
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
17  19⋄  ⋄  ⋄
13  15  16  18  19
k_dum_p(ℒ)
20⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
18  20⋄  ⋄  ⋄
19⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_md_n(ℒ)
8  8  8  9  9
8  8  8  8  9
7  7  7  7  8
6  6  7  7  7
4  4  4  4  5
k_md_p(ℒ)
7  7  7  7  8
8  8  9  9  9
6  7  7  7  7
6  7  7  7  7
3  3  3  4  4
k_path_n(ℒ)
4  4  4  5  5
4  4  4  5  5
4  4  4  4  5
3  4  4  4  4
3  3  3  4  4
k_path_p(ℒ)
4  5  5  5  6
4  4  5  5  5
4  4  4  5  5
3  3  4  4  4
3  3  4  4  4
k_ph_n(ℒ)
7  7  8  8  9
6  7  7  8  8
7  7  8  8  8
6  6  7  7  8
5  5  6  6  7
k_ph_p(ℒ)
6  7  7  8  8
6  6  7  7  8
6  6  7  7  8
6  7  7  8  8
5  6  6  7  7
k_ploy_n(ℒ)
4  4  5  6  6
4  4  5  5  6
4  5  5  5  6
3  3  5  5  5
2  2  4  4  4
k_ploy_p(ℒ)
8  8  10  10  11
8  8  10  10  10
8  8  9  10  10
6  6  9  9  10
4  4  6  6  7
k_t4p_n(ℒ)
3  3  5  5  6
3  3  4  5  6
3  3  4  4  6
2  2  3  4  4
1  1  3  3  3
k_t4p_p(ℒ)
5  5  7  7  7
5  5  6  7  7
5  5  7  7  7
1  2  2  4  4
1  1  2  2  3


## 6.2.3. S4(ℒ) Tests

The results of S4(ℒ) tests, given in Table 6, show that backjumping performs very well compared to other methods. This result is surprising; global caching is less effective at almost all in this test suite. The probable reason for the ineffectiveness of the method is that, with such a small number of literals in the successor nodes, the purely propositional problems can always be worked out deterministically, while the performance is contingent on the efficiency of propositional reasoning at the root node.Table 6
Results for S4(ℒ) tests.
Problem
ALL
NP
ND
NB
NC
s4_branch_n(ℒ)
10  11  12  13  15
9  10  11  12  14
8  9  10  11  12
8  9  10  12  13
8  9  10  11  13
s4_branch_p(ℒ)
12  13  14  16  17
11  12  13  14  15
10  11  12  13  14
10  11  13  14  16
10  11  13  14  16
s4_45_n(ℒ)
12  15  19⋄  ⋄
10  13  16  20⋄
9  12  15  18⋄
6  9  11  14  17
7  9  12  15  18
s4_45_p(ℒ)
15  19⋄  ⋄  ⋄
13  16  19⋄  ⋄
12  15  18  20⋄
9  12  16  20⋄
10  13  17  20⋄
s4_ipc_n(ℒ)
9  11  12  15  16
11  13  15  16  18
10  12  14  16  17
10  12  12  14  15
10  12  12  15  15
s4_ipc_p(ℒ)
16  19⋄  ⋄  ⋄
14  16  18  19⋄
15  17  19  20⋄
18⋄  ⋄  ⋄  ⋄
17  20⋄  ⋄  ⋄
s4_grz_n(ℒ)
18⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
s4_grz_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
s4_md_n(ℒ)
8  8  9  9  10
7  8  8  9  9
6  6  7  7  8
5  6  6  7  7
6  6  7  7  8
s4_md_p(ℒ)
7  7  8  8  9
6  6  7  8  8
6  7  7  8  8
4  4  5  5  5
5  5  6  6  7
s4_path_n(ℒ)
3  3  3  3  4
2  3  3  3  3
2  3  3  3  3
3  4  4  4  4
3  3  3  3  3
s4_path_p(ℒ)
4  4  4  4  4
3  3  4  4  4
3  4  4  4  4
4  4  5  5  5
3  4  4  4  4
k_ph_n(ℒ)
9  9  9  10  10
8  9  9  9  10
8  8  9  9  10
8  8  8  9  9
10  10  10  10  11
k_ph_p(ℒ)
11  11  11  11  12
10  10  10  10  11
9  10  10  10  10
7  8  8  8  8
12  12  12  13  13
s4_s5_n(ℒ)
7  7  8  8  8
7  7  7  8  8
7  7  7  7  8
6  7  7  7  7
6  6  6  6  7
s4_s5_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
s4_t4p_n(ℒ)
3  4  4  6  7
3  3  4  6  7
3  3  4  6  6
2  2  3  3  4
1  1  3  3  4
s4_t4p_p(ℒ)
5  7  7  9  10
5  7  8  9  10
5  7  8  8  10
4  4  6  6  8
3  4  4  6  6There appears to be no clear winner between the two methods “partition based on connectivity” and “dealing with TBox axioms.” “Dealing with TBox axioms" method outperforms the “partition based on connectivity” method for most problems, and for the problems s4_ipc_p(ℒ) and s4_path_p(ℒ), “dealing with TBox axioms” method beats the “partition based on connectivity" method. However, the differences are not great.


## 6.2.4. K(ℒ) TBox Tests

Due to latticed LWB benchmarks not covering TBox problem, so test on the test set DL’98 T98 kb is employed. As shown in Table7, in this test, “dealing with TBox axioms" is by far the most important optimisation. The next most important optimisations are global caching and backjumping. That is because of explosion in the large size of the search space (2
k
n) in the problems, which results in a destructive degradation in performance, even when optimisations such as global caching and backjumping are used. “Partition based on connectivity" method is almost totally ineffective.Table 7
Results for K(ℒ) TBox tests.
Problem
ALL
NP
ND
NB
NC
k_branch_n(ℒ)
5  5  6  6  7
5  5  5  6  7
4  5  5  6  6
4  4  5  5  6
5  5  6  6  7
k_branch_p(ℒ)
8  8  9  9  10
8  8  9  9  9
7  7  8  8  9
6  7  7  8  8
8  8  9  9  10
k_d4_n(ℒ)
4  5  5  5  6
4  4  5  5  6
3  3  4  5  6
3  3  4  4  5
4  5  5  5  5
k_d4_p(ℒ)
16  18  19  20⋄
15  18  19  20  20
13  15  17  18  18
14  14  15  16  17
13  15  16  17  18
k_dum_n(ℒ)
17  19  20⋄  ⋄
17  18  20⋄  ⋄
10  12  15  17  20
8  10  13  16  19
16  18  19  20⋄
k_dum_p(ℒ)
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
20⋄  ⋄  ⋄  ⋄
⋄  ⋄  ⋄  ⋄  ⋄
k_grz_n(ℒ)
13  15  17  19⋄
12  14  16  18⋄
11  13  14  17  20
10  12  14  17  19
13  15  17  18  20
k_grz_p(ℒ)
6  9  11  14  16
5  8  10  13  15
5  7  9  11  15
4  6  9  11  13
4  7  10  12  14
k_lin_n(ℒ)
10  10  11  11  12
10  10  10  11  11
9  10  10  10  11
9  9  10  10  10
9  10  10  11  11
k_lin_p(ℒ)
7  7  7  8  8
7  7  7  7  8
6  6  7  7  8
6  6  7  7  7
6  6  7  7  7
k_path_n(ℒ)
12  12  13  14  14
11  12  13  13  14
6  6  9  10  10
5  5  7  7  7
11  12  13  13  14
k_path_p(ℒ)
14  14  15  15  16
13  14  14  15  15  11  11
9  9  11  12  12
7  7  8  9  9
10  10  11
k_ph_n(ℒ)
10  10  13  13  15
9  10  12  12  15
9  10  13  13  15
6  7  7  8  8
10  10  12  13  14
k_ph_p(ℒ)
12  12  16  16  19
11  12  15  16  18
10  11  14  14  14
8  8  10  10  11
10  10  12  12  13
k_ploy_n(ℒ)
16  19⋄  ⋄  ⋄
17  18  20⋄  ⋄
12  16  20⋄  ⋄
11  15  19  20⋄
12  16  20⋄  ⋄
k_ploy_p(ℒ)
18⋄  ⋄  ⋄  ⋄
17  20⋄  ⋄  ⋄
15  18⋄  ⋄  ⋄
14  17  20⋄  ⋄
14  17  19⋄  ⋄
k_t4p_n(ℒ)
7  9  11  14  17
7  9  11  15  17
6  8  10  13  15
4  7  9  13  16
5  7  9  12  15
k_t4p_p(ℒ)
10  13  15  17  20
10  12  15  17  19
7  11  14  16  18
6  10  13  15  18
6  10  13  15  17The results reveal that, amongst the tested configurations, global caching is more efficient over the other methods in most but not all cases. Since global caching severely prunes the search space by avoiding multiple expansions of the same node, by enabling greater propagation ofsat   and  unsat  via subset checking and hence allowing more cutoffs to be done [28]. Backjumping approach can be applied together with global caching well, which reduces the number of tested nondeterministic branches largely especially for S4(ℒ) Tests, while in particular, the method may increase memory usage. When considering TBox problem, “dealing with TBox axioms” is the most important optimisation. Sometimes “partition based on connectivity" method is very effective but not all the time.As shown in the test results, the difference between using preprocessing optimizations or not is less significant than the core satisfiability optimization at least within our set of test cases. Furthermore, preprocessing optimizations cooperates very well with core satisfiability optimization techniques in most of the time.


## 7.  Conclusion and Future Work

Many papers offer technical contributions but without practical motivations. Our method forL-𝒮
ℋ
ℐ
𝒩 is definitely promising and should be extended to more expressive logics to test whether it remains feasible. In the further way, the tableau algorithm can be used on the large scale data set such as linked data to solve the practical problem. As far as we know L-𝒮
ℋ
ℐ
𝒩 is the first presentation of a reasoning algorithm for such complex fuzzy DL languages over finite residuated lattices. Besides, this is the first time that optimized techniques were used to tableau reasoning for completion forest in DLs augmented by De Morgan lattices. This enabled us to treat the case of general concept inclusions instead of the simpler acyclic TBoxes.Of course, there remains plenty of work to do with the tableau algorithm ofL-𝒮
ℋ
ℐ
𝒩, such as to directly and efficiently handle general TBoxes and to deal with concrete domains. We intend to extendL-𝒮
ℋ
ℐ
𝒩 also for more description logics under more semantics. Besides, the presented dependency management allows for more informed backjumping, while also supporting the creation of precise cache unsatisfiability entries [29]. Among others, better heuristics are needed to guide the choices needed during tableau reasoning, and better use of cached information is expected to provide significant benefits. Additionally, like other related research areas such as Semantic Web, most DL reasoners are implemented in Java for usability by many applications, so the Java implementation of the optimized algorithm will be carried out in the future work.



---

*Source: 702326-2014-04-07.xml*