Non-expansive Fuzzy ALC
Stefan Gebhart, Lutz Schröder, Paul Wild
TL;DR
The paper addresses the trade-off between expressiveness and decidability in fuzzy description logics by introducing non-expansive fuzzy $\mathcal{ALC}$, an extension of the Zadeh base with constant shift operators $(-)\ominus c$ and $(-)\oplus c$ that enables damped inheritance along roles while preserving non-expansiveness. It provides an unlabelled tableau calculus with global caching for reasoning over general TBoxes, showing ExpTime-completeness for $\mathcal{T}$-satisfiability and enabling termination without fully expanding the tableau. By reducing $\mathcal{T}$-satisfiability to a single concept assertion $T \ge 1$ and leveraging a finite label space, the work achieves a practical, scalable decision procedure that remains in the same complexity class as classical $\mathcal{ALC}$. The framework increases expressivity relative to Zadeh fuzzy $\mathcal{ALC}$ while avoiding the undecidability seen in full Łukasiewicz fuzzy $\mathcal{ALC}$, with potential applications in modeling nuanced hierarchical inheritance and behavioural distance. Future work aims to extend the calculus to transitive roles, inverses, and nominals, integrating these features into the non-expansive tableaux paradigm.
Abstract
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 Lukasiewicz 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 Lukasiewicz 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.