Fixpoint Semantics for DatalogMTL with Negation

TL;DR

This paper introduces a formal fixpoint semantics framework for DatalogMTL with negation, leveraging Approximation Fixpoint Theory to unify and extend existing semantics.

Contribution

It defines stable, well-founded, Kripke-Kleene, and supported model semantics for DatalogMTL with negation using AFT, providing a simple and rigorous formal foundation.

Findings

Semantics coincide with previous definitions

Formalization via AFT simplifies understanding

Provides a unified approach to DatalogMTL semantics

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.