Practical Reasoning in DatalogMTL
CoRR(2024)
摘要
DatalogMTL is an extension of Datalog with metric temporal operators that has
found an increasing number of applications in recent years. Reasoning in
DatalogMTL is, however, of high computational complexity, which makes reasoning
in modern data-intensive applications challenging. In this paper we present a
practical reasoning algorithm for the full DatalogMTL language, which we have
implemented in a system called MeTeoR. Our approach effectively combines an
optimised (but generally non-terminating) materialisation (a.k.a. forward
chaining) procedure, which provides scalable behaviour, with an automata-based
component that guarantees termination and completeness. To ensure favourable
scalability of the materialisation component, we propose a novel seminaïve
materialisation procedure for DatalogMTL enjoying the non-repetition property,
which ensures that each specific rule application will be considered at most
once throughout the entire execution of the algorithm. Moreover, our
materialisation procedure is enhanced with additional optimisations which
further reduce the number of redundant computations performed during
materialisation by disregarding rules as soon as it is certain that they cannot
derive new facts in subsequent materialisation steps. Our extensive evaluation
supports the practicality of our approach.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要