# nonexpansive_fuzzy_alc__1b7328f6.pdf

Non-expansive Fuzzy ALC

Stefan Gebhart , Lutz Schr oder and Paul Wild Friedrich-Alexander-Universit at Erlangen-N urnberg {stefan.gebhart, lutz.schroeder, paul.wild}@fau.de

Fuzzy description logics serve the representation of vague knowledge, typically letting concepts take truth degrees in the unit interval. Expressiveness, logical properties, and complexity vary strongly with the choice of propositional base. The Łukasiewicz propositional base is generally perceived to have preferable logical properties but often entails high complexity or even undecidability. Contrastingly, the less expressive Zadeh propositional base comes with low complexity but entails essentially no change in logical behaviour compared to the classical case. To strike a balance between these poles, we propose non-expansive fuzzy ALC, in which the Zadeh base is extended with Łukasiewicz connectives where one side is restricted to be a rational constant, that is, with constant shift operators. This allows, for instance, modelling dampened inheritance of properties along roles. We present an unlabelled tableau method for non-expansive fuzzy ALC, which allows reasoning over general TBoxes in EXPTIME like in two-valued 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 Rich has Child. (Rich 0.1)

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

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

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. 2. Let (NC, NR) be a signature. Then concepts C, D, . . . of non-expansive fuzzy ALC are generated by the grammar

C, D ::= p | c | C | C c | C D | R.C

where c [0, 1] is a constant, p NC is an atomic concept and R NR is a role name. 3. A (fuzzy) interpretation I consists of a set I = of individuals , a map p I : I [0, 1] for every atomic concept p NC, and a map RI : I I [0, 1] for every role name R NR. 4. 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

c I(x) = c ( D)I(x) = 1 DI(x)

(C c)I(x) = max(CI(x) c, 0)

(C D)I(x) = min(CI(x), DI(x))

( R.C)I(x) = sup y I{min(RI(x, y), CI(y))}.

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

b | = log2 a + log2 b | C| = |C| + 1 |C c| = |C| + |c| + 1 |C D| = |C| + |D| + 1 | R.C| = |C| + 1.

7. 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.

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

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 CI : 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:

x I : CI(x) DI(x)

2. 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 CI(x) c. We then also say that C c is satisfied in x. 3. 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. 4. 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 CI(x) c. 5. We say a sequent Γ is T -valid if every concept assertion of Γ is T -valid. 6. 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 CI(x) + DI(x)) p. However this is clearly equivalent to min(1, DI(x) + (1 p)) CI(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:

<, if = > , if = >, if = < , if =

, if = > >, if = , if = < <, if =

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:

A R. (A 0.2) A 0.2 B 0.3 B ( R. B) 0.2

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.

2. 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 Is Friends With (abbreviated as IFW) and as atomic concepts we take opinions people can hold to some

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

degree. Our TBox could then look like this:

IFW.Football Fan Football Fan IFW.( Football Fan 0.4) Football Fan 0.2 IFW.(Sports Fan 0.3) Sports Fan 0.2 Football Fan Sports Fan Football Fan 0.3 IFW.(Football Fan 0.2)

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.( Football Fan) 0.4) Sports Fan 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 Cited By and Collaborated With (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:

Cited By.Influence Influence 0.2 CW.(Influence 0.4) Influence CW.Influence Influence Influence Cited By.(Influence 0.3)

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) ( Cited By.(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 ϵ = 1

2 min(Z \ {0}) and Z = Z {z + ϵ | z Z \ {1}}. The concept assertion associated to T and Γ is T 1 where T = (dn i=1 F 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.

Definition 3.3. For {<, } and {>, }, we put

( , ):= <, if ( , ) = ( , ) , otherwise.

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).

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

Tableau Rules

(Ax 1) S,p c

(if c 1, p NC) (Ax 0) S,p c

(if c 0, p NC) (Ax c) S,c d

(Ax p) S,p c,p d

(if c ( , ) d, p NC) ( ) S,C D c S,C c,D c ( ) S,C D c S,C c S,D c

( ) S, C c S,C 1 c ( ) S,C c d S,C d+c,d 0 ( ) S,C c d

S,C d+c (if d 0)

( R) S,{ R.Dj jdj|1 j n}, R.C c {Dj jdj|dj ( j , )c,j {1,...,n}},C c,T 1 (if c 0 and S does not contain any R.D d)

Table 1: Tableau Calculus for T 1 and Γ

2. 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. 3. 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. 4. 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 r G V G; and for each node v V G a label LG(v), which is a set of concept assertions or . 2. 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 r G 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

r G V Gc; for v V Gc, v AG, we have w V Gc for all (v, w) EG; and for v V Gc, v OG, we have w V Gc for some (v, w) EG.

2. A marking is consistent if it does not contain a node with label .

3. 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;

2. p c Γ, p d Γ for some p NC, c ( , ) d;

3. 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.

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

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. Put I := AG V Gc.

2. 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.

3. 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 CI(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 r Gc and ending at τ.

Next, we prove soundness:

Theorem 3.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 r G 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 r G 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 r G / 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 r G / 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

p I (x) := 1 if x p I

0 otherwise

RI (x, y) := 1 if (x, y) RI

0 otherwise.

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 p I

iff p I (x) > 0.5 and (x, y) RI iff RI (x, y) > 0.5. One can then prove CI (x) > 0.5 iff x CI 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

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

Algorithm 1: checking satisfiability in non-expansive fuzzy ALC

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 r G Unsat then

11 return false;

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 nonlabel 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 fea-

tures, 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].

[Baader and Pe naloza, 2011] Franz Baader and Rafael Pe naloza. On the undecidability of fuzzy description logics with GCIs and product t-norm. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, Fro Co S 2011, volume 6989 of LNCS, pages 55 70. Springer, 2011.

[Baader et al., 2015] Franz Baader, Stefan Borgwardt, and Rafael Pe naloza. On the decidability status of fuzzy ALC with general concept inclusions. J. Philos. Log., 44(2):117 146, Apr 2015.

[Baader et al., 2017] Franz Baader, Stefan Borgwardt, and Rafael Pe naloza. Decidability and complexity of fuzzy description logics. KI - K unstliche Intelligenz, 31(1):85 90, Mar 2017.

[Bobillo and Straccia, 2011] Fernando Bobillo and Umberto Straccia. Reasoning with the finitely many-valued Łukasiewicz fuzzy description logic SROIQ. Inf. Sci., 181(4):758 778, 2011.

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

[Bonatti and Tettamanzi, 2003] Piero A. Bonatti and Andrea Tettamanzi. Some complexity results on fuzzy description logics. In Vito Di Ges u, Francesco Masulli, and Alfredo Petrosino, editors, Fuzzy Logic and Applications, WILF 2003, volume 2955 of LNCS, pages 19 24. Springer, 2003.

[Borgwardt and Pe naloza, 2016] Stefan Borgwardt and Rafael Pe naloza. Reasoning in expressive G odel description logics. In Maurizio Lenzerini and Rafael Pe naloza, editors, Description Logics, DL 2016, volume 1577 of CEUR Workshop Proceedings. CEUR-WS.org, 2016.

[Borgwardt and Pe naloza, 2017] Stefan Borgwardt and Rafael Pe naloza. Fuzzy description logics - A survey. In Seraf ın Moral, Olivier Pivert, Daniel S anchez, and Nicol as Mar ın, editors, Scalable Uncertainty Management, SUM 2017, volume 10564 of LNCS, pages 31 45. Springer, 2017.

[Borgwardt et al., 2015] Stefan Borgwardt, Felix Distel, and Rafael Pe naloza. The limits of decidability in fuzzy description logics with general concept inclusions. Artif. Intell., 218:23 55, 2015.

[Bou et al., 2011] F elix Bou, Marco Cerami, and Francesc Esteva. Finite-valued lukasiewicz modal logic is pspacecomplete. In Toby Walsh, editor, International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 774 779. IJCAI/AAAI, 2011.

[Caicedo et al., 2017] Xavier Caicedo, George Metcalfe, Ricardo Oscar Rodr ıguez, and Jonas Rogger. Decidability of order-based modal logics. J. Comput. Syst. Sci., 88:53 74, 2017.

[Cerami and Esteva, 2022] Marco Cerami and Francesc Esteva. On decidability of concept satisfiability in description logic with product semantics. Fuzzy Sets Syst., 445:1 21, 2022.

[Flaminio et al., 2013] Tommaso Flaminio, Llu ıs Godo, and Enrico Marchioni. Logics for belief functions on mvalgebras. Int. J. Approx. Reason., 54(4):491 512, 2013.

[Gebhart et al., 2025] Stefan Gebhart, Lutz Schr oder, and Paul Wild. Non-expansive fuzzy ALC. Co RR, 2025.

[Gor e and Nguyen, 2007] Rajeev Gor e and Linh Anh Nguyen. EXPTIME tableaux for ALC using sound global caching. In Diego Calvanese, Enrico Franconi, Volker Haarslev, Domenico Lembo, Boris Motik, Anni-Yasmin Turhan, and Sergio Tessaris, editors, Description Logics, DL 2007, volume 250 of CEUR Workshop Proceedings, 2007.

[Gor e and Nguyen, 2013] Rajeev Gor e and Linh Anh Nguyen. Exptime tableaux for using sound global caching. J. Automated Reasoning, 50(4):355 381, 2013.

[Gor e et al., 2010a] Rajeev Gor e, Clemens Kupke, and Dirk Pattinson. Optimal tableau algorithms for coalgebraic logics. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 114 128, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.

[Gor e et al., 2010b] Rajeev Gor e, Clemens Kupke, Dirk Pattinson, and Lutz Schr oder. Global caching for coalgebraic description logics. In J urgen Giesl and Reiner H ahnle, editors, Automated Reasoning, pages 46 60, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. [H ajek, 2005] Petr H ajek. Making fuzzy description logic more general. Fuzzy Sets Sys., 154:1 15, 2005. [Hermes, 2023] Philipp Hermes. Tableau calculi for nonexpansive fuzzy modal logics, 2023. Bachelor s thesis, Friedrich-Alexander-Universit at Erlangen-N urnberg. [H ajek, 1995] Petr H ajek. Fuzzy logic and arithmetical hierarchy. Fuzzy Sets Sys., 73(3):359 363, 1995. [Keller and Heymans, 2009] Uwe Keller and Stijn Heymans. Fuzzy description logic reasoning using a fixpoint algorithm. In Logical Foundations of Computer Science, LFCS 2009, volume 5407 of LNCS, pages 265 279. Springer, 2009. [Kulacka et al., 2013] Agnieszka Kulacka, Dirk Pattinson, and Lutz Schr oder. Syntactic labelled tableaux for lukasiewicz fuzzy ALC. In Francesca Rossi, editor, International Joint Conference on Artificial Intelligence, IJCAI 2013, pages 962 968. IJCAI/AAAI, 2013. [Kundu and Chen, 1998] Sukhamay Kundu and Jianhua Chen. Fuzzy logic or Łukasiewicz logic: A clarification. Fuzzy Sets Sys., 95(3):369 379, 1998. [Ladner, 1977] R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6, 1977. [Lukasiewicz and Straccia, 2008] Thomas Lukasiewicz and Umberto Straccia. Managing uncertainty and vagueness in description logics for the semantic web. J. Web Semant., 6(4):291 308, 2008. [Pavelka, 1979] J. Pavelka. On fuzzy logic l, ii, iii. Z. Math. Loqik, 45:45 52, 119 134, 447 464, 1979. [Schild, 1994] Klaus Schild. Terminological cycles and the propositional µ-calculus. In Principles of Knowledge Representation and Reasoning, pages 509 520. Elsevier, 1994. [Stoilos and Stamou, 2014] Giorgos Stoilos and Giorgos B. Stamou. Reasoning with fuzzy extensions of OWL and OWL 2. Knowl. Inf. Syst., 40(1):205 242, 2014. [Stoilos et al., 2006] Giorgos Stoilos, Umberto Straccia, Giorgos B. Stamou, and Jeff Z. Pan. General concept inclusions in fuzzy description logics. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors, European Conference on Artificial Intelligence, ECAI 2006, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 457 461. IOS Press, 2006. [Stoilos et al., 2007] Giorgos Stoilos, Giorgos Stamou, Jeff Pan, Vassilis Tzouvaras, and Ian Horrocks. Reasoning with very expressive fuzzy description logics. JAIR, 30:273 320, 2007. [Straccia, 2001] Umberto Straccia. Reasoning within fuzzy description logics. J. Artif. Intell. Res., 14:137 166, 2001.

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)

[Straccia, 2005] Umberto Straccia. Description logics with fuzzy concrete domains. In Uncertainty in Artificial Intelligence, UAI 2005, pages 559 567. AUAI Press, 2005. [van Breugel and Worrell, 2005] F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115 142, 2005. [Wild and Schr oder, 2021] Paul Wild and Lutz Schr oder. A quantified coalgebraic van benthem theorem. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, FOSSACS 2021, volume 12650 of LNCS, pages 551 571. Springer, 2021. [Wild et al., 2018] Paul Wild, Lutz Schr oder, Dirk Pattinson, and Barbara K onig. A van Benthem theorem for fuzzy modal logic. In Anuj Dawar and Erich Gr adel, editors, Logic in Computer Science, LICS 2018, pages 909 918. ACM, 2018.

Proceedings of the Thirty-Fourth International Joint Conference on Artiﬁcial Intelligence (IJCAI-25)