Analysing Temporal Reasoning in Description Logics Using Formal Grammars (IJCAI Extended Abstract)

摘要

We establish a correspondence between (fragments of) TEL^o, a temporal extension of the EL description logic with the LTL operator O^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 TEL^o does not possess the property of ultimate periodicity of models, and further leads to undecidability of query answering in TEL^o, closing a question left open since the introduction of TEL^o. Moreover, it also allows to establish decidability of query answering for some new interesting fragments of TEL^o, and to reuse for this purpose existing tools and algorithms for conjunctive grammars.