Finite materialisability of Datalog programs with metric temporal operators - Wałęga, PA; Zawidzki, M; Cuenca Grau, B (AI Access Foundation, 2023)
DatalogMTL is an extension of Datalog with metric temporal operators that has recently found applications in stream reasoning and temporal ontology-based data access. In contrast to plain Datalog, where materialisation (a.k.a. forward chaining) naturally terminates in finitely many steps, reaching a fixpoint in DatalogMTL may require infinitely many rounds of rule applications. As a result, existing reasoning systems resort to other approaches, such as constructing large Büchi automata, whose implementations turn out to be highly inefficient in practice.