Non-expansive Fuzzy ALC

1 Introduction

Fuzzy description logics (fuzzy DLs; see [Lukasiewicz and Straccia, 2008] for an overview) model vague knowledge by replacing the classical two-valued truth set with more finegrained alternatives, most commonly with the unit interval. (Other choices are possible, such as quantales, e.g. [Wild and Schr¨oder, 2021], or MV-algebras, e,g. [Flaminio et al., 2013]). Both concepts and roles may be 'fuzzified' in this sense, allowing for the appropriate representation of concepts such as 'tall person' or 'fast car', and of roles such as 'likes' or 'supports'. In the design of fuzzy DLs, an important factor is the choice of propositional base, that is, of the set of propositional connectives and their interpretation over the given truth set. Over the unit interval [0, 1], standard options include Zadeh, Łukasiewicz, G¨odel, and product logic [Lukasiewicz and Straccia, 2008], with the Zadeh and the Łukasiewicz base having received a comparatively large share of the overall attention [Bobillo and Straccia, 2011; Borgwardt and Pe˜naloza, 2017; Bou et al., 2011;

H´ajek, 2005; Kulacka et al., 2013; Stoilos et al., 2007; Straccia, 2005].

In the Zadeh base, conjunction and disjunction are just interpreted as minimum and maximum, respectively. This has intuitive appeal but closer analysis has shown that under this interpretation, the logic in fact remains very close to its twovalued correspondent. For instance, the problem of deciding whether an ALC concept is satisfiable with truth degree at least p in Zadeh semantics is equivalent to satisfiability in two-valued semantics if p ≥ 0.5, and largely trivial, in particular decidable in linear time, if p < 0.5 [Bonatti and Tettamanzi, 2003; Keller and Heymans, 2009; Straccia, 2001]. The Łukasiewicz base, which uses the additive structure of [0, 1] to interpret disjunction and conjunction, does not suffer from such deficiencies, and is generally perceived to have favourable logical properties (in fact, it is determined up to isomorphism by a set of desirable properties including residuation and axiomatizability [Kundu and Chen, 1998]). On the other hand, the Łukasiewicz base comes with an increase in computational hardness. Indeed, the best known upper bound for concept satisfiability in Łukasiewicz fuzzy ALC is NEXPTIME [Kulacka et al., 2013; Straccia, 2005] (compared to PSPACE for two-valued ALC [Ladner, 1977]), and reasoning over general TBoxes in Łukasiewicz fuzzy ALC is even undecidable [Baader and Pe˜naloza, 2011].

In the present work, we aim to strike a balance between these poles, proposing non-expansive fuzzy ALC as a logic that offers more expressive power than Zadeh fuzzy ALC but retains the same complexity as two-valued ALC. As the propositional base, we use an extension of the Zadeh base where we allow rational truth constants and Łukasiewicz connectives with one argument restricted to be a truth constant; phrased more simply, the latter effectively just means that we include constant shift operators (-)⊕c where ⊕ denotes truncated addition and c is a rational constant (one can then also express truncated subtraction (-)⊖c). For instance, the TBox axiom

asserts (debatably, of course) that children of rich people tend to be even richer than their parents. This propositional base has been widely used in modal logics that characterize behavioural distances, for instance, on probabilistic [van Breugel and Worrell, 2005] or fuzzy [Wild et al., 2018] systems, and in particular does ensure non-expansiveness of the logic w.r.t. behavioural distance; hence our choice of nomenclature.

Our main technical result on non-expansive fuzzy ALC is decidability of the main reasoning problems in the same complexity as for two-valued ALC; most notably, threshold satisfiability over general TBoxes is (only) EXPTIME-complete, in sharp contrast with the undecidability encountered for full Łukasiewicz fuzzy ALC, and in spite of the fact that the semantics of general concept inclusions is pointwise inequality and thus corresponds to validity of Łukasiewicz implication. We base this result on an unlabelled tableau calculus. We construct tableaux using an algorithm that follows the global caching principle [Gor´e and Nguyen, 2007] and thus can terminate before the tableau has been fully expanded, offering a perspective for practical scalability.

Proofs are sometimes omitted or only sketched; full proofs can be found in the full version [Gebhart et al., 2025].

Further related work The idea of using explicit (rational) truth constants comes from (rational) Pavelka logic [H´ajek, 1995; Pavelka, 1979] For finite-valued Łukasiewicz fuzzy ALC, the threshold satisfiability problem is PSPACEcomplete [Bou et al., 2011]. Reasoning in fuzzy ALC with product semantics has also been shown to be computationally hard: Validity over the empty TBox is decidable but only a lower bound is known [Cerami and Esteva, 2022] and undecidable under general concept inclusions [Baader and Pe˜naloza, 2011]. For a more general classification of the decidability of description logics under TBoxes depending on the propositional base, see, for example, [Baader et al., 2017]. Under the G¨odel propositional base, threshold satisfiability (without a TBox) remains in PSPACE [Caicedo et al., 2017], and decidability is retained even for expressive fuzzy description logics [Borgwardt and Pe˜naloza, 2016]. Reasoning in Zadeh fuzzy ALC becomes more involved in presence of ABoxes with explicit thresholds. An existing tableau algorithm for this case [Stoilos et al., 2006] (which does cover general concept inclusions in the sense indicated above) is quite different from ours; in particular, it updates labels of tableau nodes after their creation, and relies on almost all relevant threshold values being explicitly mentioned in the ABox. Reasoning methods for Zadeh fuzzy DLs have been extended to highly expressive DLs [Stoilos et al., 2007; Stoilos and Stamou, 2014]. In the absence of TBoxes, there is a tableau algorithm for fuzzy ALC for any continuous t-norm [Baader et al., 2015]. The tableaux algorithm for Łukasiewicz fuzzy ALC necessarily applies only the case without TBoxes, and works in a different way from ours, in particular is labelled. A preliminary variant of the tableau calculus for non-expansive fuzzy ALC without TBoxes has featured in an undergraduate thesis supervised by the second author [Hermes, 2023].

2 Non-Expansive Fuzzy ALC

We proceed to introduce the fuzzy DL non-expansive fuzzy ALC. As indicated earlier, it follows the Zadeh interpretation of conjunction ⊓ and disjunction ⊔ as minimum and maximum, but includes constant shifts (-) ⊖ c and (-) ⊕ c for rational constants as additional propositional operators. Formal definitions are as follows.

Convention 2.1. Throughout, let ◁ ∈ {<,≤}, ▷ ∈ {>,≥} and ▷◁ ∈ {<,≤,>,≥}. Whenever we talk about constants we refer to rational numbers, usually in the unit interval. We encode a constant by taking the binary representation of the numerator and denominator of its representation as an irreducible fraction.

Definition 2.2. 1. A signature of a description language consists of a set NC of atomic concepts and a set NR := {Ri | i ∈ I} of role names for some index set I.

1. Let (NC,NR) be a signature. Then concepts C,D, . . . of non-expansive fuzzy ALC are generated by the grammar

where c ∈ [0, 1] is a constant, p ∈ NC is an atomic concept and R ∈ NR is a role name.

1. A (fuzzy) interpretation I consists of a set ∆I ̸= ∅ of individuals , a map pI : ∆I → [0, 1] for every atomic concept p ∈ NC, and a map RI : ∆I ×∆I → [0, 1] for every role name R ∈ NR.
2. Let I be an interpretation and x ∈ ∆I an individual. Then we define the valuation of concepts in x with respect to the interpretation I recursively by

1. A concept assertion is an inequality of the form C ▷◁ c. A (tableau) sequent is a finite set of concept assertions.
2. We define the (syntactic) size |C| of a concept C inductively by

1. The (syntactic) size of a concept assertion C ▷◁ c is |C| + |c|, and that of a sequent is the sum of the syntactic sizes of its elements.

As usual, we define C ⊔ D = ¬(¬C ⊓ ¬D) and ∀R.C = ¬∃R.¬C. We also define C⊕c = ¬((¬C)⊖c). Furthermore we call ∃R.C ▷ c an existential restriction and ∃R.C ◁ c a universal restriction.

Remark 2.3. The concept language of non-expansive fuzzy ALC agrees essentially with a fuzzy modal logic featuring in a quantitative modal characterization theorem [Wild et al., 2018]. We could also equivalently define non-expansive fuzzy ALC as Łukasiewicz ALC where we we keep the weak connectives, i.e. the Zadeh connectives, and require that at least one of the arguments of the Łukasiewicz connectives must be a constant. Recall here that in Łukasiewicz semantics, we have, e.g., strong disjunction ⊕ interpreted as addition, so our concepts C ⊕c are effectively strong disjunctions with constants.

Remark 2.4. For most reasoning problems in fuzzy ALC with a plain Zadeh base, it has been shown not only that they have the same complexity as the classical counterpart ALC but also that logical consequence remains mostly the same [Bonatti and Tettamanzi, 2003; Keller and Heymans, 2009; Stoilos et al., 2007; Straccia, 2001]. It has also been noted that non-implication of falsity is not a useful notion of knowledge base consistency in this setting, and is in deterministic linear time while threshold satisfiability is EXPTIMEcomplete [Bonatti and Tettamanzi, 2003]. Non-expansive fuzzy ALC employs a more expressive concept language than classical ALC and as such is not formally subject to such phenomena; we aim to illustrate in Example 2.10 that there is also a practical gain in expressiveness over Zadeh fuzzy ALC, in particular in connection with general TBoxes.

Remark 2.5. In analogy to two-valued notions of bisimilarity, one can give a natural fixpoint definition of behavioural distance between individuals in interpretations I. Under this distance, the maps C I : ∆I → [0, 1] become nonexpansive (and in fact even characterize behavioural distance), a property that fails in Łukasiewicz semantics [Wild et al., 2018]. This motivates the nomenclature 'non-expansive fuzzy ALC'.

Definition 2.6. 1. A TBox T is a set of general concept inclusions or GCIs for short, which are of the form C ⊑ D. We say that an interpretation I satisfies the TBox T if for every GCI C ⊑ D we have:

1. We say that a concept assertion C ▷◁ c is T -satisfiable if there exists an interpretation that satisfies T and that has an individual x ∈ ∆I such that C I (x) ▷◁ c. We then also say that C ▷◁ c is satisfied in x.
2. We say that a sequent Γ is T -satisfiable if there exists an interpretation that satisfies T and that has an individual x such that every concept assertion of Γ is satisfied in x. We then also say that Γ is satisfied in x.
3. We say a concept assertion C ▷◁ c is T -valid if for every interpretation I that satisfies T and all individuals x ∈ ∆I we have C I (x) ▷◁ c.
4. We say a sequent Γ is T -valid if every concept assertion of Γ is T -valid.
5. We define the (syntactic) size of a GCI by the sum of the syntactic sizes of its concepts and the syntactic size of a TBox as the sum of the syntactic sizes of its elements.

Remark 2.7. There is also a notion of fuzzy GCIs of the form C ⊑ D ≥ p [Borgwardt et al., 2015]. In Łukasiewicz semantics, this GCI is satisfied by an interpretation I iff for all x ∈ ∆I we have (C =⇒ D)I (x) = min(1, 1 - C I (x) +DI (x)) ≥ p. However this is clearly equivalent to min(1, DI (x) + (1 - p)) ≥ C I (x), which would be the GCI C ⊑ (D ⊕ (1 - p)) in non-expansive fuzzy ALC. Thus we can restrict ourselves to just handling regular GCIs.

In order to ease working with varying comparison operators, we define the following operators to turn inequalities around and to turn strict inequalities into weak inequalities and vice versa:

Definition 2.8. Let ▷◁ ∈ {<,≤,>,≥}. We define:

Clearly, C ▷◁ c is T -valid iff C ▷◁◦ c is not T -satisfiable. So in order to prove the T -validity of C ≥ c or C ≤ c, we have to check C < c or C > c for T -satisfiability respectively.

Remark 2.9. As noted already for the case of Zadeh ALC [Stoilos et al., 2006], TBoxes cause substantial additional difficulties in reasoning algorithms. One reason for this additional difficulty is that in Zadeh-type logics, TBoxes cannot be internalized as valid implications: The concept ¬C ⊔D is satisfied by all individuals in an interpretation iff whenever C has value > 0, then D has value 1, which is not equivalent to satisfaction of the GCI C ⊑ D. Contrastingly, in Łukasiwicz semantics, the strong disjunction (cf. Remark 2.3) ¬C ⊕D holds in every individual of an interpretation iff the interpretation satisfies the GCI C ⊑ D; that is, we can regard TBoxes as demanding satisfaction of top-level Łukasiewicz implications.

Example 2.10. 1. To better illustrate and understand the semantics of non-expansive fuzzy ALC, we begin with the following example:

The ⊖ on the right hand side of the GCI A ⊖ 0.2 ⊑ B ⊖ 0.3 makes it so B has to be bigger than the left hand side by at least 0.3 and on the other hand the ⊖ on the left hand side decreases the value of A which means that the right hand side has to be at most 0.2 smaller than A. Combined, this tells us that the value of B is bigger than that of A by at least 0.1. So we could reformulate this as just A ⊑ B ⊖ 0.1. The GCI A ⊑ ∀R. (A ⊖ 0.2) tells us that each R-successor either has a successorship degree smaller than or equal to 1 minus the value of A or the value of A in this successor is bigger than the value of A at this current individual by at least 0.2. The GCI B ⊑ (∀R. B) ⊖ 0.2 on the other hand tells us that each R-successor either has a successorship degree smaller than or equal to 0.8 minus the value of B or the value of B in this successor is bigger than the value of B of the current individual by at least 0.2. An example of an inference would then be that (¬(A⊖0.5))⊔((∀R.B)⊖0.2) ≥ 0.8 is T -valid; this makes use of the GCIs A ⊖ 0.2 ⊑ B ⊖ 0.3 (or rewritten as A⊕0.1 ⊑ B) and B ⊑ (∀R.B)⊖0.2 and states that either A is smaller than 0.7 or B is equal to 1 in all R-successors with non-zero successorship degree.

1. We model social influences on opinions and beliefs (as a disclaimer, we note that neither this example nor the next one are meant as realistic formalizations of the respective domains): In this model, individuals are people, the single role is the interaction IsFriendsWith (abbreviated as IFW) and as atomic concepts we take opinions people can hold to some

degree. Our TBox could then look like this:

We can then reason about how much people like sports or football based on who they interact with and to what degree. An inference we could then make (using the first and fourth GCIs) is that (∃IFW.(¬FootballFan) ⊕ 0.4) ⊔ SportsFan ≥ 0.7 is T -valid, which means that either you have a close friend that is not really interested in football or you are a very big sports fan.

3. We model the influence of scientists: As individuals we have scientists, as roles we have citation and collaboration relations CitedBy and CollaboratedWith (or CW for short) Influence of a scientist. Here the fuzziness of the roles represents the frequency of collaborations or citations. Our TBox could then look like this:

We can then reason about how much citations and collaborations affect influence. For instance, from the above we may infer (using the second and fourth GCIs) that (∀CW.(¬Influence ⊕ 0.4) ⊕ 0.6) ⊔ (∃CitedBy.(Influence ⊕ 0.3)) ≥ 0.8 is T -valid, which means the influence of collaborators of a scientist has an impact on the citations of the scientist.

3 Tableaux Calculus for TBoxes

Having introduced our language and the concept of T - satisfiability, we now construct an unlabelled tableau calculus and prove EXPTIME-completeness of determining if a sequent is T -satisfiable. We start by finding a more easily computable notion of T -satisfiability: Let A ⊑ B be a GCI from a TBox T and Γ be a sequent. Then for any interpretation I, we have that A ⊑ B is satisfied in I iff for all individuals x, there exists a constant c such that AI (x) ≤ c and BI (x) ≥ c. The latter formulas can be rewritten as ((¬A⊕c)⊓(B⊕(1-c)))I (x) ≥ 1. Checking this formula for all possible c would not yield a terminating algorithm, however as it turns out it suffices to check this for finitely many constants:

Definition 3.1. Let T = {Ci ⊑ Di | i = 1, . . . , n} be a TBox and Γ be a sequent. Let Z be the intersection of the unit interval and the additive subgroup of the rationals generated by 1 and the constants appearing in Γ and T . Put ϵ = 12 min(Z \ {0}) and Z ′ = Z ∪ {z + ϵ | z ∈ Z \ {1}}. The concept assertion associated to T and Γ is T ≥ 1 where T = (�ni=1 ⊔z∈Z′ (¬Ci ⊕ z) ⊓ (Di ⊕ (1 - z))).

Lemma 3.2. Let T be a TBox and let Γ be a sequent. Then Γ is satisfiable under T iff there exists an interpretation where

Γ is satisfied by some individual and each individual satisfies T ≥ 1 where T is the concept assertion associated to T and Γ.

Proof sketch. 'If' is trivial by the above argumentation. 'Only if' can be shown by transforming an arbitrary interpretation satisfying Γ under T into one where all atomic concepts in all individuals and all roles have values in Z ′ by either keeping them as is if they already were in Z ′ or taking the closest value in Z ′ \ Z otherwise. One can then show by induction that concept assertions containing only values of Z on their right hand side and subconcepts of Γ and T on their left hand side cannot distinguish between these interpretations and that T ≥ 1 is satisfied in every individual.

Remark 3.4. The ◀(◁,▷) operator is used to obtain a nonstrict inequality if at least one of the inputs is a strictly greater or smaller than. This will be useful when determining if a pair of inequalities is solvable or not; explicitly, if we have p ≤ c and p ≥ d we cannot find a valid value for p if c < d and in all other cases p ◁ c and p ▷ d we cannot find a valid value for p if c ≤ d.

If T ≥ 1 is the associated concept assertion for the TBox T and a sequent Γ, this gives us the tableau calculus of Table 1. The axioms (Ax 1), (Ax 0) and (Ax p) assert that the truth value of an atomic concept cannot be larger than 1, smaller than 0 or in an empty interval. The axiom (Ax c) asserts that c ◁ d is satisfiable only if this constraint actually holds for the constants c, d. The (⊓ ▷), (⊓ ◁) and (¬ ▷◁) rules are the usual fuzzy propositional rules. The (⊖ ◁) rule asserts that we can add c to both sides of a concept assertion without affecting satisfiability, as long as the assertion is not already unsatisfiable by the fact that C ⊖ c would have to be smaller than 0. The (⊖ ▷) rule also asserts that we can add c to both sides of the concept assertion. However, this time we have to be careful not to apply this to concept assertions that are always satisfied, i.e. assertions saying that the left hand side should be greater than or equal to 0. We have to avoid this case, as otherwise these trivial assertions could be transformed into unsatisfiable ones, e.g. the satisfiable concept assertion 0 ⊖ 1 ≥ 0 would be transformed into 0 ≥ 1, which is not satisfiable. The rule (∃R) first takes all universal restrictions of some role R ∈ NR and one existential restriction ∃R.C ▷ c. We then filter out all universal restrictions ∃R.Dj ◁ dj that can be trivially satisfied by finding a value e for the role R such that e ▷ c but e ◁ dj. This means we only have universal restrictions ∃R.Dj ◁ dj left with dj ◀(◁j,▷) c. We then take these universal restrictions and the existential restriction, remove their ∃R. part, and add T ≥ 1, while dropping the remaining context S, to see if we can create an individual satisfying these constraints.

Definition 3.5. 1. The propositional rules of the calculus are all rules except (∃R).

Tableau Rules

Table 1: Tableau Calculus for T ≥ 1 and Γ

1. As usual, for each rule we take all its possible instances for concrete constants, concepts, and sets of concept assertions, and say the the rule is applicable to a sequent if the sequent matches the premise of an instance of the rule, satisfying possible side conditions of the rule.
2. When we say we apply a rule to a sequent, we mean that we take the conclusions of a rule instance whose premise matches the sequent.
3. A sequent is saturated if no propositional rules can be applied to it.

The idea of a global caching algorithm to construct a tableau is to cache all the labels of its nodes, and whenever a new node with an already encountered label would be created, we instead create an edge to the already existing node with that label, thus obtaining a directed graph, possibly with cycles. As we will see later, this will ensure the algorithm terminates in exponentially many steps.

Definition 3.6. 1. A tableau graph G consists of

• a directed graph (V G,EG) consisting of a set V G of nodes and a set EG ⊆ V G × V G of edges;
• a root node rG ∈ V G;
• and for each node v ∈ V G a label LG(v), which is a set of concept assertions or ⊥.
• A node v ∈ V G in a tableau graph G is an AND-node if its label LG(v) is saturated, and otherwise an OR-node. We denote by AG the set of AND-nodes and by OG the set of OR-nodes.

Definition 3.7. Let G be a tableau graph and v ∈ V G be a node.

1. A propositional rule has been applied to v in G if the labels of the child nodes of v are exactly the conclusions of an application of an instance of this rule to the label of v.
2. The rule (∃R) has been applied to v in G if the labels of the child nodes of v are exactly the conclusions of all possible applications of this rule (maybe none) to the label of v.
3. We call G a tableau for a sequent Γ and T ≥ 1 if the root node rG has the label LG(r) = Γ ∪ {T ≥ 1}, a propositional rule has been applied to all OR-nodes and the rule (∃R) has been applied to all AND-nodes.

The next goal is to prove soundness and completeness of this tableau calculus and then termination and its complexity bound.

Definition 3.8. Let G be a tableau for Γ and T ≥ 1.

1. A marking Gc := (V Gc ,EGc ) of G is a full subgraph of (V G, EG) where
2. rG ∈ V Gc ;
3. for v ∈ V Gc , v ∈ AG, we have w ∈ V Gc for all (v,w) ∈ EG; and
4. for v ∈ V Gc , v ∈ OG, we have w ∈ V Gc for some (v, w) ∈ EG.
5. A marking is consistent if it does not contain a node with label ⊥.
6. We call G open if there exists a consistent marking, and closed otherwise.

As we will see later, a consistent marking of a tableau is a postfixpoint of a functional. We now show that an open tableau for Γ and T ≥ 1 can be used to construct an interpretation that satisfies T and where some individual satisfies Γ. We construct such an interpretation by first considering Gc-saturation paths:

Definition 3.9. Let Gc be a marking of a tableau G and v0 ∈ V Gc . A Gc-saturation path from v0 is a finite sequence v0, v1, . . . , vn such that for all 0 ≤ i < n we have (vi, vi+1) ∈ EGc , {v0, . . . , vn-1} ⊆ OG, and vn ∈ AG.

Remark 3.10. The above definition implies that a node is an AND-node iff it has a Gc-saturation path of length 0. Furthermore, all nodes have a Gc-saturation path, as we would otherwise need to have some infinite path that only visits ORnodes. However, since all rules that can be applied to an ORnode decrease the syntactic size of concepts in the label, such a path cannot exist.

Definition 3.11. We call a sequent Γ clashing if at least one of the following holds:

1. p ▷ c ∈ Γ for some p ∈ NC, c ▷ 1 or p ◁ c ∈ Γ for some p ∈ NC, c ◁ 0;

1. c ◁ d ∈ Γ for some c ◁◦ d.

We now prove completeness of the tableau calculus by extracting an interpretation from a consistent marking:

Theorem 3.12. Let Γ be a sequent and T be a TBox with associated concept assertion T ≥ 1. If there exists an open tableau G for Γ and T ≥ 1, then Γ is T -satisfiable.

Proof sketch. We directly construct an interpretation I from a consistent marking Gc of the open tableau G by contracting the marking along Gc-saturation paths:

1. For every x ∈ ∆I , we put the value of atomic concepts as any value satisfying all the concept assertions in its corresponding label. We can do this since the label of an x ∈ V Gc can never be clashing.
2. We take for every x, y ∈ ∆I and role name R ∈ NR all the nodes along Gc-saturation paths starting at a child node of x and ending with y and by investigating their labels determine which node corresponds to which existential restriction in x. We then find a value for RI (x, y) that is large enough to satisfy all these existential restrictions but small enough such that all universal restrictions ∃R.D ◁ d are either satisfied by the value of the transition or D ◁ d is part of the label of a child node of x that has a Gc-saturation path ending with y.

By induction on C, we have C I (x) ▷◁ c for every x ∈ ∆I and every C ▷◁ c ∈ L(y) where y ∈ V Gc has a Gc-saturation path ending with x. Investigating maximal Gc-saturation paths and the tableau rules, we notice that T ≥ 1 must therefore always be satisfied in every x ∈ ∆I and that Γ is satisfied in some τ ∈ ∆I where there is a Gc-saturation path starting with the root node rGc and ending at τ.

Next, we prove soundness:

Theorem3.13. The above tableau calculus is sound. That is, if Γ is T -satisfiable, then every tableau for Γ and T ≥ 1 has a consistent marking, where T ≥ 1 is the concept assertion associated to T and Γ.

Proof sketch. Let G be a tableau for Γ and T ≥ 1. The label of the root rG can never be ⊥, and by checking the rules one by one, we see that they create some satisfiable conclusion or, in the case of the rule (∃R), only satisfiable conclusions from a satisfiable premise. This shows that for all nodes with satisfiable label, there is at least one child node for an OR-node that has a satisfiable label and all child nodes of AND-nodes have satisfiable labels. This means that if we start at the root node rG we always have at least one child with a satisfiable label or all children have a satisfiable label for AND-nodes, as is required to construct Gc.

The procedure and proof for the EXPTIME bound and termination is inspired by [Gor´e and Nguyen, 2013, Section 5]. It is a construction of the least fixpoint of a functional calculating unsatisfiable nodes. More specifially, we start with the node with label ⊥ as the only unsatisfiable node and then apply the functional to the set of unsatisfiable nodes until we reach a fixpoint. A node is then in this least fixpoint iff its label is T -unsatisfiable. This entails the following tight complexity bound:

Theorem 3.14. Algorithm 1 is an EXPTIME decision procedure for checking satisfiability of the concept assertions in Γ with regards to a TBox T .

Proof. Let Γ be a sequent, T ≥ 1 be the concept assertion associated to T and Γ and G a tableau for Γ and T ≥ 1.

1. By investigating the rules and the design of the concept assertion associated to T and Γ, one can show that there are at most 2O(n3 ) possible labels, where n is the syntactic size of Γ and T . More specifically, there are 2O(n) possible labels arising from applying rules to Γ, and for every GCI C ⊑ D in T , there are 2O(n2 ) possible labels that can be obtained from the corresponding conjunct ⊔z∈Z′ (¬C ⊕ z) ⊓ (D ⊕ (1 - z)) ≥ 1 in T . Since we have at most O(n) GCIs, we thus have 2O(n3 ) possible labels that arise from the TBox, and multiplying with the 2O(n) labels of Γ, we obtain at most 2O(n3 ) labels.
2. We now immediately have that Algorithm 1 terminates after at most 2O(n3 ) steps, since there are 2O(n3 ) nodes in G.
3. The condition rG /∈ Unsat is equivalent to the existence of a consistent marking for G, where Unsat is the set of unsatisfiable nodes as computed in Algorithm 1: For v ∈ AG we have v /∈ Unsat iff v does not have ⊥ as its label and for all nodes w ∈ V G with (v, w) ∈ EG we have w /∈ Unsat. Similarly for v ∈ OG we have v /∈ Unsat iff there exists a w ∈ V G with (v,w) ∈ EG and w /∈ Unsat. Taking all the nodes that are not in Unsat then by definition is a consistent marking iff rG /∈ Unsat. This also shows that a consistent marking is a postfixpoint of some functional, as Algorithm 1 calculates the least fixpoint for Unsat.

Theorem 3.15. Checking a sequent Γ for T -satisfiability is EXPTIME hard.

Proof. We reduce ALC satisfiability under a TBox, which is known to be EXPTIME hard [Schild, 1994], to T -satisfiability in non-expansive fuzzy ALC: Let Γ be a set of concepts and T be a TBox for ALC. Let Γ′ := {C ≥ 1 | C ∈ Γ} and T ′ := T . If Γ is satisfiable under T in ALC by some interpretation I, we obtain an interpretation I ′ for non-expansive fuzzy ALC by putting ∆I ′ :=∆I and

We then obviously have Γ′ is satisfiable under T ′ , as the evaluation of concepts is the same in this case as in non-fuzzy ALC. On the other hand, if Γ′ is satisfiable under T ′ by some interpretation I ′ in non-expansive fuzzy ALC, then we obtain an interpretation I for ALC by ∆I := ∆I ′ , x ∈ pI iff pI ′ (x) > 0.5 and (x, y) ∈ RI iff RI ′ (x, y) > 0.5. One can then prove C I ′ (x) > 0.5 iff x ∈ C I for all concepts C of regular ALC by induction. This then implies that Γ is satisfiable under T .

Remark 3.16. We can modify Algorithm 1 as in [Gor´e and Nguyen, 2013, Section 6] to decide and propagate satisfiability or unsatisfiability on the fly when constructing the tableau. After expanding a node, we immediately mark it as unsatisfiable if the node has label ⊥, if the node is an OR-node and all child nodes are marked as unsatisfiable or if the node is an

Input: a sequent Γ and an associated concept assertion T ≥ 1 for a TBox T and Γ Output: true if all concept assertions of Γ are satisfiable under the TBox T , false otherwise 1 construct a tableau G for Γ and T ≥ 1; 2 Unsat := ∅, Queue := ∅; 3 if ∃v⊥ ∈ V G : LG(v⊥) = {⊥} then 4 Unsat := {v⊥}, Queue := {v⊥}; 5 while Queue ̸= ∅ do 6 remove some w from Queue; 7 forall p ∈ V G : (p, w) ∈ EG do 8 if (p /∈ Unsat and p ∈ AG or p ∈ OG, ∀(p, q) ∈ EG : q ∈ Unsat) then 9 add p to Unsat and Queue; 10 if rG ∈ Unsat then 11 return false; 12 else 13 return true;

AND-node and at least one child node is marked as unsatisfiable. On the other hand we mark a node with a non-⊥ label as satisfiable if the node is an OR-node and at least one child node is marked as satisfiable or if the node is an AND-node and all child nodes are marked as satisfiable. If a node has been marked in this way, we propagate these results upward, i.e. we check these conditions again for all parent nodes and if their status changed we propagate again and so on. Thus we can stop expanding the tableau whenever we can decide if the root node is satisfiable or not instead of constructing the full tableau. One can also make propagation an optional step that can be applied instead of expanding the graph as seen in [Gor´e et al., 2010a] and [Gor´e et al., 2010b].

Remark 3.17. For readability, we have so far elided ABoxes from the technical development. As usual, a fuzzy ABox consists of concept assertion C(a) ▷◁ c and role assertions R(a, b) ▷◁ c, with the expected semantics, where a, b ∈ Ni for a dedicated name space Ni of individuals, which denote elements of the domain. The calculus is extended to handle ABoxes in a straightforward manner by just initializing the run of the tableau procedure with additional root nodes for the individuals mentioned in the ABox, containing all concepts asserted for the respective individual and connected by edges reflecting the role assertions. The complexity remains unaffected.

4 Conclusion

We have introduced the description logic non-expansive fuzzy ALC, which lies between the Łukasiewicz and Zadeh variants of fuzzy ALC, notably featuring constant shift operators. In particular in connection with general TBoxes, expressivity is markedly increased in comparison to Zadeh fuzzy ALC; nevertheless, we have shown that the complexity of reasoning remains EXPTIME, the same as for two-valued ALC in sharp contrast to the undecidability encountered in the case of Łukasiewicz fuzzy ALC [Baader and Pe˜naloza, 2011]. Future work will partly concern coverage of additional features, in particular transitive roles, inverses, and nominals. These have been integrated fairly smoothly into the less expressive Zadeh variant in earlier work [Stoilos et al., 2007; Stoilos and Stamou, 2014]; for non-expansive fuzzy ALC, the degree of adaptation to the tableau system required to accommodate these features remains to be explored.

Acknowledgements

This work is supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 531706730.

We extend recognition to Philipp Hermes, who developed a preliminary unlabelled tableau calculus for non-expansive fuzzy ALC without TBoxes within his bachelor thesis supervised by the second author [Hermes, 2023].