Analysing Temporal Reasoning in Description Logics Using Formal Grammars

2025/08/01 by Camille Bourgaux, Bourgaux, Camille, Anton Gnatenko +3
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2508.00575

openalex publication_date 2025/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

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

Citations

• On Deciding the Data Complexity of Answering Linear Monadic Datalog Queries with LTL Operators(Extended Version)
• MeTeoR: Practical Reasoning in Datalog with Metric Temporal Operators
• First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries
• On rules with existential variables: Walking the decidability line

Related

• Temporal Conjunctive Query Answering in the Extended DL-Lite Family
• A Standard Grammar for Temporal Logics on Finite Traces
• When is Metric Temporal Logic Expressively Complete?
• On LL(k) linear conjunctive grammars
• Temporal Logic Programs with Variables