On Syntactical Simplification of Temporal Operators in Negation-Free Metric Temporal Logic

Abstract

Temporal reasoning in dynamic, data-intensive environments increasingly demands expressive yet tractable logical frameworks. Traditional approaches often rely on negation to express absence or contradiction. In such contexts, negation-as-failure is commonly used to infer negative information from the lack of positive evidence. However, for open and distributed systems such as IoT networks and the Semantic Web, negation-as-failure semantics become unreliable due to incomplete and asynchronous data. This has led to growing interest in negation-free fragments of temporal rule-based systems, which preserve monotonicity and enable scalable reasoning. This paper investigates the expressive power of negation-free Metric Temporal Logic (MTL), a temporal logic framework designed for rule-based reasoning over time. We show that the “always” operators ⊞ and ⊟, often treated as syntactic sugar for combinations of other temporal constructs, can be eliminated using “once”, “since” and “until” operators. Remarkably, even the “once” operators can be removed, yielding a fragment based solely on “until” and “since”. These results challenge the assumption that negation is necessary for expressing universal temporal constraints and reveal a robust fragment capable of capturing both existential and invariant temporal patterns. Furthermore, the results induce a reduction in the syntax of MTL, which, in turn, can provide benefits for both theoretical study as well as for implementation efforts.