Temporal substrate

Why bitemporal

The substrate before this section operates on a single state mapping concepts to extents. The mutation grammar (mutate) advances the state from snapshot to snapshot; prior snapshots are not addressable. This section introduces the bitemporal substrate: every fact carries a valid time and a transaction time. Bare queries default to the current snapshot; explicit temporal operators address the past, the future, and the historical record of the system’s beliefs.

The formalism is DatalogMTL (Wałęga et al., IJCAI 2019) with stratified negation (Tena Cucala et al., AAAI 2021) over the integer timeline; the reference reasoner is MeTeoR (Wałęga et al., AAAI 2022).

Valid time and transaction time

Two interval annotations on every fact (and every relation tuple):

• Valid time (VT) — when the fact holds in the world. [VT_start, VT_end], with open-ended [VT_start, ∞] for ongoing.
• Transaction time (TT) — when the system recorded the fact. [TT_start, TT_end], with open-ended [TT_start, ∞] for current belief.

The snapshot view is the projection ${,\mathsf{iof}(x, T),\mid,VT_{\text{start}} \le \mathit{now} \le VT_{\text{end}} ;\wedge; TT_{\text{start}} \le \mathit{now} \le TT_{\text{end}},}$. Bare rule atoms and bare queries default to this view.

The bitemporal extension applies uniformly to all relations, not just iof. A pub rel Enrolment(s: Person, u: University) tuple carries VT and TT just like an iof fact.

Mechanized at spec/lean/Argon/Reasoning/Temporal.lean (BiState as the bitemporal State; TTHistory and TTMonotone for the transaction-time invariant). The bitemporal extension is additive — the termination machinery of Argon.Reasoning.State lifts pointwise without modification.

Retroactive correction and audit

Mutations that close a VT interval retroactively (delete iof(x, T) at #PAST-DATE#) do not erase the prior record. They close its TT interval at now and append a new record with the corrected VT. Audit queries as of TT = #PAST-DATE# reconstruct what the system believed at any past point. The substrate is append-only by default; explicit erasure (forget), crypto-shredding (#[shred_on_forget]), and #[retention(…)] bounds are storage-layer concerns specified in mutate and Storage layer.

Three-valued evaluation under OWA

Under open-world assumption, temporal atoms evaluate to Is | Not | Can. The since and until operators (see Temporal rule atoms) lift to three-valued via the strong-Kleene meet/join tables that truth values defines, composed pointwise across the interval. Unknown temporal extent projects to Can, never to Both — there are no conflicting witnesses, just single-source uncertainty.

Temporal sub-tier

Temporal expressiveness is an orthogonal sub-tier on top of the main tier ladder. Every program has a tier pair (main, temporal) — see Tier ladder.