Fixpoint Semantics for DatalogMTL with Negation
Samuele Pollaci
TL;DR
The paper addresses the challenge of defining robust semantics for DatalogMTL$^ eg$, a metric-temporal extension of Datalog with unstratifiable negation. It adopts Approximation Fixpoint Theory to construct a three-valued approximation space and a consistent approximator, from which Kripke-Kleene, well-founded, stable, and supported semantics follow. The main contributions are (i) a rigorous AFT-based formulation of three-valued and two-valued models for DatalogMTL$^ eg$, (ii) a proof that AFT-derived stable models coincide with prior HT-based stable models, and (iii) a demonstration of the practical benefits and interoperability of AFT for this temporal logic setting. This work provides a solid, extensible semantic foundation for temporal Datalog with negation and suggests fruitful directions for cross-pollination with related logics such as MEL and stratification theory.
Abstract
DatalogMTL with negation is an extension of Datalog with metric temporal operators enriched with unstratifiable negation. In this paper, we define the stable, well-founded, Kripke-Kleene, and supported model semantics for DatalogMTL with negation in a very simple and straightforward way, by using the solid mathematical formalism of Approximation Fixpoint Theory (AFT). Moreover, we prove that the stable model semantics obtained via AFT coincides with the one defined in previous work, through the employment of pairs of interpretations stemming from the logic of here-and-there.