A Qualitative Temporal Extension of Here-and-There Logic

Abstract

Model-based Diagnosis (MBD) is an approach to diagnosis, where an (objective) model of a system is diagnosed to find a set of explanations revealing root causes for issues. Temporal behavioral models are prominent approach for temporal MBD, where their associated temporal formulas (TBFs) by Brusoni et al. (Artificial Intelligence, 102:39–79, 1998) can be used to relate explanations to observations under temporal constraints based on Allen’s Interval Algebra (IA). Due to expressive limitations of the constructs, we envision an extended language of TBFs that allows for complex formulas and nesting of formulas in temporal constraints. To this end, we present a language that extends propositional resp. FO logic with IA relations and provide semantics for it based on here-and-there (HT) logic as well as on Equilibrium Logic. Furthermore, we lift a well-known tableau calculus for propositional HT logic to the temporal setting and report about an experimental prototype implementation. Based on these results, rich notions of diagnostic explanations from temporal behavior models may be developed.

1 Introduction

Model-based Diagnosis (MBD) [11] is an approach to diagnosis, where an (objective) model of a system is diagnosed to find a set of explanations revealing root causes for errors. For instance in Urban Traffic Management (UTM) systems traffic flow is analyzed over longer periods to reveal root causes for traffic congestions in a road network, e.g., frequent accidents or delays. Temporal behavioral models (TBMs) by Brusoni et al. [5] are a prominent approach for temporal MBD, where their associated temporal formulas (TBFs) can be used to relate explanations to observations under temporal constraints based on Allen’s Interval Algebra (IA). However, TBMs are sometimes too restrictive in expressing complex relationships between possible explanations and observations; more details and an example are given below. Motivated by this fact, we aim at providing a language for finding possible explanations for observations, e.g., for a traffic congestion, using temporal constraints and by extending TBMs for linking temporal relations directly to atoms, supporting undefined time intervals, and allowing for various encodings of “explains”. The extension is a step towards an abduction-based traffic diagnosis framework that combines TBMs, a flow model for observations, e.g., as we presented in previous work [8], and a background knowledge base (KB) that allows one to find likely explanations.

Temporal Behavioral Models. According to [5], a temporal behavioral model (TBM) is defined as a set of temporal behavior formulae (TBFs) and a set of global temporal integrity constraints. For example, a TBF may be used to explain the causal relation between the cause water retention with no fluid therapy and the effect high blood volume [5]:

$$water\_ret(T_1), therapy(absent) \text { explains } blood\_vol(high,T_2) \{ T_1 ( before,overlaps ) T_2 \}.$$

Such a TBF captures the idea that statements on the left-hand-side (LHS) explain observation(s) on the right-hand-side (RHS) taking the local temporal constraints (e.g., $before$) into account, where these constraints must be fulfilled with respect to time intervals assigned to the variables $T_1$ and $T_2$. As Brusoni et al. noted, we may interpret explains in backward or forward direction. Our work aims at using TBMs for traffic diagnosis over a stream of observations to find a set of explanations that capture specific traffic patterns using Allen’s Time Interval Algebra (IA). Therefore, we extend the original TBF syntax as illustrated by the following formula:

$$\begin{array}{@{}l@{\;}l} (a(T_1)\,{\vee }\,b(T_2)),&c(T_3) \text { explains}\ o_1(T_4), o_2(T_5)\ \{ TC \} \end{array} $$

where $TC = \!\{\boldsymbol{(} (T_1 \sqcap \sim T_3) \, overlaps \, (T_4\,{\sqcup }\,T_5) \boldsymbol{)} \vee \boldsymbol{(} (T_2\,{\sqcap }\,T_3) \, overlaps \, (T_4\,{\sqcup }\,T_5) \boldsymbol{)}\}$. The atoms a and b represent the explanations for normal congestion and accident-related congestion, c represents an auxiliary atom stating whether roadworks occur in a time period (with $\sim T_3$ denoting it is known that it is not occurring), and $o_1$ and $o_2$ are two observations of slow traffic. Note that we require coalescing (denoted by $\sqcap$ and $\sqcup$) for time intervals to check the temporal constraints.

The original TBF syntax appears to be not well-suited for expressing complex relationships as above. Furthermore, a reduced syntax (not involving explains nor time intervals explicitly) may be desirable. This can be achieved by the following steps: (a) combine the LHS, RHS, and constraints to one conjunction dropping $\text {explains}$; (b) make the temporal information assigned to atoms implicit, with the possibility of having undefined time intervals; and (c) let temporal relations refer directly to atoms, which allows for nested sub-formulas.

Example 1

We obtain the following formula applying the steps on the TBF above:

$$(a \vee b) \wedge c \wedge \boldsymbol{(} (a \wedge \sim c) \; overlaps \; (o_1 \vee o_2) \boldsymbol{)} \vee \boldsymbol{(} (b \wedge c) \; overlaps \; (o_1 \vee o_2) \boldsymbol{)} \wedge o_1 \wedge o_2. $$

We aim to evaluate whether a or b are explanations supported by observations in various temporal assignments under the temporal constraints, so $(a \wedge \sim c)$ and $(b \wedge c)$ must occur on time intervals that overlap with $(o_1 \vee o_2)$. The meta directive “explains” can be replaced based on the desired reasoning task; we may e.g., conjoin the LHS and RHS for checking the consistency of the new formula according to various temporal assignments, while we may state that the LHS implies the RHS for abductive reasoning.

The new language requires a suitable semantics, where theories can be characterized and an evaluation algorithm can be developed. For this, we build on the work on here-and-there logic (HT) [12] and its extension to Equilibrium Logic [17], which can be evaluated using a tableau system or an ASP solver on restricted formulas. The novel language extends HT logic with coalescing operators, undefined time intervals, and temporal relations. For the evaluation, we extend the tableau calculus for HT logic by Pearce et al. [16] and include temporal expansion rules. We then provide soundness and completeness results for the new tableau system. Besides the technical results, we developed a prototypical implementation to enable initial experimentation with the calculus. Our contributions are developed as follows:

• After stating necessary preliminaries (Sect. 2), we present our temporal extension of HT logic including a novel syntax and semantics (Sect. 3).

• We present a temporal tableau calculus and give technical details about it (Sect. 4).

• We report on a prototypical implementation and illustrate it on a case study (Sect. 5).

• We discuss related work and compare our approach to others for (qualitative) temporal reasoning and conclude with ongoing and future work (Sect. 6).

2 Preliminaries

To analyze temporal behavioral models, we introduce a novel language that is based on an extension of here-and-there (HT) logic [12, 13] with a FO semantics and strong negation called FOHT [17]. The authors of [17] also showed that HT and FOHT are equivalently represented by the five-valued logic N₅ and the quantified five-valued logic QN₅, respectively.

FOHT is a FO language over a signature $\varSigma = \langle \mathcal {C},\mathcal {F}, \mathcal {P} \rangle$, where $\mathcal {C}$ is a (w.l.o.g. nonempty) set of constants, $\mathcal {F}$ a set of functions, and $\mathcal {P}$ a set of predicates. We denote by $Term(\mathcal {C}, \mathcal {F})$ and $Atom(\mathcal {C}, \mathcal {F}, \mathcal {P})$ the sets of ground terms and atoms induced by $\mathcal {C}$ and $\mathcal {F}$, resp. by $\mathcal {C},\mathcal {F}$, and $\mathcal {P}$; furthermore, $Lit(\mathcal {C}, \mathcal {F}, \mathcal {P}) = \{ a, \sim a \mid a \in Atom(\mathcal {C}, \mathcal {F}, \mathcal {P})\}$ is the set of ground literals, where $\sim \;$ is strong negation and a and $\sim a$ are contrary literals; weak negation is denoted by $\lnot$. The notions of free/bound variables and closed formulas (sentences) are as usual.

Definition 1

(cf. [17]). A FOHT-model is a quadruple $\mathcal {M} = \langle D_h, H, D_t, T \rangle$, where $D_h$ and $D_t$ are domains s.t. $\mathcal {C} \subseteq D_h \subseteq D_t$, and $H \subseteq T \subseteq Lit(D, \mathcal {F}, \mathcal {P})$ are sets of literals such that T does not contain contrary literals and H does not contain constants from $D_t\setminus D_h$. The satisfaction relation $\mathcal {M},w\models \phi$ for $w \in \{ h,t\}$, where $h\le h$, $h\le t$, $t\le t$ are totally ordered worlds, and a sentence $\phi$ is depending on the structure of $\phi$ as follows ($\mathcal {T}_w = Term(D_w, \mathcal {F})$):

$\mathcal {M}$ is a model of a closed formula $\phi$, denoted $\mathcal {M} \models \phi$, if $\mathcal {M},h \models \phi$ and $\mathcal {M},t \models \phi$. A closed formula $\phi$ is valid in FOHT if $\phi$ is true in all models.

FOHT under the constant domain assumption, i.e., $D_h = D_t$, is denoted by $\textsc {FOHT}_\text {c}$; we then simplify $\textsc {FOHT}_\text {c}$ models to triples $\mathcal {M} = \langle D, H, T \rangle$ where $D=D_h=D_t$.

In [17], equilibrium models were defined using minimal models for $\textsc {FOHT}_\text {c}$ similar as in HT logic. A model $\mathcal {M}=\langle D, H, T \rangle$ of a theory $\varPi$ over $\varSigma$ is an equilibrium model, if (1) $\mathcal {M}$ is total, i.e., $H\,{=}\,T$, and (2) $\mathcal {M}$ is $\preceq$-minimal among the models of $\varPi$, where $\mathcal {M}_1 \preceq \mathcal {M}_2$ holds for $\mathcal {M}_i = \langle D_i,H_i,T_i \rangle$, $i=1,2$, if $D_1\,{=}\,D_2$, $T_1\,{=}\,T_2$, and $H_1\,{\subseteq }\,H_2$ (tantamount $\varPi$ has no model $\langle D, H', T \rangle$ with $H' \subset H$).

Quantified Many-Valued Logic. The (quantified) many-valued logic N₅ (${\textsc {QN}_{5}}$) allows one to characterize the Kripke-style model semantics of HT-logic using a five-valued matrix for the set $\mathcal {T}_5 = \{ -2,-1,0,1,2 \}$ of truth values. We also will use $\textsc {N}_{3}$ (${\textsc {QN}_{3}}$) with truth-values $\mathcal {T}_3 = \{ -2,-0,2 \}$, when only total models are of interest.

Each k-ary connective F has an associated interpretation function $f_F : \mathcal {T}_5^k \rightarrow \mathcal {T}_5$ as follows:

$$ \begin{array}{l*{5}{|c}} F &{} x \wedge y &{} x \vee y &{} \sim x &{} \lnot x &{} x \rightarrow y \\ \hline f_F &{} \min (x,y) &{} \max (x,y) &{} -1{\cdot }x &{} \left\{ \begin{array}{ll} 2 &{} \text { if } x \le 0 \\ -1{\cdot }x &{} \text { otherwise} \end{array} \right. &{} \left\{ \begin{array}{ll} 2 &{} \text { if } x \le 0 \text { or } x \le y \\ y &{} \text { otherwise} \end{array} \right. \end{array} $$

Definition 2

A valuation (or truth-value assignment) is a function $\sigma : Atom(\mathcal {C}, \mathcal {F}, \mathcal {P}) \rightarrow \mathcal {T}_5$ that can be uniquely extended to a homomorphism from $\varSigma$ to $\mathcal {T}_5$ via $\sigma (F(\phi _1,...,\phi _i)) = f_F(\sigma (\phi _1),...,\sigma (\phi _i))$.

Fig. 1.

Truth table for $x \rightarrow y$

For ${\textsc {N}_{3}}$, interpretations and valuations are restricted to $\mathcal {T}_3$. For $S\subseteq \mathcal {T}_k$, a formula $\phi$ is S-satisfiable (resp., an S-tautology) in N_k, if for some (every) valuation $\sigma$ over $\mathcal {T}_k$ it holds that $\sigma (\phi ) \in S$. In case $S=\{2\}$, we say $\varPhi$ is satisfiable (resp. valid). For instance, we give in Fig. 1 every valuation for an implication with $\sigma (x)$, resp., $\sigma (y)$ shown on the first column, resp., first row (the grey coloring of cells is discussed in Sect. 4).

We use $\phi \equiv _k \psi$ to denote semantic equivalence in N_k, i.e., for every valuation $\sigma$ we have $\sigma (\phi )=\sigma (\psi )$. In ${\textsc {N}_{3}}$, we then have that $(x \rightarrow y) \equiv _3 (\lnot x \vee y)$ as $\sigma (x \rightarrow y) = \sigma (\lnot x \vee y)$ holds for all possible valuations of x and y. Note that this equivalence does not hold for N₅: e.g., for $\sigma (x) = 1$ and $\sigma (y) = -2$ we have $\sigma (x \rightarrow y) = -2$ while $\sigma (\lnot x \vee y) = -1$.

Proposition 1

The following equivalences hold for all formulas $\alpha ,\beta , \gamma$ in N_k, $k=3,5$:

In [17], ${\textsc {QN}}_{5}$ models are pairs $\langle D, \sigma \rangle$, where $D\supseteq \mathcal {C}$ is the domain and $\sigma$ a valuation as above, which is extended to closed formulas by $\sigma (\forall x \; \phi (x)) = min\{ \sigma (\phi (t));\; t \in \mathcal {T} \}$, and $\sigma (\exists x \; \phi (x)) = max\{ \sigma (\phi (t));\; t \in \mathcal {T} \}$, where $\mathcal {T} = Term(D, \mathcal {F})$. If $D_h \ne D_t$, the many-valued semantics does not always coincide with the FOHT-semantics as quantifiers are interpreted as supremum and infimum. However, under restriction to constant domains, $\textsc {FOHT}_\text {c}$-models and ${\textsc {QN}_{5}}$-models tightly correspond.

Proposition 2

(Theorem 1, [17]). A bijection f between $\textsc {FOHT}_\text {c}$-models $\mathcal {M}$ and ${\textsc {QN}_{5}}$-models exists s.t. for each formula $\phi$, $\mathcal {M} \models \phi$ iff $f(\mathcal {M})(\phi )\,{=}\,2$; hence, $\phi$ is is valid in $\textsc {FOHT}_\text {c}$ iff it is valid in ${\textsc {QN}_{5}}$.

Propositional N₅-models (given by $\sigma$) can be converted from/to HT-models with the following table for truth-value assignments $\sigma (p)$, where $p \in Atom(\mathcal {C}, \mathcal {F}, \mathcal {P})$ and $H\,{\subseteq }\,T$ are as in Definition 1.

$$\begin{array}{l@{~}*{5}{@{~}|@{~}c}} &{} \sim p \in H &{} \sim p \in T \wedge \sim p \not \in H &{} p \not \in T \wedge \sim p \not \in T &{} p \in T \wedge p \not \in H &{} p \in H \\ \hline \sigma (p) &{} -2 &{} -1 &{} 0 &{} 1 &{} 2 \end{array}$$

Furthermore, [17] showed how $\preceq$-ordering of HT-models can be transferred to N₅ ’s many-valued semantics. Given a theory $\varPi$ over $\varSigma$ in N₅, the ordering $\sigma _1 \preceq \sigma _2$ of N₅-models $\sigma _1,\sigma _2$ holds, if for every atom $p \in Atom(\mathcal {C}, \mathcal {F}, \mathcal {P})$ the following conditions (1)–(3) hold:

$$\begin{array}{c}(1)\ \sigma _1(p)\,{=}\, 0 \Leftrightarrow \sigma _2(p)\,{=}\, 0; ~ (2)\ \sigma _1(p)\,{<}\,1 \vee \sigma _1(p)\,{\le }\,\sigma _2(p); \text { and } \\ (3)\ \sigma _1(p)\,{>}\,{-}1 \vee \sigma _1(p) \,{\ge }\, \sigma _2(p).\end{array}$$

The equilibrium models of $\phi$ amount then to the $\preceq$-minimal N₅-models $\sigma$ of $\phi$ where no atom is assigned $\{ -1, 1 \}$ (called total); intuitively, no model with less assignments in $\{-2,2\}$ is possible.

Example 2

Consider the formula $\phi : \lnot x \rightarrow y$ and the following HT-models $i_1$ – $i_5$ ($H \subseteq T$):

$$i_1: ( \emptyset , \{ x \}),~ i_2: ( \{ x \}, \{ x \}),~ i_3: ( \{ x \}, \{ x,y \}),~ i_4: ( \{ y \}, \{ y \}),~ and~ i_5: ( \{ x,y \}, \{ x,y \}).$$

The corresponding N₅ models are $\sigma _1 = \{ x\mapsto 1, y\mapsto 0\}$; $\sigma _2 = \{ x\mapsto 2, y\mapsto 0\}$; $\sigma _3 = \{ x\mapsto 2, y\mapsto 1\}$; $\sigma _4 = \{ x\mapsto 0, y\mapsto 2\}$; $\sigma _5 = \{x\mapsto 2, y\mapsto 2\}$. The only equilibrium model of $\phi$ among them is $i_4$: indeed, $i_1$ and $i_3$ are not total models; $i_2$ and $i_5$ are not minimal as $i_1\preceq i_2$ and $i_3 \preceq i_5$.

Allen’s Interval Algebra. For temporal constraints, we will focus on Allen’s Time Interval Algebra (IA) [1] and calculus. IA is based on time intervals and the binary relations defined between them. The domain of IA relations is the set of intervals over the linear order of $\mathbb {T}$ defined as $[p_i] = [\underline{p_i}, \overline{p_i}]$ with $\underline{p_i} < \overline{p_i}$. The 13 basic relations are defined according to their start/end points [1] as shown in Table 1. We denote with $IA _\nu (x,y)$ that a specific relation $\nu$ holds between the two intervals. The 13 basic relations give rise to $2^{13}$ general relations. Note that several base relations can hold between two events represented by intervals that can be open.

Table 1. IA relations with inverses and Allen’s naming in brackets

3 Qualitative Temporal Here-and-There Logic

We now extend the language with (binary) temporal relations, which allow one to state formulas like $(a\wedge \sim c) \ overlaps \ (o_1\vee o_2)$ in the introductory example.

For the evaluation, we extend $\varSigma$ to $\varSigma ^{t} = \langle \mathcal {C},\mathcal {F}, \mathcal {P}, \mathcal {A} \rangle$, where $\mathcal {A} \subseteq \mathcal {L} \times (\mathbb {Z} \times \mathbb {Z})$ is a relation that associates with each literal in $\mathcal {L} = Lit(\mathcal {C}, \mathcal {F}, \mathcal {P})$ at most one time interval from $(\mathbb {Z} \times \mathbb {Z})$, where for contrary literals g and $\sim g$ the associated intervals [x] and [y] must be disjoint, i.e., [x] and [y] have no common point in time.

Formally, $\mathcal {A}$ induces a function $\tau _\mathcal {A} : Lit(\mathcal {C}, \mathcal {F}, \mathcal {P}) \rightarrow (\mathbb {Z} \times \mathbb {Z}) \cup \{ \textbf{u} \}$ called temporal assignment, where $\textbf{u}$ is the undefined time instance, and for each $g \in Lit(\mathcal {C}, \mathcal {F}, \mathcal {P})$:

$$\tau _\mathcal {A}(g) = \left\{ \begin{array}{ll} \textbf{u} &{} \text { if } (g, (t_1,t_2)) \not \in \mathcal {A}, \\ (t_1,t_2) : (g, (t_1,t_2)) \in \mathcal {A} &{} \text { otherwise}. \\ \end{array}\right. $$

In slight abuse of terminology, we will call $\mathcal {A}$ also temporal assignment. Note that the assignment to contrary literals does not cover the whole timeline; intuitively, $\tau (g)$ expresses that for this interval the truth value of g is certain. The value $\textbf{u}$ stands for time information that is non-evaluable, due to missing observations (at evaluation time), or due to intervals that cannot be coalesced (as seen later).

Example 3

Consider a model $\mathcal {M}_2 = \langle D, (H, \mathcal {A}_1), (T, \mathcal {A}_1) \rangle$ with $D = \{x,y,z\}$ and the formula $\phi : (p(x) \vee p(y)) \wedge ((p(x) \; before \; p(z)) \vee (p(y) \; before \; p(z)))$. A possible temporal assignment over which $\phi$ should be evaluated is $\mathcal {A}_1 = \{(p(x), [1,2]), p(y), [2,3]), (p(z), [4,5]) \}$.

To evaluate a formula $a\ before \ b$, say, where a and b are atoms, we can readily use $\tau$ above to assess the temporal relationship of a and b. However, for complex formulas $\alpha \ \nu \ \beta$, where $\alpha$ and $\beta$ are non-atomic, as in case of $(a\wedge {\sim } c) \ overlaps \ o_1\vee o_2$, an evaluation on the basis of $\tau$ is non-obvious in general. We thus restrict formulas by disallowing nested temporal relations and some connectives.

Definition 3

A flat temporal formula (FTF) is of the form $\alpha \;\nu \; \beta$, where $\nu$ is a temporal relation and $\alpha$ and $\beta$ are closed formulas without temporal relations, implication $\rightarrow$ and weak negation $\lnot$.

In the rest of this paper, we then consider formulas in the extended language in which each occurring subformula $\alpha \;\nu \ \beta$ is an FTF.

Coalescing. For the evaluation of formulas $\alpha$ and $\beta$ nested in FTFs, we introduce two coalescing operators, where we distinguish between coalescing intervals associated with a conjunction resp. disjunction.

Definition 4

The coalescing operators $coal_{\wedge }(x,y)$ and $coal_{\vee }(x,y)$ for the intervals $x=\tau (\alpha )$ and $y=\tau (\beta )$ associated with the literals $\alpha$ and $\beta$ in $\alpha \wedge \beta$ resp. $\alpha \vee \beta$, are as in the following table:¹

In Example 3, we have for instance that $coal_{\vee }(\tau _{\mathcal {A}_1}(p(x)), \tau _{\mathcal {A}_1}(p(y)))=[1,3]$.

Temporal assignments can then be generalized to formulas $\alpha$ and $\beta$ inside FTFs by a (nested) temporal assignment $\phi \mapsto \tau _\mathcal {A}^*(\phi )$ where

$$\tau _\mathcal {A}^*(\phi ) = \left\{ \begin{array}{ll} \tau _\mathcal {A}(\phi ) &{} \text { if } \phi \in Lit(\mathcal {C}, \mathcal {F}, \mathcal {P}), \\ coal_{\circ }(\tau _\mathcal {A}^*(\phi _1), \tau _\mathcal {A}^*(\phi _2))) &{} \text { if } \phi : \phi _1 \circ \phi _2, \text { for } \circ \in \{\wedge , \vee \}, \\ \tau _\mathcal {A}^*(\phi _1) &{} \text { if } \phi = \sim \!\sim \phi _1, \\ \tau _\mathcal {A}^*(\sim \phi _1\wedge \!\sim \phi _2) &{} \text { if } \phi = \sim (\phi _1\vee \phi _2), \\ \tau _\mathcal {A}^*(\sim \phi _1\vee \!\sim \phi _2) &{} \text { if } \phi = \sim (\phi _1\wedge \phi _2). \end{array} \right. $$

By convention, we regard for $\tau _\mathcal {A}^*$ conjunctions $\alpha \wedge \beta \wedge \gamma$ as $\alpha \wedge (\beta \wedge \gamma )$, and similar for disjunctions.

Next, we introduce $\textsc {FOHT}^\text {t}_\text {c}$-models over the extended signature $\varSigma ^\text {t}$. They extend $\textsc {FOHT}_\text {c}$-models to tuples $\mathcal {M}^t = \langle D, (H, \mathcal {A}_h ), (T, \mathcal {A}_t) \rangle$, where D, H, and T are as before, and $\mathcal {A}_h \subseteq \mathcal {A}_t$, are assignments.

Definition 5

The satisfaction relations $\models$ for $w \in \{ h,t\}$, where h, t are defined as before, is extended based on Definition 1 with temporal relations, denoted as $\nu$ (e.g., $\nu := before$):

• $\mathcal {M}^t,w \models \boldsymbol{(} \alpha \;\nu \; \beta \boldsymbol{)}$ if $\mathcal {M}^t,w \models \alpha$ and $\mathcal {M}^t,w \models \beta$, $\tau ^*_w(\alpha ) \ne \textbf{u}$, $\tau ^*_w(\beta ) \ne \textbf{u}$, and $IA _\nu (\tau ^*_w(\alpha ),\tau ^*_w(\beta ))$ holds;

• $\mathcal {M}^t,w \models \sim \boldsymbol{(}\alpha \;\nu \; \beta \boldsymbol{)}$ if $\mathcal {M}^t,w \models \alpha$ and $\mathcal {M}^t,w \models \beta$, $\tau ^*_w(\alpha ) \ne \textbf{u}$, $\tau ^*_w(\beta ) \ne \textbf{u}$, and $IA _\nu (\tau ^*_w(\alpha ),\tau ^*_w(\beta ))$ does not hold;

Note that $\mathcal {M}^t,w \not \models \alpha \;\nu \; \beta$ iff either (i) $\mathcal {M}^t,w \not \models \alpha$, (ii) $\mathcal {M}^t,w \not \models \beta$, (iii) $\tau ^*_w(\alpha ) = \textbf{u}$, or (iv) $\tau ^*_w(\beta ) = \textbf{u}$.

As previously, we call $\mathcal {M}^t$ a model of a closed formula $\phi$, denoted as $\mathcal {M}^t \models \phi$ if $\mathcal {M}^t,h \models \phi$ and $\mathcal {M}^t,t \models \phi$; validity is defined accordingly.

To lift the notion of equilibrium models, we need to adjust the minimality property of $\textsc {FOHT}_\text {c}$ by taking temporal assignments into account.

Definition 6

A model $\mathcal {M}^t = \langle D, (H, \mathcal {A}_h), (T, \mathcal {A}_t) \rangle$ of a theory $\varPi$ over $\varSigma ^{t}$ is an equilibrium model if

• 1. M is total, i.e., $H=T$ and $\mathcal {A}_h=\mathcal {A}_t$, and

• 2. M is $\preceq '$-minimal among the models of $\varPi$, where $\mathcal {M}^t_1 \preceq ' \mathcal {M}^t_2$ holds, for $\mathcal {M}^t_i = \langle D, (H_i, \mathcal {A}^i_h), (T_i, \mathcal {A}^i_t) \rangle$, $i=1,2$, if (i) $T_1=T_2$, (ii) $\mathcal {A}^1_{h}=\mathcal {A}^2_{h}, \mathcal {A}^1_{t}=\mathcal {A}^2_{t}$ and (iii) $H_1\subseteq H_2$.

That is, temporal assignments are frozen for model comparison. However, alternatives may be considered that view the relation between $\mathcal {A}^1$ and $\mathcal {A}^2$ differently, which we leave for further study.

In the (quantified) many-valued logics N_k resp. QN_k, truth value assignments are extended to temporal formulas, taking temporal assignments into account as follows.

Definition 7

An extended QN_k, model is a triple $\langle D, \sigma , \tau _{\mathcal {A}} \rangle$, where $D,\sigma$ and $\tau _{\mathcal {A}}$ are as before, such that $\sigma$ maps non-temporal formulas $\phi$ to $\mathcal {T}_k$ as before, and temporal formulas $\alpha \;\nu \; \beta$ to $\mathcal {T}_k$ using $\tau _{\mathcal {A}}^*$, with $\nu$ as a temporal relation we have

$$ \sigma (\alpha \; \nu \; \beta ) = \frac{1}{2}{\cdot }eval_{\nu }(\tau _{\mathcal {A}}^*(\alpha ),\tau _{\mathcal {A}}^*(\beta )){\cdot }\min ( \sigma (\alpha ), \sigma (\beta )) $$

where (i) $eval_{\nu }(x,y) = 2$ if $x,y \ne \textbf{u}$ and $IA _\nu (x,y)$ holds, (ii) $eval_{\nu }(x,y) = {-}2$ if $x,y \ne \textbf{u}$ and $IA _\nu (x,y)$ does not hold, and (iii) $eval_{\nu }(x,y) = 0$ if $x = \textbf{u}$ or $y = \textbf{u}$.

Note that the strong negation of a temporal formula evaluates to $\sigma (\sim (\alpha \; \nu \; \beta )) = -\sigma (\alpha \; \nu \; \beta )$.

Example 3 (cont.) For the formula $\phi$, we look at the following five interpretations: $i_1$:$( \emptyset , \{ (p(x), [1,2]) \})$,$i_2$:$( \{ (p(x), [1,2]) \}, \{ (p(x), [1,2]) \})$,$i_3$:$( \{ (p(x), [1,2]), (p(z), [4,5]) \} , \{ (p(x), [1,2]), (p(z), [4,5]) \})$,$i_4$:$( \{ (p(x), [1,2]), (p(y), [2,3]), (p(z), [4,5]) \},$ $\{ (p(x), [1,2]), (p(y), [2,3]), (p(z), [4,5]) \})$, and $i_5: ( \{ (p(y), [2,3]),$ $p(z), [4,5]) \}, \{ (p(y), [2,3]), (p(z), [4,5]) \})$. Only $i_3$ and $i_5$ are equilibrium models, since $i_1$ is not a total model, $i_2$ is not a model, and $i_4$ is not minimal since $i_3 \preceq i_4$ as well as $i_5 \preceq i_4$. If $\mathcal {A}_2 := \mathcal {A}_1 \setminus \{ (p(y), [2,3]) \}$, the only equilibrium model is $i_3$, since $\tau _{\mathcal {A}_2}(p(y))=\textbf{u}$.

4 Temporal Tableau Calculus

As described in [16], the validity of a set of N₃ formulas (similarly for N₅) can be checked by a labeled tableau system, where possible truth-values are assigned as labels (also called signs) in tableau nodes. Then total models can be generated by applying the tableau rules that work with labels over the set $\mathcal {T}_3 = \{ -2,0,2 \}$ of truth values. We first present the (labeled) non-temporal tableau system in [16], on which we then build our temporal tableau system.

Tableau system for total models. A tableau system applies expansion rules (as given in Defn. 8) on an initial tableau $\varPi = \{ \phi _1,...,\phi _n \}$ of arbitrary N₃ formulas, the initial tableau is defined as shown on the right:

Definition 8

The tableau expansion rules capture the connectives of N₃ in the standard way; we show them for all connectives, where the label S is from ${\textsc {S}} := \{ \{ 2 \}$, $\{ 0,2 \}$, $\{ -2,0 \}, \{-2\}\}$, $S^+$ from ${\textsc {S}}^+ :=\{ \{ 2,0 \}, \{ 2\}\}$ and $S^-$ from ${\textsc {S}}^- :=\{ \{ -2,0 \}, \{ -2 \}\}$:

where $(-1){\cdot } S = \{ (-1){\cdot }x\mid x\in S\}$. Only the labels in ${\textsc {S}}$ are relevant for the tableau expansion, e.g., $\{0\}$ does not occur. The expansion rules for a connective are computed based on the coverage in its truth table [7]. For instance, the implication connective was computed based on Fig. 1 with one rule for $S^-$ covering the non-blank cells, and another rule for $S^+$ as disjunction covering the blank cells.

Definition 9

A tableau $\mathfrak {T}$ is generated by the tableau system for $\varPi = \{ \phi _1,...,\phi _n \}$ by applying the above tableau expansion rules on formulas $S:\phi$, where $S \in \textsc {S}$, expanding it to one or more branches. After use, formulas are marked for each branch, so are applicable only once per branch. A branch in $\mathfrak {T}$ is

• closed, if for a formula $\phi$ in it, there are labels $S_1:\phi ,\; S_2:\phi$ with $S_1 \cap S_2 = \emptyset$;

• finished, if all its formulas are marked, and is open if it is finished and not closed.

$\mathfrak {T}$ is closed, if every branch is closed, it is open if at least one branch is open, and it is terminated if every branch is either closed or open.

Based on the above definition, the total models of a conjunction $\phi _1\wedge \cdots \wedge \phi _n$ of N₃ formulas, represented as a set $\varPhi = \{ \phi _1,...,\phi _n \}$, are generated by the tableau system from the open branches of a tableau $\mathfrak {T}$ for $\varPhi$, where for an atom $p_i$ a truth assignment $\sigma (p_i) \in S_i$ is taken from the signed literals $\varSigma = \{ S_1:p_1,..., S_n:p_n \}$ of an open branch in $\mathfrak {T}$ (Theorem 3 in  [16]); notably, if $p_i$ does not occur in $\varSigma$, any truth value can be assigned to it.

Example 4

For $\varPhi = \{ \sim q, \lnot p \rightarrow q, \lnot r \rightarrow p \}$ [16], the generated tableau tree is given in Fig. 2a. For the two open branches, we can derive three models: $i_1: (\{ p,\sim q,r \}, \{ p, \sim q,r\})$, $i_2: ( \{ p,\sim q \}, \{ p,\sim q \})$, and $i_3: ( \{ p,\sim q, \sim r \}, \{ p,\sim q, \sim r \})$; only $i_2$ is minimal, as $i_2 \preceq i_1$ as well as $i_2 \preceq i_3$.

Validity of a formula $\phi$ in N₃ can be established via a tableau proof, which is any closed tableau $\mathfrak {T}$ for $\lnot \phi$. We write $\vdash _{\textsc {N}_{3}} \phi$ in this case.

Definition 10

A branch $\theta$ in $\mathfrak {T}$ is satisfiable, if for every signed formula $S_i : \phi _i$ on $\theta$, there is a valuation such that $\sigma (\phi _i) \in S_1 \cap \cdots \cap S_n$ where $S_1:\phi _i$ to $S_n:\phi _i$ are on branch $\theta$. A tableau $\mathfrak {T}$ is satisfiable if at least one branch of $\mathfrak {T}$ is satisfiable.

We recall from [9] that soundness, resp., completeness, of a tableau system is, if a theory $\varPi$ has a tableau proof, then $\varPi$ is a tautology, i.e., $\vdash _{\textsc {N}_{3}} \varPi$ implies $\models _{\textsc {N}_{3}} \varPi$, resp., if $\varPi$ is a tautology, then $\varPi$ has a tableau proof, i.e., $\models _{\textsc {N}_{3}} \varPi$ implies $\vdash _{\textsc {N}_{3}} \varPi$. Both were merely sketched in Theorem 2 of  [16]. However, Fitting’s method [9] can be extended to show soundness by establishing that satisfiability is a tableau system’s loop invariant. For the completeness proof, we follow the generic approach by Hähnle [10] and use its machinery. Due to space limitations, we only show the proofs for the temporal tableau system since the non-temporal system is its special case.

Temporal Tableau Extension. A temporal tableau system is an extension of the non-temporal tableau of the previous section and introduces the process of signing up N₃ formulas with temporal labels. Besides the existing labels of tableau nodes, we also sign-up formulas in the tableau according to given temporal assignments $\mathcal {A}$, where the functions $\tau$ and $\tau ^*$ are defined as before.

Definition 11

Given a set $\mathcal {A}$ of pairs (p, [x]) inducing a temporal assignment $\tau$ and a formula $\phi$, we let $t_\mathcal {A}(\phi ) = \{ (p,[x]) \in \mathcal {A} \mid p = a \text { or } p = \sim a, a \in atm (\phi )\}$ denote the local temporal assignment for $\phi$ w.r.t. $\mathcal A$, where $atm (\phi )$ denotes the set of atoms occurring in $\phi$.

Temporal tableau system for total models. A temporal tableau system applies expansion rules on an initial tableau $\varPi = \{ \phi _1,...,\phi _n \}$ of $(\varPi ,\mathcal {A})$ with the temporal assignment $\mathcal {A}$; the initial tableau, shown to the right, includes labels with temporal assignments denoted as $S: (\phi _{i})_{t_\mathcal {A}(\phi _i)}$.

Definition 12

The tableau expansion rules from above are extended with temporal assignments; we show some exemplary rules; the other rules can be extended similarly:

Note that the assignments $t_{\mathcal {A'}}(\phi )$ and $t_{\mathcal {A'}}(\psi )$ are easily calculated from $\mathcal {A'}$ and $\phi$ resp. $\psi$; in any tableau extending the initial tableau, they amount to $t_{\mathcal {A}}(\phi )$ resp. $t_{\mathcal {A}}(\psi )$ for the given assignment $\mathcal {A}$. The reason for the use of (local) assignments in each branch relates (besides it is purely syntactical nature) to future work, where nested temporal formulas and multiple intervals per literal could be allowed.

Furthermore, there are additional expansion rules for temporal formulas:

where $E:= eval_{\nu }(\tau ^*_\mathcal {A'}(\phi ), \tau ^*_\mathcal {A'}(\psi ))$ is as in Definition 7. Since the temporal formula must evaluate to 0 if $E=0$, the upper left rules generate a closed branch and the upper right rules a branch that cannot be closed. The lower left rules work only for $S^+=\{0,2\}$ and $S^+=\{2\}$: $E\ne 0$ must hold. If $E=2$, the input S must be $\{0,2\}$ resp. $\{2\}$ and the case amounts to conjunction; if $E=-2$, the input must be $\{0,-2\}$ resp. $\{-2\}$ and the case amounts to conjunction of the strongly negated formulas $\phi _{t_\mathcal {A'}(\phi )}$ and $\psi _{t_\mathcal {A'}(\psi )}$. The lower right rule similarly requires $E\ne 0$. It covers for $E=2$ and $S=\{0,-2\}, \{-2\}$ the conjunction of the sub-formulas, and for $E=-2$ and $S=\{0,2\}, S=\{2\}$ the conjunction of the strongly negated sub-formulas. This reflects the truth value assignment described in Definition 7.

A tableau $\mathfrak {T}^\text {t}$ is generated from the tableau system on $(\varPi ,\mathcal {A})$ by applying the above expansion rules on formulas $S:\phi _{\mathcal {A'}}$ to expand it to one or more branches. The formulas are marked for each branch after being used. The notions of closed, finished, and open branch in $\mathfrak {T}^\text {t}$ can be carried over, and similarly whether $\mathfrak {T}^\text {t}$ is closed or open.

Definition 13

Given a tableau system $(\varPi , \mathcal {A})$, a temporal tableau proof is a closed tableau $\mathfrak {T}^{t}$ for $\{\lnot \varPi \}$ and $\mathcal {A}$; $\varPi$ is a theorem in this case.

Next, we show soundness for the temporal tableau system.

Definition 14

Let $\varPhi = \{ (\phi _i)_{t_\mathcal {A}(\phi _i)}\mid i=1,\ldots ,n\}$ be temporal assigned formulas for $\mathcal {A}$. Then, $(\varPhi , \mathcal {A})$ is satisfiable for $\mathcal {T}_3$, if for some valuation $\sigma$ (with $\tau ^*$ embedded), $\sigma ((\phi _i)_{t_\mathcal {A}(\phi _i)}) = 2$ for all $i=1,\ldots ,n$. A branch $\theta$ in a temporal tableau $\mathfrak {T}^{t}$ is satisfiable, if for some valuation $\sigma$ every formula $S : (\phi )_{t_\mathcal {A}(\phi )}$ on $\theta$ fulfills $\sigma ((\phi )_{t_\mathcal {A}(\phi )}) \in S$. A temporal tableau $\mathfrak {T}^{t}$ is satisfiable under $\mathcal {A}$, if some branch of $\mathfrak {T}^{t}$ is satisfiable.

Proposition 3

Any application of the tableau expansion rules defined in Definition 12 to a satisfiable tableau yields another satisfiable tableau.

Proof

Assume a tableau $\mathfrak {T}^{t}$ that is satisfiable, and a tableau expansion rule is applied to $\mathfrak {T}^{t}$ to a signed formula $S_i : \phi _\mathcal {A'}$ resulting in the tableau $\mathfrak {T}^{{t}{'}}$; we show that $\mathfrak {T}^{{t}{'}}$ is also satisfiable. We distinguish several cases as follows, where we choose some satisfiable branch $\theta '$ in $\mathfrak {T}^{t}$ (which must exist):

Case 1 $\theta ' \ne \theta$: The rule was applied to $\theta$, hence $\theta '$ and $\mathfrak {T}^{{t}{'}}$ are still satisfiable.

Case 2 $\theta ' = \theta$. We distinguish between sub-cases depending on the tableau expansion rule type:

Case 2a $S_i: (\phi _{1} \wedge \phi _{2})_\mathcal {A'}$: As $(\phi _{1} \wedge \phi _{2})_\mathcal {A'}$ is on the branch already, it is satisfied by some valuation $\sigma$, and w.l.o.g. $\sigma (\phi _\mathcal {A'}) = \sigma ((\phi _{1} \wedge \phi _{2})_\mathcal {A'}) \in S_i$. If $S_i= \{0,-2\},\{-2\}$, then $\sigma (\phi _\mathcal {A'}) \le 0$ and by the expansion rule $S_i : \phi _\mathcal {A'}$ may be put on $\theta '$, and so $\theta '$ remains satisfiable. Otherwise, if $S_i= \{0,2\},\{2\}$, both $S_i:(\phi _1)_{t_\mathcal {A'}(\phi _1)}$ and $S_i:(\phi _2)_{t_\mathcal {A'}(\phi _2)}$ are on the branch $\theta '$, and as $\sigma ((\phi _1)_{t_\mathcal {A'}(\phi _1)})\le \sigma ((\phi _2)_{t_\mathcal {A'}(\phi _2)})$ holds $\sigma ((\phi _2)_{t_\mathcal {A'}(\phi _2)}) \in S_i$ hold as well. Thus, $\theta '$ is satisfiable and $\mathfrak {T}^{{t}{'}}$ is satisfiable.

Case 2b $S_i: (\phi _{1} \vee \phi _{2})_\mathcal {A'}$: The argument is similar to the one on Case 2a, respecting $\max (x,y)$ for $\vee$ instead of $\min (x,y)$ for $\wedge$.

Case 2c $S_i: (\sim \phi _{i})_\mathcal {A'}$: Here, $\theta$ was sequentially extended with $(-1) \cdot S_i: (\phi _i)_{t_\mathcal {A'}(\phi _i)}$ resulting in $\mathfrak {T}^{{t}{'}}$. Satisfiability is preserved since $\sigma ((\phi _i)_{t_\mathcal {A'}(\phi _i)}) \in (-1) \cdot S_i$ iff $\sigma ((\sim \phi _{i})_\mathcal {A'}) \in S_i$ by Definition 2.

Case 2d $S_i: \lnot (\phi _i)_\mathcal {A'}$: Based on Definition 2, we have two subcases, for $\sigma (\lnot (\phi _i)_\mathcal {A'}) \in S_i$: where (i) $\sigma (\lnot (\phi _i)_\mathcal {A'}) = 2$ or (ii) $\sigma (\lnot (\phi _i)_\mathcal {A'}) = -2$. By the expansion rules of Definition 8, in case (i) $\theta$ was sequentially extended with $\{-2,0\}:(\phi _i)_\mathcal {A'}$, and in case (ii) with $\{2\}:(\phi _i)_\mathcal {A'}$. As with Case 2c, satisfiability is preserved as $\sigma (\lnot (\phi _i)_\mathcal {A'}) = 2$ implies $\sigma ((\phi _i)_\mathcal {A'}) \in \{-2,0\}$ respectively $\sigma (\lnot (\phi _i)_\mathcal {A'}) = -2$ implies $\sigma ((\phi _i)_\mathcal {A'}) \in \{2\}$.

Case 2e $S_i:(\phi _{1} \rightarrow \phi _{2,})_\mathcal {A'}$: Let $x:= \sigma ((\phi _{1} \rightarrow \phi _{2})_\mathcal {A'})$. For $S_i=\{2\}$ or $S_i= \{-2\}$, the expansion rules of Definition 8 clearly preserve satisfiability via Definition 2. For $S_i=\{0,2\}$, in case $x=2$ satisfiability is preserved by the branch $\{-2,0\}: (\phi _1)_{t_\mathcal {A'}(\phi _1)}$ if $\sigma ((\phi _1)_{t_\mathcal {A'}(\phi _1)}) = -2$ or $\sigma ((\phi _1)_{t_\mathcal {A'}(\phi _1)}) = 0$, and by the branch $\{0,2\}: (\phi _2)_{t_\mathcal {A'}(\phi _2)}$ if $\sigma ((\phi _2)_{t_\mathcal {A'}(\phi _2)})=2$; likewise, if $x=0$ satisfiability is preserved by the branch $\{0,2\}: (\phi _2)_{t_\mathcal {A'}(\phi _2)}$ as $\sigma ((\phi _2)_{t_\mathcal {A'}(\phi _2)})=0$. Finally, for $S_i=\{-2,0\}$, in case $x=-2$ (resp., $x=0$) by Definition 2$\sigma ((\phi _1)_{t_\mathcal {A'}(\phi _1)}) = 2$ and $\sigma ((\phi _2)_{t_\mathcal {A'}(\phi _2)})=-2$ (resp., $\sigma ((\phi _2)_{t_\mathcal {A'}(\phi _2)})=0$), which are in the respective labels $\{2\}$ and $\{-2,0\}$. Thus, satisfiability of $\mathfrak {T}^{{t}{'}}$ is preserved.

Case 2f $S_i: (\phi \,\nu \, \psi )_\mathcal {A'}$: We distinguish three cases according to $E:= eval_{\nu }(\tau ^*_\mathcal {A'}(\phi ), \tau ^*_\mathcal {A'}(\psi ))$:

• (i) $E=0$. We have $\sigma ((\phi \,\nu \, \psi )_\mathcal {A'}) = \frac{1}{2}{\cdot }\min ( \sigma (\phi ), \sigma (\psi )) = 0$; as $\theta$ is satisfiable, the rule for $E=0$ cannot be applied.

• (ii) $E=2$. As $\theta$ is satisfiable, $\min ( \sigma (\phi ), \sigma (\psi )) \in S$. Now if the rule for $\frac{1}{2}E{\cdot }S=S^+$ is applied, we have $S=S^+=\{0,2\}$ or $S=S^+=\{2\}$; hence $\sigma (\phi ) \in S^+$ and $\sigma (\psi ) \in S^+$follows, and thus $\theta '$ is satisfiable. If the rule for $\frac{1}{2}E{\cdot }S=S^-$ is applied, we have $S=S^-$ $=\{0,-2\}$ or $S=S^-=\{-2\}$; thus, either $\sigma (\phi )\in S^-$ or $\sigma (\psi ) \in S^-$ must hold. Hence, extending $\theta$ with $S^-:(\phi )_{\tau _\mathcal {A'}^*(\phi )}$ resp. $S^-:(\psi )_{\tau _\mathcal {A'}^*(\psi )}$ yields a satisfiable branch $\theta '$ and $\mathfrak {T}^{{t}{'}}$ is satisfiable.

• (iii) $E=-2$. The argument is analogous to the one for the case $E=2$.

   $\square$

Case 2f takes nested FTFs into account, hence $\theta '$ is only expanded by non-temporal rules applied to $S_i: (\phi )_{\tau _\mathcal {A'}^*(\phi )}$ and $S_i: (\psi )_{\tau _\mathcal {A'}^*(\psi )}$ with the local temporal assignments $\tau ^*$ carried over. They do not affect satisfiability in derived branches of $\theta '$, but are needed to evaluate minimal models and future work, where also nested temporal formulas are allowed.

Proposition 4

If there is a closed tableau for $(\varPi , \mathcal {A})$, then $(\varPi , \mathcal {A})$ is not satisfiable.

Proof

Assume towards a contradiction that we have a closed tableau while $(\varPi , \mathcal {A})$ is satisfiable. We construct a tableau $\mathfrak {T}^{t}$ from $(\varPi , \mathcal {A})$ with the initial branch $\theta$ that is constructed from $(\varPi , \mathcal {A})$ and is satisfiable. Then according to Proposition 3, either $\theta$ or one of the successor branches of $\theta$ will not be closed, hence we obtain a contradiction to the assumption.    $\square$

Theorem 1

(Soundness) If $(\varPi , \mathcal {A})$ has a tableau proof, then $(\varPi , \mathcal {A})$ is a tautology.

Proof

As a consequence of Proposition 4, if there is a closed tableau for the set $\{\lnot \varPi \}$ of negated temporal N₃ formulas and $\mathcal {A}$, then $\{\lnot \varPi \}$ is not a satisfiable set. It follows that $(\varPi , \mathcal {A})$ is a tautology.    $\square$

Completeness is shown based on propositional Hintikka sets for the many-valued setting, enriched with further (local) temporal assignments. We follow the generic approach in [10] and use its machinery.

A many-valued sets-as-signs (mvs) Hintikka set is a set $\varPhi$ of signed formulas such that

• (H1) $\varPhi$ is open, i.e., there are no signed formulas $S_1:\phi , \ldots , S_n:\phi$ in $\varPhi$ such that $\bigcap _{i=1}^n S_i = \emptyset$, nor any formulas $S: \gamma (\phi _1,\ldots ,\phi _m)$ such that $S\cap rg(\gamma )=\emptyset$, where $rg(\gamma )$ are the possible truth values for the connective $\gamma$, and

• (H2) if $\phi = S: \gamma (\phi _1,\ldots ,\phi _m)$ is in $\varPhi$ and $\psi = \bigvee _{i=1}^l C_i$ is some sets-as-signs DNF representation of $\phi$, then for some $C_i = \bigwedge _{j=1}^{n_i} S_{i,j}\,{:}\,\psi _{i,j}$, it holds that $\{S_{i,1}\,{:}\,\psi _{i,1},\ldots ,S_{i,n_i}\,{:}\,\psi _{i,n_i}\} \subseteq \varPhi$.

Here $\gamma$ is a connective and a sets-as-signs DNF representation of $\phi$ is a satisfiability preserving formula $\psi$ of the given form where each $S_{i,j}$ is from ${\textsc {S}}\cup \{ \{0\}\}$ and each $\psi _{i,j}$ is from $\phi _1,\ldots ,\phi _m$. Then

Proposition 5

(cf. [10]). Every mvs-Hintikka set $\varPhi$ has a model, i.e. a truth assignment $\sigma$ such that $\sigma (\phi ) \in S$ for each $S:\phi \in \varPhi$.

Notably, from DNF representations corresponding tableau rules can be readily obtained.

Definition 15

(Defn. 33 in [10]). Let $\phi = S: \gamma (\phi _1,\ldots ,\phi _m)$ , $m \ge 1$, be a signed formula. Given a sets-as-signs DNF representation $\bigvee _{i=1}^l C_i$ of $\phi$ where $C_i = \bigwedge _{j=1}^{n_i} S_{i,j}\,{:}\,\phi _{i,j}$, the corresponding sets-as-signs tableau expansion rule for $\phi$ is, where $\bigwedge _{\psi \in F}\psi = C_i$:

From Proposition 5, we can then conclude that an open branch $\theta$ in a tableau $\mathfrak {T}$ for a formula $\lnot \varPi$ on which all possible rules have been applied, is an mvs-Hintikka set and thus has a model; hence, $\lnot \varPi$ is satisfiable. It follows that if $\varPi$ is valid then a tableau proof for $\varPi$ exists.

We extend mvs-Hintikka sets and sets-as-signs DNFs to the temporal setting for formulas $S:\phi _\mathcal {A'}$ where $S:\phi$ is a signed temporal formula labeled with a temporal assignment $\mathcal {A'}$ as in the extension of the tableau rules. As for temporal operators, we observe:

Lemma 1

Every FTF formula $\phi = (\phi \;\nu \;\psi )$ can be viewed as a formula $\gamma _E(\phi _1,\phi _2)$ where $E:= eval_{\nu }(\tau ^*_\mathcal {A}(\phi _1), \tau ^*_\mathcal {A}(\phi _2))$, i.e. as a connective $\gamma _E$ depending on the operator $\nu$ and the assignment $\mathcal {A}$.

In (H1), the notion of open set is extended by labeling each $S_i: \phi _i$ resp. $S: \gamma (\phi _1,\ldots ,\phi _m)$ with an assignment $\mathcal {A}'$; in (H2), the notion of sets-as-sign DNF representation is extended by requiring that satisfiability of $\phi = S: \gamma (\phi _1,\ldots ,\gamma _m)_{\mathcal {A}'}$ is preserved by $\psi =\bigvee _{i=1}^l C_i$, with $C_i = \bigwedge _{j=1}^{n_i} S_{i,j}:{\psi _{i,j}}_{\mathcal {A}'_{i,j}}$, where each formula $\alpha _{\mathcal {A}'}$ is evaluated using the assignment $\mathcal {A}'$. Proposition 5 then generalizes to the resulting temporal mvs-Hintikka sets.

For our concerns, we note that the tableau rules above ensure for the formulas on a temporal tableau Condition (H2).

Example 5

This example shows the theories $\varPhi _1 = \{ \{2\}{:}(a \vee b)_{\mathcal {A}_1},\; \{2\}{:}\boldsymbol{(}a \; before \; c \boldsymbol{)}_{\mathcal {A}_2},\; \{2\}{:}(c)_{\mathcal {A}_3}\}$, and $\varPhi _2 = \{\{2\}{:}(a \wedge b)_{\mathcal {A}_1},\; \{2\}{:}\boldsymbol{(} b \; before \; c \boldsymbol{)}_{\mathcal {A}_4},\; \{2\}{:}(c)_{\mathcal {A}_3}\}$, where the temporal assignments are not given but we assume that $eval_{(p)}(\tau ^*_{\mathcal {A}_2}(a), \tau ^*_{\mathcal {A}_2}(c)) = 2$ and $eval_{(p)}(\tau ^*_{\mathcal {A}_4}(b), \tau ^*_{\mathcal {A}_4}(c)) = -2$. Then $\varPhi _1$ can be represented by a mvs-Hintikka set since Condition (H2) is fulfilled as it can be converted from CNF to sets-as-sign DNF; (H1) is fulfilled since for all formulas, the signs do overlap. $\varPhi _2$ is not representable by a mvs-Hintikka set since (H1) is violated by $\{-2\}{:}b$ or $\{-2\}{:}c$ that are derived from $\{2\}{:}\boldsymbol{(} b \; before \; c \boldsymbol{)}$.

Lemma 2

Every temporal tableau expansion rule of Definition 12 corresponds to a temporal set-as-signs DNF representation for $S: \gamma (\phi _1,\ldots ,\phi _n)_{\mathcal {A}'}$.

Proof

By inspecting the expansion rules of Definition 12, we can see that they are already in the form of Definition 15. The sets-as-signs representation were computed directly from the coverage of the truth tables (as illustrated by Fig. 1), which is according to [10] an eligible method.

Thus, the formulas on an open branch in a temporal tableau $\mathfrak {T}$ for $(\varPi ,\mathcal {A})$ form a temporal mvs-Hintikka set and are satisfiable if each formula $S: \phi _{\mathcal {A}'}$ is evaluated with assignment $\mathcal {A}'$. However, each such $\mathcal {A}'$ is by construction the restriction of $\mathcal {A}$ to the literals relevant for $\phi$, i.e. $\mathcal {A}' = t_\mathcal {A}(\phi )$, and thus $\sigma _{\mathcal {A}'}(\phi ) = \sigma _{t_\mathcal {A}(\phi )}(\phi ) = \sigma _\mathcal {A}(\phi )$ holds for every truth assignment $\sigma$. Consequently,

Proposition 6

Every open branch $\theta$ in a temporal tableau $\mathfrak {T}$ for $(\varPi ,\mathcal {A})$ on which all possible rules have been applied, has a model and hence $\lnot \varPi$ is satisfiable under $\mathcal {A}$.

We then readily obtain the claimed completeness result for the temporal tableau calculus.

Theorem 2

(Completeness) If a temporal N₃ formula $\varPi$ is a tautology with the temporal assignment $\mathcal {A}$, then $(\varPi ,\mathcal {A})$ has a temporal tableau proof.

Proof

Towards a contradiction, suppose that $(\varPi ,\mathcal {A})$ has no temporal tableau proof. Hence no closed temporal tableau for $\{ \lnot \varPi \}$ and $\mathcal {A}$ exists, which implies that some temporal tableau $\mathfrak {T}$ for $\{ \lnot \varPi \}$ and $\mathcal {A}$ with an open branch $\theta$ exists on which all possible rules have been applied. By Proposition 6 $\lnot \varPi$ is satisfied by some truth value assignment $\sigma$, i.e., $\sigma (\lnot \varPi ) = 2$; hence $\sigma (\varPi )\ne 2$, which means $\varPi$ is not a tautology, which is a contradiction.    $\square$

5 Prototypical Implementation

As for the implementation of a tableau prover, it may be convenient to restrict the input formulas to a specific form. Well-known such forms are CNF, DNF, as well as negation normal form (NNF). For our concerns, we may consider a temporal version of CNF.

Definition 16

A temporal conjunctive normal form (CNF) in N₃, is a conjunction $\bigwedge _{i=1}^n C_i$ of clauses $C_i = L_{i_1} \vee ... \vee L_{i_{m}}$, where each $L_{i_j}$ is of the form $\alpha$, $\sim \alpha$, $\lnot \alpha$, $\lnot \lnot \alpha$, or $\lnot \!\!\sim \alpha$, where $\alpha$ is either an atom or an FTF formula. Temporal disjunctive normal form (DNF) in N₃ is defined dually as usual.

By means of equivalence preserving rewritings, every temporal formula in N₃ that we consider can be rewritten to temporal CNF (and similarly, to temporal DNF); indeed, Proposition 1 generalizes to the case where $\alpha$, $\beta$, and $\gamma$ can be FTFs. In addition, any FTF $\alpha \,\nu \, \beta$ can be due to the definition of $\tau _\mathcal {A}^*(\alpha \,\nu \, \beta )$ be rewritten into NNF (i.e. $\alpha$ and $\beta$ become NNF) by applying Proposition 1. We remark that a temporal CNF is infeasible for N₅ as there is no equivalence preserving rewriting for implications.

Implementation. We have implemented an initial temporal tableau solver in Python 3.7, which currently evaluates N₃-theories in temporal CNF. The solver is intended for prototyping and no optimization techniques of modern tableau solvers are implemented. It also includes a model generator, and outputs all models extracted from the open branches in a tableau. The implementation is available on https://github.com/patrik999/EL-TempTableau, and is used to evaluate the cased study.

Case Study. We recall the slightly modified theory $\varPi$ of Example 1 and the assignment $\mathcal {A}$ :

$$\begin{array}{r@{~}c@{~}l} \varPi &{}= &{} \{ \lnot a \vee b, \sim c, \boldsymbol{(} (a \wedge \sim c) \;( o )\; (o_1 \vee o_2) \boldsymbol{)} \vee \boldsymbol{(} (b \wedge c)\;( o )\; (o_1 \vee o_2) \boldsymbol{)}, o_1, o_2 \},\\ \mathcal {A} &{} = &{} \{(a, [1,4]), (b, \boldsymbol{u}), (c, [1,2] (\sim c, [3,5]), (o_1, [1,3]), ({o_2}, [3,5]) \}. \end{array}$$

The tableau tree for $\varPi$ is shown in Fig. 2b, where $\textsf{o}$ is short for $(\textsf{o})$ and the temporal assignments are for instance (all others are derivable accordingly): $\mathcal {A}_1 = \{(a,[1,4]),(b,\textbf{u}) \}$, $\mathcal {A}_{3,1,1} = \{(a,[3,4]),(\sim c,[3,4]) \}$, and $\mathcal {A}_{3,1,2} = \{(o_1,[1,5]),(o_2,[1,5]) \}$. For the two open branches, we can derive two models, where the temporal assignments can be seen in $\mathcal {A}_{3,1,1}$ and $\mathcal {A}_{3,1,2}$. Two branches were closed since the a temporal formula was evaluated over $(b,\textbf{u})$, thus the expansion rule for $E=0$ was applied. The leftmost branch was closed due to $\{-2\}{:}a$ and $\{2\}{:}a$ being on the same branch.

Fig. 2.

Tableau tree for (a) Example 4 on the left and (b) the case study on the right

6 Related Work and Conclusion

This work is inspired by Temporal Behavioral Models [5] and builds mainly on here-and-there (HT) logic [13] and Equilibrium Logic [17], with a tableau system for reasoning [16]. The syntax/semantics presented in [17] is extended with temporal assignments/relations, which then affect the extension of the tableau system of [16]. In a broader perspective, the work is related to tableau calculi for many-valued logics [7] and to nested expressions in logic programs [15], but neither of them considers the temporal setting. Qualitative temporal reasoning was introduced to ASP by Brenton et al. [4] and Janhunen and Sioutis [14], where the former encoded temporal relations in ASP directly while the latter presented a hybrid-approach based on an extension of ASP with difference logic. Both focused on a particular encoding in ASP but did not provide a novel semantics nor a respective tableau system. With Metric Temporal ASP [6] and DatalogMTL under stable models semantics [18], Cabalar et al. and Walega et al. respectively, extended HT and Equilibrium logic, defining metric linear time connectives such as always or until over finite respectively infinite traces. Our approach is different from them regarding (a) the language, which is in [18] and [6] restricted to rules, (b) the (qualitative) temporal relations of Allen’s Time Interval Algebra, and (c) the temporal annotation instead of trace-based valuation of time. Arias et al. [2] focused on goal-oriented top-down execution of Constraint ASP, which differs from our aim of model generation; in principle, one could encode intervals by fluents in this framework.

This work provides the initial step towards a framework for an abduction-based traffic diagnosis framework. Temporal behavior formulas (TBFs) [5] can be used in it to define relations between explanations and observations that take temporal constraints into account, where the constraints are based on Allen’s IA [1]. Since TBFs offer limited expressive means, we have introduced a novel language that allows for nesting of temporal formulas, where associated time intervals are coalesced, and temporal assignments can express undefined time instances. We provided for this language a semantics based on an extension of HT logic and Equilibrium logic [17]. For reasoning, we have extended the three-valued propositional tableau calculus for HT logic in [16] with temporal expansion rules and provided soundness and completeness results. Furthermore, we have implemented a proof-of-concept prototype and demonstrated it on a case study.

Outlook. The work on the new language and the temporal tableau system can be extended in several directions. One direction is to equip the tableau system with minimality checking of models in order to support Equilibrium logic semantics. Pearce et al. [16] considered for this the use of sub-tableaux. However, we believe that an approach to minimality checking akin to the modular one in [3], which uses a super-dependency graph derived from an atom-clause dependency graph, could be more attractive. In connection with this, alternative notions of minimal models may be considered that allow for differences in temporal assignments. Regarding syntactic extensions of the language, richer nesting in temporal formulas may be investigated, e.g., restricted or arbitrary use of weak negation or temporal formulas. This however would require redefining (undefined) time instances and coalescing. Another direction is refined temporal semantics, where undefinedness may be avoided in some cases (e.g., $(\alpha \, before \, \alpha )$ should always evaluate to false), or where literals are assigned with sets of intervals rather than a single interval. The current tableau system was designed for N₃, but it can be extended to N₅, moreover in combination with quantifiers. Finally, we aim to advance the proof-of-concept implementation of the prototype, using optimization techniques of tableau reasoners, and to evaluate an improved reasoner on benchmarks for temporal reasoning, e.g., on traffic flows [8].