Analysing Temporal Reasoning in Description Logics Using Formal Grammars
This addresses foundational issues in temporal logic and knowledge representation for AI and computer science, with incremental contributions to specific fragments.
The paper tackles the problem of analyzing temporal reasoning in description logics by establishing a correspondence between fragments of TEL^○ and formal grammars like conjunctive grammars. This leads to results such as the undecidability of query answering in TEL^○ and decidability for some new fragments, enabling reuse of existing grammar tools.
We establish a correspondence between (fragments of) $\mathcal{TEL}^\bigcirc$, a temporal extension of the $\mathcal{EL}$ description logic with the LTL operator $\bigcirc^k$, and some specific kinds of formal grammars, in particular, conjunctive grammars (context-free grammars equipped with the operation of intersection). This connection implies that $\mathcal{TEL}^\bigcirc$ does not possess the property of ultimate periodicity of models, and further leads to undecidability of query answering in $\mathcal{TEL}^\bigcirc$, closing a question left open since the introduction of $\mathcal{TEL}^\bigcirc$. Moreover, it also allows to establish decidability of query answering for some new interesting fragments of $\mathcal{TEL}^\bigcirc$, and to reuse for this purpose existing tools and algorithms for conjunctive grammars.