A tractable temporal description logic for reasoning fuzzy spatiotemporal knowledge

Fuzzy spatiotemporal reasoning is extensively used in various application fields such as Geographic Information Systems, Geospatial Artificial Intelligence, and Remote Sensing Systems. However, providing a tractable reasoning mechanism for fuzzy spatiotemporal knowledge is a challenging research problem. Description logics (DLs) are a type of logic-based tractable knowledge representation formalism that allow for describing knowledge structure of an application domain, but they are limited in their ability to express fuzzy spatiotemporal knowledge. To address this limitation, we propose a tractable temporal DL named f-\(\mathcal {ALC(S)}\)-LTL, which expands linear temporal logic (LTL) by utilizing fuzzy spatial DL f-\(\mathcal {ALC(S)}\). In this article, we first define the syntax and formal-semantic model of our logic and investigate a tableau rule-based reasoning procedure to verify satisfiability. We further show the correctness and computational complexity of the reasoning procedure and demonstrate a running example of its application. Finally, we implement a prototype reasoning tool that can determine the satisfiability problem. Our case studies show that our logic f-\(\mathcal {ALC(S)}\)-LTL is feasible and the prototype reasoning tool actually works. The logic f-\(\mathcal {ALC(S)}\)-LTL enables tractable reasoning about the dynamic evolution of fuzzy RCC relations over time.