Pedro Cabalar
email: cabalar@udc.es

Stéphane Demri
email: demri@lsv.ens-cachan.fr

Automata-based Computation of Temporal Equilibrium Models ⋆

Temporal Equilibrium Logic (TEL) is a formalism for temporal logic programming that generalizes the paradigm of Answer Set Programming (ASP) introducing modal temporal operators from standard Linear-time Temporal Logic (LTL). In this paper we solve some problems that remained open for TEL like decidability, bounds for computational complexity as well as computation of temporal equilibrium models for arbitrary theories. We propose a method for the latter that consists in building a Büchi automaton that accepts exactly the temporal equilibrium models of a given theory, providing an automata-based decision procedure and illustrating the ω-regularity of such sets. We show that TEL satisfiability can be solved in exponential space and it is hard for polynomial space. Finally, given two theories, we provide a decision procedure to check if they have the same temporal equilibrium models.

Introduction

Stable models. Stable models have their roots in Logic Programming and in the search for a semantical interpretation of default negation [START_REF] Gelfond | The stable model semantics for logic programming[END_REF] (or answer set semantics). They have given rise to a successful declarative paradigm, known as Answer Set Programming (ASP) [START_REF] Niemelä | Logic programs with stable model semantics as a constraint programming paradigm[END_REF][START_REF] Marek | Stable models and an alternative logic programming paradigm[END_REF], for practical knowledge representation. ASP has been applied to a wide spectrum of domains for solving several types of reasoning tasks: making diagnosis for the Space Shuttle [START_REF] Nogueira | An A-Prolog decision support system for the space shuttle[END_REF], information integration of different data sources [START_REF] Leone | Boosting information integration: The INFOMIX system[END_REF], distributing seaport employees in work teams [START_REF] Grasso | An ASP-based system for team-building in the Gioia-Tauro seaport[END_REF] or automated music composition [START_REF] Boenn | ANTON: Composing logic and logic composing[END_REF] to cite some examples. Some of these application scenarios frequently involve representing transition-based systems under linear time, so that discrete instants are identified with natural numbers. ASP offers interesting features for a formal treatment of temporal scenarios. For instance, it provides a high degree of elaboration tolerance [START_REF] Mccarthy | Elaboration tolerance[END_REF], allowing a simple and natural solution to typical representational issues such as the frame problem and the ramification problem, see respectively [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF] and [START_REF] Kautz | The logic of persistence[END_REF].

Another interesting feature is that it allows a uniform treatment of different kinds of reasoning problems such as prediction, postdiction, planning, diagnosis or verification. However, since ASP is not a temporal formalism, it also involves some difficulties for dealing with temporal problems. In particular, since most ASP tools must deal with finite domains, this additionally requires fixing a finite path length with an obvious impossibility for solving problems such as proving the non-existence of a plan for a given planning scenario, or checking whether two temporal representations are strongly equivalent (i.e., they are interchangeable inside any context and for any path length). Temporal Equilibrium Logic. To overcome these difficulties, in [START_REF] Aguado | Strongly equivalent temporal logic programs[END_REF] a temporal extension of ASP, called Temporal Equilibrium Logic (TEL), was considered. This extension is an orthogonal combination of linear-time temporal logic (LTL) (see e.g. [START_REF] Pnueli | The temporal logic of programs[END_REF]) with the nonmonotonic formalism of Equilibrium Logic [START_REF] Pearce | A new logical characterisation of stable models and answer sets[END_REF], probably the most general and best studied logical characterisation of ASP. TEL extends the stable model semantics to arbitrary LTL theories, that is, sets of formulae that combine atoms, the standard Boolean connectives, and the temporal operators X (read "next"), G (read "always"), F (read "eventually"), U (read "until") and R (read "release"). Towards arbitrary TEL theories. The definition of TEL has allowed studying problems like the aforementioned strong equivalence [START_REF] Aguado | Strongly equivalent temporal logic programs[END_REF] of two temporal theories, but it had mostly remained as a theoretical tool, since there was no method for computing the temporal stable models of a temporal theory, at least until quite recently. In a first step in this direction, the paper [START_REF] Aguado | Loop formulas for splitable temporal logic programs[END_REF] started from the normal form for TEL called temporal logic programs (TLPs) from [START_REF] Cabalar | A normal form for linear temporal equilibrium logic[END_REF] and showed that, when a syntactic subclass is considered (the so-called splitable TLPs), its temporal stable models can be obtained by a translation into LTL. This method has been implemented in a tool called STeLP [START_REF] Cabalar | STELP -a tool for temporal answer set programming[END_REF] that uses an LTL model checker as a backend and provides the temporal stable models of a splitable TLP in terms of a Büchi automaton. Although the splitable TLPs are expressive enough to capture most temporal scenarios treated in the ASP literature, a general method to compute the temporal equilibrium models for arbitrary TEL theories was not available until now. The interest for obtaining such a method is not only to cover the full expressiveness of this logic, but also to show its decidability and assess the complexity associated to its main reasoning tasks. In this sense, it is not convenient to use TLPs as a starting point since, despite of being a normal form for TEL, they are obtained by introducing new auxiliary atoms not present in the original propositional signature. Our contributions. In this paper we cover this gap and introduce an automatabased method to compute the temporal equilibrium models of an arbitrary temporal theory. We will pay a special attention to recall standard relationships between LTL and Büchi automata in order to facilitate the connection between ASP concepts and those from model-checking with temporal logics. More precisely, we propose automata-based decision procedures as follows:

1. We show that the satisfiability problem for the monotonic basis of TEL -the so-called logic of Temporal Here-and-There (THT) -can be solved in PSpace by translation into the satisfiability problem for LTL. Whence, any decision procedure for LTL (automata-based, tableaux-based, resolutionbased, etc.) can be used for THT. We are also able to demonstrate the PSpace-hardness of the problem. 2. For any temporal formula, we effectively build a Büchi automaton that accepts exactly its temporal equilibrium models which allows to provide an automata-based decision procedure. We are able to show that TEL satisfiability can be solved in ExpSpace and it is PSpace-hard. Filling the gap is part of future work. Hence, we provide a symbolic representation for sets of temporal equilibrium models raising from temporal formulae. 3. Consequently, given two theories, we provide a decision procedure to check whether they have the same temporal equilibrium models (that is, regular equivalence, as opposed to strong equivalence). 4. Our proof technique can indeed be adapted to any extension of LTL provided that formulae can be translated into Büchi automata (as happens with LTL with past or LTL with fixed-points operators).

Temporal Equilibrium Logic

Let AT = {p, q, . . .} be a countably infinite set of atoms. A temporal formula is defined with the formal grammar below:

ϕ ::= p | ⊥ | ϕ 1 ∧ ϕ 2 | ϕ 1 ∨ ϕ 2 | ϕ 1 → ϕ 2 | Xϕ | ϕ 1 U ϕ 2 | ϕ 1 R ϕ 2
where p ∈ AT. We will use the standard abbreviations:

¬ϕ def = ϕ →⊥ ⊤ def = ¬⊥ ϕ ↔ ϕ ′ def = (ϕ → ϕ ′ ) ∧ (ϕ ′ → ϕ) Gϕ def = ⊥ R ϕ Fϕ def = ⊤ U ϕ
The temporal connectives X, G, F, U and R have their standard meaning from LTL. A theory Γ is defined as a finite set of temporal formulae.

In the non-temporal case, Equilibrium Logic is defined by introducing a criterion for selecting models based on a non-classical monotonic formalism called the logic of Here-and-There (HT) [START_REF] Heyting | Die formalen Regeln der intuitionistischen Logik[END_REF], an intermediate logic between intuitionistic and classical propositional calculus. Similarly, TEL will be defined by first introducing a monotonic, intermediate version of LTL, we call the logic of Temporal Here-and-There (THT), and then defining a criterion for selecting models in order to obtain nonmonotonicity.

In this way, we will deal with two classes of models. An LTL model H is a map H : N → P(AT), viewed as an ω-sequence of propositional valuations. By contrast, the semantics of THT is defined in terms of sequences of pairs of propositional valuations, which can be also viewed as a pair of LTL models. A THT model is a pair M = (H, T) where H and T are LTL models and for i ≥ 0, we impose that H(i) ⊆ T(i). H(i) and T(i) are sets of atoms standing for here and there respectively. A THT model M = (H, T) is said to be total when H = T. The satisfaction relation |= is interpreted as follows on THT models (M is a THT model and k ∈ N):

1. M, k |= p def ⇔ p ∈ H(k). 2. M, k |= ϕ ∧ ϕ ′ def ⇔ M, k |= ϕ and M, k |= ϕ ′ . 3. M, k |= ϕ ∨ ϕ ′ def ⇔ M, k |= ϕ or M, k |= ϕ ′ . 4. M, k |= ϕ → ϕ ′ def ⇔ for all H ′ ∈ {H, T}, (H ′ , T), k |= ϕ or (H ′ , T), k |= ϕ ′ . 5. M, k |= Xϕ def ⇔ M, k + 1 |= ϕ. 6. M, k |= ϕU ϕ ′ def ⇔ there is j ≥ k such that M, j |= ϕ ′ and for all j ′ ∈ [k, j-1], M, j ′ |= ϕ. 7. M, k |= ϕR ϕ ′ def ⇔ for all j ≥ k such that M, j |= ϕ ′ , there exists j ′ ∈ [k, j-1], M, j ′ |= ϕ. 8. never M, k |=⊥.
A model for a theory Γ is a THT model M such that for every formula ϕ ∈ Γ , we have M,

0 |= ϕ. A formula ϕ is THT valid def ⇔ M, 0 |= ϕ for every THT model M. Similarly, a formula ϕ is THT satisfiable def ⇔ there is a THT model M such that M, 0 |= ϕ.
As we can see, the main difference with respect to LTL is the interpretation of implication (item 4), that must be checked in both components, H and T, of M. In fact, it is easy to see that when we take total models M = (T, T), THT satisfaction (T, T), k |= ϕ collapses to standard LTL satisfaction T, k |= ϕ. We write T, k |= ϕ instead of (T, T), k |= ϕ whenever convenient. For instance, item 4 in the above definition can be rewritten as:

4 ′ . M, k |= ϕ → ϕ ′ def ⇔ (M, k |= ϕ implies M, k |= ϕ ′ ) and T, k |= ϕ → ϕ ′ (LTL satisfaction) Note that M, k |= ¬p iff M, k |= p →⊥ iff (M, k |= p implies M, k |=⊥ and T, k |= p implies T, k |=⊥) iff (p ∈ H(k) and p ∈ T(k)).
Similarly, a formula ϕ is LTL valid def ⇔ M, 0 |= ϕ for every total THT model M whereas a formula ϕ is LTL satisfiable def ⇔ there is a total THT model M such that M, 0 |= ϕ. We write Mod(ϕ) to denote the set of LTL models for ϕ (restricted to the set of atoms occurring ϕ denoted by AT(ϕ)).

Obviously, any THT valid formula is also LTL valid, but not the other way around. For instance, the following are THT valid equivalences:

¬(ϕ ∧ ψ) ↔ ¬ϕ ∨ ¬ψ ¬(ϕ ∨ ψ) ↔ ¬ϕ ∧ ¬ψ X(ϕ ⊕ ψ) ↔ Xϕ ⊕ Xψ X ⊗ ϕ ↔ ⊗Xϕ
for any binary connective ⊕ and any unary connective ⊗. This means that De Morgan laws are valid, and that we can always shift the X operator to all the operands of any connective. On the contrary, the LTL valid formula ϕ ∨ ¬ϕ (known as excluded middle axiom) is not THT valid. This is inherited from the intermediate/intuitionistic nature of THT: in fact, the addition of this axiom makes THT collapse into LTL. By adding a copy of this axiom for any atom at any position of the models, we can force that THT models of any formula are total, as stated next.

Proposition 1. Given a temporal formula ϕ built over the propositional atoms in AT(ϕ), for every THT model (H, T), the propositions below are equivalent:

(I) (H, T), 0 |= ϕ ∧ p∈AT(ϕ) G(p ∨ ¬p), (II) T, 0 |= ϕ in LTL, and for i ≥ 0 and p ∈ AT(ϕ), we have p ∈ H(i) iff p ∈ T(i).
As a consequence, we can easily encode LTL in THT, since LTL models of ϕ coincide with its total THT models. Let us state another property whose proof can be obtained by structural induction.

Proposition 2 (Persistence). For any formula ϕ, any THT model M = (H, T) and

any i ≥ 0, if M, i |= ϕ, then T, i |= ϕ. Corollary 1. (H, T), i |= ¬ϕ iff T, i |= ϕ in LTL.
We proceed now to define an ordering relation among THT models, so that only the minimal ones will be selected for a temporal theory. Given two LTL models H and H ′ , we say that H is less than or equal to

H ′ (in symbols H ≤ H ′ ) def ⇔ for k ≥ 0, we have H(k) ⊆ H ′ (k). We write H < H ′ if H ≤ H ′ and H = H ′ .
The relations ≤ and < can be lifted at the level of THT models. Given two THT models M = (H, T) and

M ′ = (H ′ , T ′ ), M ≤ M ′ def ⇔ H ≤ H ′ and T = T ′ . Similarly, we write M < M ′ if M ≤ M ′ and M = M ′ .

Definition 1 (Temporal Equilibrium Model).

A THT model M is a temporal equilibrium model (or TEL model, for short) of a theory Γ if M is a total model of Γ and there is no

M ′ < M such that M ′ , 0 |= Γ .
Temporal Equilibrium Logic (TEL) is the logic induced by temporal equilibrium models and it is worth noting that any temporal equilibrium model of Γ is a total THT model of the form (T, T) (by definition). The corresponding LTL model T of Γ is said to be a temporal stable model of Γ .

When we restrict the syntax to non-modal theories and semantics to HT interpretations H(0), T(0) we talk about (non-temporal) equilibrium models, which coincide with stable models in their most general definition [START_REF] Ferraris | Answer sets for propositional theories[END_REF].

The TEL satisfiability problem consists in determining whether a temporal formula has a TEL model. As an example, consider the formula

G(¬p → Xp) (1)
Its intuitive meaning corresponds to the logic program consisting of rules of the form: p(s(X)) ← not p(X) where time has been reified as an extra parameter X = 0, s(0), s(s(0)), . . . . Notice that the interpretation of ¬ is that of default negation not in logic programming. In this way, (1) is saying that, at any situation i ≥ 0, if there is no evidence on p, then p will become true in the next state i + 1. In the initial state, we have no evidence on p, so this will imply Xp. As a result XXp will have no applicable rule and thus will be false by default, and so on. It is easy to see that the unique temporal stable model of ( 1) is defined by the formula ¬p ∧ G(¬p ↔ Xp).

It is worth noting that an LTL satisfiable formula may have no temporal stable model. As a simple example (well-known from non-temporal ASP) the logic program rule ¬p → p, whose only (classical) model is {p}, has no stable models. This is because if we take a model M = (H, T) where p holds in T, then (Corollary 1) M |= ¬p and so M |= ¬p → p true regardless H, so we can take a strictly smaller H < T whose only difference with respect to T is that p does not hold. On the other hand, if we take any T in which p does not hold, then M |= ¬p and so ¬p → p would make p true both in H and T reaching a contradiction. When dealing with logic programs, it is well-known that nonexistence of stable models is always due to a kind of cyclic dependence on default negation like this.

In the temporal case, however, non-existence of temporal stable models may also be due to a lack of a finite justification for satisfying the criterion of minimal knowledge. As an example, take the formula GFp, typically used in LTL to assert that property p occurs infinitely often. This formula has no temporal stable models: all models must contain infinite occurrences of p and there is no way to establish a minimal H among them. Thus, formula GFp is LTL satisfiable but it has no temporal stable model. By contrast, forthcoming Proposition 4 states that for a large class of temporal formulae, LTL satisfiability is equivalent to THT satisfiability and TEL satisfiability.

Automata-Based Approach for LTL in a Nutshell

Before presenting our decision procedures, let us briefly recall what are the main ingredients of the automata-based approach. It consists in reducing logical problems into automata-based decision problems in order to take advantage of known results from automata theory. The most standard target problems on automata used in this approach are the nonemptiness problem (checking whether an automaton admits at least one accepting computation) and the inclusion problem (checking whether the language accepted by the automaton A is included in the language accepted by the automaton B). In a pioneering work [4] Büchi introduced a class of automata showing that they are equivalent to formulae in monadic second-order logic (MSO) over (N, <).

In full generality, here are a few desirable properties of the approach. The reduction should be conceptually simple, see the translation from LTL formulae into alternating automata [START_REF] Vardi | Alternating automata: unifying truth and validity checking for temporal logics[END_REF]. Formula structure is reflected directly in the transition formulae of alternating automata. The computational complexity of the automata-based target problem should be well-characterized -see, for instance, the translation from PDL formulae into nondeterministic Büchi tree automata [START_REF] Vardi | Automata-theoretic techniques for modal logics of programs[END_REF]. It is also highly desirable that not only the reduction is conceptually simple but also that it is semantically faithful so that the automata involve in the target instance are closely related to the instance of the original logical problem. Last but not least, preferrably, the reduction might allow to obtain the optimal complexity for the source logical problem.

Basics on Büchi automata

We recall that a Büchi automaton A is a tuple

A = (Σ, Q, Q 0 , δ, F ) such that Σ is a finite alphabet, Q is a finite set of states, Q 0 ⊆ Q is the set of initial states, the transition relation δ is a subset of Q × Σ × Q and F ⊆ Q is a set of final states.
Given q ∈ Q and a ∈ Σ, we also write δ(q, a) to denote the set of states q ′ such that (q, a, q ′ ) ∈ δ.

A run ρ of A is a sequence q 0 a0 -→ q 1 a1 -→ q 2 . . . such that for every i ≥ 0, (q i , a i , q i+1 ) ∈ δ (also written q i ai -→ q i+1 ). The run ρ is accepting if q 0 ∈ Q 0 is initial and some state of F is repeated infinitely often in ρ: inf(ρ) ∩ F = ∅ where we let inf(ρ) = {q ∈ Q : ∀ i, ∃ j > i, q = q j }. The label of ρ is the word σ = a 0 a 1 • • • ∈ Σ ω . The automaton A accepts the language L(A) of ω-words σ ∈ Σ ω such that there exists an accepting run of A on the word σ, i.e., with label σ. Now, we introduce a standard generalization of the Büchi acceptance condition by considering conjunctions of classical Büchi conditions. A generalized Büchi automaton (GBA) is a structure A = (Σ, Q, Q 0 , δ, {F 1 , . . . , F k }) such that F 1 , . . . , F k ⊆ Q and Σ, Q, Q 0 and δ are defined as for Büchi automata. A run is defined as for Büchi automata and a run ρ of A is accepting iff the first state is initial and for i ∈ [1, n], we have inf(ρ) ∩ F i = ∅. It is known that every GBA A can be easily translated in logarithmic space into a Büchi automaton, preserving the language of accepted ω-words (see e.g. [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]). Moreover, the nonemptiness problem for GBA or BA is known to be NLogSpace-complete.

From LTL formulae to Büchi automata

We recall below how to define a Büchi automaton that accepts the linear models of an LTL formula. Given an LTL formula ϕ, we define its closure cl(ϕ) to denote a finite set of formulae that are relevant to check the satisfiability of ϕ. For each LTL formula ϕ, we define its main components (if any) according to the table below:

formula ϕ main components p or ¬p none ¬¬ψ or Xψ ψ ¬Xψ ¬ψ ψ1U ψ2 or ψ1 ∧ ψ2 or ψ1R ψ2 ψ1, ψ2 ¬(ψ1U ψ2) or ¬(ψ1 ∧ ψ2) or ¬(ψ1R ψ2) ¬ψ1, ¬ψ2
We write cl(ϕ) to denote the least set of formulae such that ϕ ∈ cl(ϕ) and cl(ϕ) is closed under main components. It is routine to check that card(cl(ϕ)) ≤ |ϕ| (the size of ϕ). Moreover, one can observe that if ψ ∈ cl(ϕ), then for each immediate subformula (if any), either it belongs to cl(ϕ) or its negation belongs to cl(ϕ). A subset Γ ⊆ cl(ϕ) is consistent and fully expanded whenever

-ψ 1 ∧ ψ 2 ∈ Γ implies ψ 1 , ψ 2 ∈ Γ , -¬(ψ 1 ∧ ψ 2 ) ∈ Γ implies ¬ψ 1 ∈ Γ or ¬ψ 2 ∈ Γ , -¬¬ψ ∈ Γ implies ψ ∈ Γ , -Γ
does not contain a contradictory pair ψ and ¬ψ.

The pair of consistent and fully expanded sets

(Γ 1 , Γ 2 ) is one-step consistent def ⇔ 1. Xψ ∈ Γ 1 implies ψ ∈ Γ 2 and ¬Xψ ∈ Γ 1 implies ¬ψ ∈ Γ 2 . 2. ψ 1 U ψ 2 ∈ Γ 1 implies ψ 2 ∈ Γ 1 or (ψ 1 ∈ Γ 1 and ψ 1 U ψ 2 ∈ Γ 2 ), 3. ¬(ψ 1 U ψ 2 ) ∈ Γ 1 implies ¬ψ 2 ∈ Γ 1 and (¬ψ 1 ∈ Γ 1 or ¬(ψ 1 U ψ 2 ) ∈ Γ 2 ). 4. ψ 1 R ψ 2 ∈ Γ 1 implies ψ 2 ∈ Γ 1 and (ψ 1 ∈ Γ 1 or ψ 1 R ψ 2 ∈ Γ 2 ), 5. ¬(ψ 1 R ψ 2 ) ∈ Γ 1 implies ¬ψ 2 ∈ Γ 1 or (¬ψ 1 ∈ Γ 1 and ¬(ψ 1 R ψ 2 ) ∈ Γ 2 ).
Given an LTL formula ϕ, let us build the generalized Büchi automaton A ϕ = (Σ, Q, Q 0 , δ, {F 1 , . . . , F k }) where -Σ = P(AT(ϕ)) and Q is the set of consistent and fully expanded sets.

-Q 0 = {Γ ∈ Q : ϕ ∈ Γ }. -Γ a -→ Γ ′ ∈ δ def ⇔ (Γ, Γ ′ ) is one-step consistent, (Γ ∩ AT(ϕ)) ⊆ a and {p : ¬p ∈ Γ } ∩ a = ∅. -If the temporal operator U does not occur in ϕ, then F 1 = Q and k = 1.
Otherwise, suppose that

{ψ 1 U ψ ′ 1 , . . . , ψ k U ψ ′ k } is the set of U -formulae from cl(ϕ). Then, for every i ∈ [1, k], F i = {Γ ∈ Q : ψ i U ψ ′ i ∈ Γ or ψ ′ i ∈ Γ }.
It is worth observing that card(Q) ≤ 2 |ϕ| and A ϕ can be built in exponential time in |ϕ|. Figure 1 presents a Büchi automaton recognizing the models for G(¬p → Xp) over the alphabet {∅, {p}}. The automaton obtained from the above systematic construction would be a bit larger since cl(G(¬p → Xp)) has about 2 4 subsets. However, the systematic construction has the advantage to be generic. Other translations exist with other advantages, for instance to build small automata, see e.g. [START_REF] Demri | Specification and verification using temporal logics[END_REF]. However, herein, we need to use the following properties (apart from the correctness of the reduction): (1) the size of each state of A ϕ is linear in the size of ϕ, (2) it can be checked if a state is initial [resp. final] in linear space in the size of ϕ and (3) given two subsets X, X ′ of cl(ϕ) and a ∈ Σ, one can check in linear space in the size of ϕ whether X a -→ X ′ is a transition of A ϕ (each transition of A ϕ can be checked in linear space in the size of ϕ).

Proposition 3. [29] Mod(ϕ) = L(A ϕ ), i.e. for every a 0 a 1 • • • ∈ Σ ω , a 0 a 1 • • • ∈ L(A ϕ ) iff T, 0 |= ϕ where for all i ∈ N, T(i) = a i .
These are key points towards the PSpace upper bound for LTL satisfiability since the properties above are sufficient to check the nonemptiness of A ϕ in nondeterministic polynomial space in the size of ϕ (guess on-the-fly a prefix and a loop of length at most exponential) and then invoke Savitch Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF] to eliminate nondeterminism. We will use similar arguments to establish that TEL satisfiability can be solved in ExpSpace.

Building TEL Models with Büchi Automata

In this section, we provide an automata-based approach to determine whether a formula ϕ built over the atoms {p 1 , . . . , p n } has a TEL model. This is the place where starts our main contribution. To do so, we build a Büchi automaton B over the alphabet Σ = P({p 1 , . . . , p n }) such that L(B) is equal to the set of TEL models for ϕ. Moreover, nonemptiness can be checked in ExpSpace, which allows to answer the open problem about the complexity of determining whether a temporal formula has a TEL model.

Each model M = H, T restricted to the atoms in {p 1 , . . . , p n } can be encoded into an LTL model H ′ over the alphabet Σ ′ = P({p 1 , . . . , p n , p ′ 1 , . . . , p ′ n }) such that for i ≥ 0, H ′ (i) = (T(i) ∩ {p 1 , . . . , p n }) ∪ {p ′ j : p j ∈ H(i), j ∈ [1, n]}. In that case, we write H ′ ≈ M. Lemma 1.

(I) For every THT model M = H, T restricted to atoms in {p 1 , . . . , p n }, there is a unique LTL model

H ′ such that H ′ ≈ M. (II) For every LTL model H ′ : N → Σ ′ such that H ′ , 0 |= i∈[1,n] G(p ′ i → p i ), there is a unique THT model M = H, T restricted to atoms s.t. H ′ ≈ M.
In (II), a THT model M can be built thanks to the satisfaction of the formula i∈ [1,n] G(p ′ i → p i ) by H ′ , which guarantees that for all i ∈ N, we have H(i) ⊆ T(i). The proof is by an easy verification. This guarantees a clear isomorphism between two sets of models. In order to complete this model-theoretical correspondence, let us define the translation f between temporal formulae:

f is homomorphic for conjunction, disjunction and temporal operators,

-f (⊥) def =⊥, f (p i ) def = p ′ i and f (ψ → ψ ′ ) def = (ψ → ψ ′ ) ∧ (f (ψ) → f (ψ ′ )).
Lemma 2. Let ϕ be a temporal formula built over the atoms in {p 1 , . . . , p n } and M restricted to {p 1 , . . . , p n } and H ′ be models such that H ′ ≈ M. For l ≥ 0, we have

H ′ , l |= f (ψ) iff M, l |= ψ for every subformula ψ of ϕ.
The proof is by an easy structural induction. So, there is a polynomialtime reduction from THT satisfiability into LTL satisfiability by considering the mapping f (•) ∧ i∈ [1,n] G(p ′ i → p i ). Let A 1 be the Büchi automaton such that L(A 1 ) = Mod(ϕ), following any construction similar to [START_REF] Vardi | Reasoning about infinite computations[END_REF] (see Section 3.2). The set L(A 1 ) can be viewed as the set of total THT models of ϕ. Let ϕ ′ be the formula

f (ϕ) ∧ i∈[1,n] G(p ′ i → p i ).
Lemma 3. The set of LTL models for the formula ϕ ′ corresponds to the set of THT models for the temporal formula ϕ.

For instance, taking the formula ϕ = G(¬p → Xp), we can compute its THT models M by obtaining the corresponding LTL models (with atoms p and p ′ ) for the formula below:

ϕ ′ = f ( G(¬p → Xp) ) ∧ G(p ′ → p) = G (¬p → Xp) ∧ (¬p ∧ ¬p ′ → Xp ′ ) ∧ G(p ′ → p)
Figure 2 presents a Büchi automaton for the models of the formula f (G(¬p → Xp)) ∧ G(p ′ → p) over the alphabet {∅, {p}, {p ′ }, {p, p ′ }}. Hence, we provide a symbolic representation for the THT models of G(¬p → Xp). For instance, reading the letter {p} at position i corresponds to a pair (H(i), T(i)) with p ∈ H(i) and p ∈ T(i). Similarly, reading the letter {p, p ′ } at position i corresponds to a pair (H(i), T(i)) with p ∈ H(i) and p ∈ T(i). However, {p ′ } cannot be read since

H(i) ⊆ T(i). {p}, {p, p ′ } ∅ {p, p ′ } Fig. 2. Büchi automaton for models of f (G(¬p → Xp)) ∧ G(p ′ → p)
Hence, ϕ is THT satisfiable iff ϕ ′ is LTL satisfiable. The map f shall be also useful to show Proposition 4 below, becoming a key step to obtain PSpace-hardness results (see e.g. Theorem 2). Proposition 4 below states that for a large class of formulae, LTL satisfiability is equivalent to TEL satisfiability. Proposition 4. Let ϕ be temporal formula built over the connectives ∨, ∧, →, X and U and such that → occurs only in subformulae of the form p →⊥ with p ∈ AT. The propositions below are equivalent: (I) ϕ is LTL satisfiable; (II) ϕ is THT satisfiable; (III) ϕ has a temporal stable model, i.e. ϕ is TEL satisfiable.

Proof. Let L + (∨, ∧, X, U ) be the class of temporal formulae involved in the statement. Every temporal formula ϕ in L + (∨, ∧, X, U ) states a guarantee property in the sense of [START_REF] Černá | Relating hierarchy of linear temporal properties to model checking[END_REF] (see also [START_REF] Manna | A hierarchy of temporal properties[END_REF]). In particular, this means that (P1) if T, 0 |= ϕ in the LTL sense, then there is N ≥ 0 such that for any T ′ that only agrees with T on the positions in [0, N ], we also have T ′ , 0 |= ϕ (ϕ states a guarantee property).

In particular, we can impose that for l > N , we have T ′ (l) = ∅. Moreover, since the set of sequences of length N + 1 indexed by subsets of atoms occurring in ϕ is finite, if ϕ is LTL satisfiable, then there is an LTL model T such that T, 0 |= ϕ and no T ′ < T verifies T ′ , 0 |= ϕ (this property does not hold for every LTL formulae, consider GFp). Suppose that ϕ is LTL satisfiable. From the previous properties, we have seen that there is a minimal LTL model T such that T, 0 |= ϕ. The argument is by reductio ad absurdum. Suppose that there is H < T such that (H, T), 0 |= ϕ. By minimality of T, we have H, 0 |= ϕ. Since T is minimal and has an infinite suffix of the form ∅ ω , there is a finite amount of positions l 1 , . . . , l N such that H(l i ) ⊂ T(l i ) (strict inclusion).

Let H ′ be the LTL model such that H ′ ≈ (H, T). We have seen that H ′ , 0 |= f (ϕ) (Lemma 2). Let us define the map f ′ , that we shall apply to ϕ, as a slight variant of f :

f ′ is homomorphic for conjunction, disjunction and temporal operators,

-f ′ (p i ) def = (p ′ i ∧ p i ) and f ′ (¬p i ) def = (¬p i ∧ ¬p ′ i ). Since, H ′ , 0 |= i∈[1,n] G(p ′ i → p i ), we also have H ′ , 0 |= f ′ (ϕ)
. Let H ′′ be the variant of H ′ such that for l ∈ {l 1 , . . . , l N }, H ′′ (l) def = H ′ (l) and for i ∈ [1, N ] and p ∈ AT, if p ∈ H(l i ) and p ∈ T(l i ), then p, p ′ ∈ H ′′ (l i ), otherwise (p, p ′ ∈ H ′′ (l i ) def ⇔ p ∈ T(l i )). Observe that in H ′′ the valuations on {p 1 , . . . , p n } and {p ′ 1 , . . . , p ′ n } agree and the 'atomic' formulae in f ′ (ϕ) are the form either (p ′ i ∧p i ) or (¬p ′ i ∧ ¬p i ). Consequently, H ′′ , 0 |= f ′ (ϕ) and by Lemma 2, T ′ , 0 |= ϕ where T ′ (l) = H ′′ (l) ∩ {p 1 , . . . , p n } for l ≥ 0. By construction of T ′ , we have T ′ < T, which leads to a contradiction. Hence, (T, T) is a temporal stable model for ϕ.

⊓ ⊔ Corollary 2. THT satisfiability problem is PSpace-complete.

Proof. The translation f requires only polynomial-time and since LTL satisfiability is PSpace-complete [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF], we get that THT satisfiability is in PSpace. It remains to show the PSpace lower bound.

To do so, we can just observe that, as proved by Proposition 1, LTL satisfiability (which is PSpace-complete) can be encoded into THT satisfiability using the translation from Proposition 1, which can be performed in linear time. Indeed, it just adds a formula G(p ∨ ¬p) per each atom p ∈ AT.

⊓ ⊔

We can strengthen the mapping ϕ ′ to obtain not only THT models of ϕ but also to constrain them to be strictly non-total (that is H < T) as follows

ϕ ′′ def = ϕ ′ ∧ i∈[1,n] F((p ′ i →⊥) ∧ p i )
ϕ ′′ characterizes the non-total THT models of the formula ϕ. The generalized disjunction ensures that at some position j, H(j) ⊂ T(j) (strict inclusion).

Lemma 4. The set of LTL models for the formula ϕ ′′ corresponds to the set of non-total THT models for the temporal formula ϕ.

The proof is again by structural induction. Let A 2 be the Büchi automaton such that L(A 2 ) = Mod(ϕ ′′ ), following again any construction similar to [START_REF] Vardi | Reasoning about infinite computations[END_REF] (see Section 3.2). L(A 2 ) contains exactly the non-total THT models of ϕ.

Let h : Σ ′ → Σ be a map (renaming) between the two finite alphabets such that h(a) = a ∩ {p 1 , . . . , p n }. h consists in erasing the atoms from {p ′ 1 , . . . , p ′ n } h can be naturally extended as an homomorphism between finite words, infinite words and as a map between languages. Similary, given a Büchi automaton

A 2 = (Σ ′ , Q, Q 0 , δ, F ), we write h(A 2 ) to denote the Büchi automaton (Σ, Q, Q 0 , δ ′ , F ) such that q a -→ q ′ ∈ δ ′ def ⇔ there is b ∈ Σ ′ such that q b -→ q ′ ∈ δ and h(b) = a. Obviously, L(h(A 2 )) = h(L(A 2 )
). Indeed, the following propositions imply each other:

1. a 0 a 1 • • • ∈ L(A 2 ), 2. h(a 0 )h(a 1 ) • • • ∈ h(L(A 2 )) (by definition of h on languages), 3. h(a 0 )h(a 1 ) • • • ∈ L(h(A 2 )) (by definition of h on A 2 ).
The inclusion L(h(A 2 )) ⊆ h(L(A 2 )) can be shown in a similar way. So, L(h(A 2 )) can be viewed as the set of total THT models for ϕ having a strictly smaller THT model. We have seen that L(A 1 ) contains exactly the LTL models of ϕ, i.e. the total THT models satisfying ϕ. For taking care of condition (2.), by construction, A 2 accepts the non-total THT models for ϕ whereas L(h(A 2 )) contains the total THT models for ϕ having a strictly smaller THT model satisfying ϕ, the negation of (2.). Hence, (T, T) is a TEL model for ϕ iff T ∈ L(A 1 ) and T ∈ L(h(A 2 )). ⊓ ⊔ Hence, the set of TEL models for a given ϕ forms an ω-regular language. Proposition 6. For each temporal formula ϕ, one can effectively build a Büchi automaton that accepts exactly the TEL models for ϕ.

Proof. The class of languages recognized by Büchi automata (the class of ωregular languages) is effectively closed under union, intersection and complementation. Moreover, it is obviously closed under the renaming operation. Since A 1 , A 2 , and h(A 2 ) are Büchi automata, one can build a Büchi automaton A ′ such that L(A ′ ) = Σ ω \ L(h(A 2 )). Similarly, one can effectively build a Büchi automaton B ϕ such that L(B ϕ ) = L(A 1 ) ∩ L(A ′ ). Complementation can be performed using the constructions in [START_REF] Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF] or in [START_REF] Safra | Complexity of Automata on Infinite Objects[END_REF] (if optimality is required). Roughly speaking, complementation induces an exponential blow-up.

⊓ ⊔ Proof. Let ϕ be a temporal formula and A 1 and A 2 be Büchi automata such that L(A 1 ) ∩ (Σ ω \ L(h(A 2 ))) accepts exactly the TEL models for ϕ. We shall show that nonemptiness of the language can be tested in exponential space. With the construction of A 1 using [START_REF] Vardi | Reasoning about infinite computations[END_REF], we have seen that

We have introduced an automata-based method for computing the temporal equilibrium models of an arbitrary temporal theory, under the syntax of Lineartime Temporal Logic (LTL). This construction has allowed us solving several open problems about Temporal Equilibrium Logic (TEL) and its monotonic basis Temporal Here-and-There (THT). In particular, we were able to prove that THT satisfiability can be solved in PSpace and is PSpace-hard whereas TEL satisfiability is decidable (something not proven before) being solvable in ExpSpace and at least PSpace-hard (filling the gap is part of future work). Our method consists in constructing a Büchi automaton that captures all the temporal equilibrium models of an arbitrary theory. This also implies that the set of TEL models of any theory is ω-regular.

A recent approach [START_REF] Aguado | Loop formulas for splitable temporal logic programs[END_REF][START_REF] Cabalar | STELP -a tool for temporal answer set programming[END_REF] has developed a tool, called STeLP, that also captures TEL models of a theory in terms of a Büchi automaton. Our current proposal, however, has some important advantages. First, STeLP restricts the input syntax to so-called splitable temporal logic programs, a strict subclass of a normal form for TEL that further requires the introduction of auxiliary atoms for removing U and R operators, using a structure preserving transformation. On the contrary, our current method has no syntactic restrictions and directly works on the alphabet of the original theory, for which no transformation is required prior to the automaton construction. Second, once the STeLP input is written in the accepted syntax, it translates the input program into LTL by the addition of a set of formulae (the so-called loop formulae) whose number is, in the worst case, exponential on the size of the input. Future work includes the implementation of our current method as well a comparison in terms of efficiency with respect to the tool STeLP.

Fig. 1 .

 1 Fig. 1. Büchi automaton for models of G(¬p → Xp) (over the alphabet {∅, {p}})

  (II) implies (I) is by Proposition 2 and (III) implies (II) is by definition of temporal stable model whereas (III) implies (I) is by definition of LTL satisfiability. It remains to show that (I) implies (III).

Proposition 5 .

 5 ϕ has a TEL model iff L(A 1 ) ∩ (Σ ω \ L(h(A 2 ))) = ∅.Proof. A TEL model M = (H, T) for ϕ satisfies the following properties:1. M, 0 |= ϕ and H = T. 2. For no H ′ < H, we have (H ′ , T), 0 |= ϕ.

Figure 3 Fig. 3 .Proposition 7 .

 337 Figure 3 presents a Büchi automaton accepting the (unique) temporal equilibrium model for ϕ. The next step consists in showing that the nonemptiness check can be done in exponential space. ∅ {p} Fig. 3. Büchi automaton for stable models of G(¬p → Xp)

⋆ This research was partially supported by Spanish MEC project TIN2009-14562-C05-04 and Xunta de Galicia project INCITE08-PXIB105159PR.

stored and this requires exponential space. Similarly, counting until a double exponential value requires only an exponential amount of bits. Details are omitted but the very algorithm is based on standard arguments for checking on-the-fly graph accessibility and checking nonemptiness of the intersection of two languages accepted by Büchi automata (similar arguments are used in [START_REF] Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF]Lemma 2.10]). By Savitch Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], nondeterminism can be eliminated, providing the promised ExpSpace upper bound.

⊓ ⊔ Theorem 1. Checking whether a formula has a TEL model is PSpace-hard.

Proof. We can use again the linear encoding in Proposition 1 and observe that any THT model (T, T) of ψ = ϕ ∧ p∈AT(ϕ) G(p ∨ ¬p) will also be a TEL model of ϕ, since there are no non-total models for ψ and thus (T, T) will always be minimal. But then

Thus LTL satisfiability can be reduced to TEL satisfiability and so the latter problem is PSpace-hard. ⊓ ⊔ Theorem 2. Checking whether two temporal formulae have the same TEL models is decidable in ExpSpace and it is PSpace-hard.

Proof. Let ϕ ∈ L + (∨, ∧, X, U ) and ψ = GFp 1 . We recall that ψ has no temporal equilibrium model. The propositions below are equivalent: (a) ϕ is LTL satisfiable, (b) ϕ has a temporal equilibrium model and (c) ϕ and ψ have distinct sets of temporal equilibrium models. Since LTL satisfiability for the fragment L + (∨, ∧, X, U ) is PSpace-hard, coPSpace= PSpace and ((a) iff (c)), then the equivalence problem with temporal equilibrium models is PSpace-hard.

Let ϕ and ψ be two temporal formulae built over the same set of atoms and

)) recognizes the temporal equilibrium models for ϕ and L(A ψ 1 ) ∩ (Σ ω \ L(h(A ψ 2 ))) recognizes the temporal equilibrium models for ψ. So, ϕ and ψ have distinct sets of temporal equilibrium models iff one of the sets below is non-empty.

)). A nondeterministic algorithm running in exponential space is designed as follows:

1. Guess which sets among (I)-(IV) is tested for nonemptiness. 2. Run a nondeterministic algorithm in exponential space by synchronizing the transitions of the three automata (one or two of them are designed by complementation) as done in the proof of Proposition 7.

Again, elimination of nondeterminism can be performed thanks to Savitch Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF]. So, non equivalence problem is in ExpSpace. Since coExpSpace= ExpSpace (simply because ExpSpace refers to a deterministic class of Turing machines), the equivalence problem is in ExpSpace. ⊓ ⊔


Stéphane Demri

Complexity of Simple Dependent Bimodal Logics

come


Stéphane Demri

Jaroslaw Stepaniuk

Computational Complexity of Multimodal Logics Based on Rough Sets

R

Lower Approximation

Upper Approximation


On the Complexity of Extending Ground Resolution with Symmetry Rules


Stéphane Demri
email: demri@imag.fr

Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?

We define sequent-style calculi for nominal tense logics characterized by classes of modal frames that are first-order definable by certain ⇧ 0 1 -formulae and ⇧ 0 2 -formulae. The calculi are based on d'Agostino and Mondadori's calculus KE and therefore they admit a restricted cutrule that is not eliminable. A nice computational property of the restriction is, for instance, that at any stage of the proof, only a finite number of potential cut-formulae needs to be taken under consideration. Although restrictions on the proof search (preserving completeness) are given in the paper and most of them are theoretically appealing, the use of those calculi for mechanization is however doubtful. Indeed, we present sequent calculi for fragments of classical logic that are syntactic variants of the sequent calculi for the nominal tense logics.

Introduction

Background. The nominal tense logics are extensions of Prior tense logics (see e.g. [START_REF] Prior | Time and Modality[END_REF][START_REF] Rescher | Temporal Logic[END_REF]) by adding nominals (also called names) to the language (see e.g. [START_REF] Blackburn | Nominal tense logic[END_REF]). Nominals are understood as atomic propositions that hold true in a unique world of the Kripke-style models. The nominal tense logics are quite expressive since not only do they extend the standard (mono)modal logics by adding a past operator (giving the tense flavour) but they also admit nominals in the language. In spite of the analogy between nominals (in the object language of the logic) and prefixes, also called labels, used in various proof systems for modal logics (see e.g. [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF][START_REF] Wallen | Automated Deduction in Nonclassical Logics[END_REF]), no proof systems for nominal tense logics using this conceptual similarity exist. This is all the more surprising because during the last years, prefixed calculi have regained some interest (see e.g. [START_REF] Ognjanović | A tableau-like proof procedure for normal modal logics[END_REF][START_REF] Massacci | Strongly analytic tableaux for normal modal logics[END_REF][START_REF] Governatori | Labelled tableaux for multi-modal logics[END_REF][START_REF] Russo | Modal logics as labelled deductive systems[END_REF][START_REF] Gabbay | Labelled Deductive Systems[END_REF][START_REF] Basin | Labelled propositional modal logics: Theory and practice[END_REF][START_REF] Beckert | Free variable tableaux for propositional modal logics[END_REF]).

Although designing general frameworks defining proof systems for modal logics is a fundamental task, other works deal with the di cult problem of improving significantly the mechanization of logics by finding refined properties, mostly proof-theoretical, that provide better complexity bounds or that allow the design of e cient decision procedures (see e.g. [START_REF] Hudelmaier | Improved decision procedures for the modal logics K, KT and S4[END_REF][START_REF] Ganzinger | A resolutionbased decision procedure for extensions of K4[END_REF][START_REF] Heuerding | Sequent Calculi for Proof Search in Some Modal Logics[END_REF]). We claim that the latter approach is the most promising for mechanization. As witness, the present paper illustrates that for many nominal tense logics, it is not so di cult to find a general framework for mechanization as long as only qualitative properties (soundness, completeness, . . . ) are investigated. Our contribution. For any nominal tense logic L from the class C ⇧ 0 2 defined in this paper, we define a sequent-style calculus, say GL, that is based on the sequent-style counterpart of the calculus KE defined in [dM94]. Our calculi admit a cut rule satisfying the following nice computational properties. When reading the proof upwards, at any stage of the construction of the proof, (CR1) the number of potential cut-formulae is linear in the size of the part of the proof constructed so far; (CR2) any potential cut-formula can be computed in linear-time in the size of the part of the proof constructed so far. (CR3) the size of any potential cut-formula is linear in the size of the part of the proof constructed so far (consequence of (CR2));

(CR1) means for instance that when growing the proofs upwards, if one decides to apply the cut rule at some stage, only a limited amount of candidate cut formulae could be useful to end the construction of the proof. The non-determinism of the cut rule is therefore weakened. Analycity is however not guaranteed because new nominals shall be introduced during the construction of the proofs. It is known (see e.g. [START_REF] Boolos | Don't eliminate cut[END_REF][START_REF] Agostino | The taming of the cut. Classical refutations with analytic cut[END_REF]) that cut-elimination is not always a guarantee for (e cient) mechanization. The search for some analytic cut rule is often desirable and the calculi defined in this paper follow that line of research. Furthermore, we take advantage of the presence of nominals in the modal language to use "implicit prefixes" in the proof systems. As far as we know, the idea of using such implicit prefixes when nominals are involved is due to Konikowska [START_REF] Konikowska | A logic for reasoning about relative similarity[END_REF]. In [START_REF] Konikowska | A logic for reasoning about relative similarity[END_REF], Rasiowa-Sikorski-style calculi for relative similarity logics are defined. Herein, we generalize the use of implicit prefixes to a class of nominal tense logics and we introduce various restrictions on the applications of the rules while preserving completeness. Although, for some particular logics, decision procedures can be obtained using the restrictions, in the general case, the design of decision procedures (when possible) is not straightforward from our calculi. It is also fair to state that the paper [START_REF] Konikowska | A logic for reasoning about relative similarity[END_REF] has been a source of inspiration in order to develop some of the ideas present in this paper.

In the last part of the paper, we define sequent-style calculi (based on KEQ [d'A90]), say GF OL L , for fragments of the classical logic such that the calculi GL and GF OL L can be clearly viewed as syntactic variants. This allows to observe that GL is first-order in nature and to explain why it is so. Moreover, it clearly raises the questions about the relevancy of defining calculi within a general prooftheoretical framework when mechanization is wanted. Apart from the technical results of the paper, we wish to formally illustrate why numerous calculi for modal logics can be viewed as an encoding into classical logic. Although this fact is widely recognized for particular systems, we want here to propose a more general picture since the class C ⇧ 0 2 is quite large. Related work. Most of the proof systems designed for nominals tense logics are Hilbert-style ones [START_REF] Blackburn | Nominal tense logic[END_REF]. Calculi for (non nominal) tense logics can be for instance found in [RU71,Kra96,Heu98,BG98] but these calculi do not treat the nominal case and they do not consider so large a class of logics as C ⇧ 0 2 . In [START_REF] Demri | Cut-free display calculi for nominal tense logics[END_REF], display calculi for nominal tense logics have been defined and cut is not only eliminable but also a strong normalization theorem is established. For all the calculi designed in the present paper, cut (or equivalently the principle of bivalence) is not eliminable. Furthermore, the sequent calculi defined in the present paper are based on a completely di↵erent approach: we rather use the nominals as "implicit prefixes". In that sense, our calculi are explicit systems following [START_REF] Goré | Tableaux methods for modal and temporal logics[END_REF] but without introducing any extra proof-theoretical device that does not belong to the object modal language. Furthermore, the calculi defined in this paper does not di↵er very much in spirit with those defined in [START_REF] Russo | Modal logics as labelled deductive systems[END_REF][START_REF] Basin | Natural deduction for nonclassical logics[END_REF]. Indeed, we associate syntactically rules to formulas defining relational theories. However, we are able to capture all the conditions on frames for the properly displayable modal logics defined in [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF]. We wish also to thank one of the referees for pointing us to [START_REF] Blackburn | Internalizing labeled deduction[END_REF][START_REF] Tzakova | Tableau calculi for hybrid logics[END_REF] where tableau-style calculi having technical similarities with ours have been defined.

Nominal tense logics

Given a countably infinite set 1

For 0 = {p 0 , p 1 , p 2 , . . .} of atomic propositions and a countably infinite set For N 0 = {i 0 , i 1 , . . .} of names, the formulas 2 NTL(G, H) are inductively defined as follows:

:

:= p k | i k | 1 ^ 2 | 1 ) 2 | ¬ | G | H for p k 2
For 0 and i k 2 For N 0 . Standard abbreviations include ,, F , P . We write | | to denote the length of the formula for some (unspecified) succinct encoding. An occurrence of the formula is said to be a subformula of the formula of secondary disjunctive force def , is a subformula of and is the immediate subformula either of a conjunction in of negative polarity or of an implication in of positive polarity. We use here the usual notion of polarity. For instance, p 0 occurs negatively in (p 1 ^p0 ) ) p 1 . A modal frame F = hW, Ri is a pair such that W is a non-empty set and R is a binary relation on W . We use R(w , is true in all the models based on the frames of C. A formula is said to be L-satisfiable def , ¬ is not L-valid. Now, we define the class C ⇧ 0 2 of nominal tense logics announced in the introduction. First, we need to present preliminary definitions. Here, we consider the fragment of FOL built using the following vocabulary: > is the verum logical constant; {P k : k 2 !} is a countable set of unary predicate symbols; R and = (identity) are the unique binary predicate symbols;

) def = {v 2 W : (w, v) 2 R}. A model M is a structure M = hW,
{a k : k 2 !} is a countable set 2 of individual constants; {x k : k 2 !} [ {y k : k 2 !} is a countable set of individual variables. A ⇧ 0
1formula is a FOL-formula of the form 8x 1 . . . 8x n where is quantifier-free and n 1. A ⇧ 0 2 -formula is a FOL-formula of the form 8x 1 . . . 8x n 9y 1 . . . 9y m where is quantifier-free and n, m 1. A restricted ⇧ 0 2 -formula is defined here as a FOL-formula of the form 8x 1 . . . 8x n 9y 1 . . . 9y m ( 1 ) 2 ) where 1.

is in prenex normal form (PNF) and 1 ) 2 is precisely its matrix; 2. 1 and 2 are formulas built upon the binary predicate symbols R, =, the truth logical constant > and from {x 1 , . . . , x n , y 1 , . . . , y m } (no individual constant occurs in 1 ) 2 ); n 1; m 0; 3. 1 is either the logical constant > or a finite conjunction of literals (atomic formulae or negated atomic formulae) where no y i occurs in 1 ; 4. 2 is a disjunction of conjunctions of literals.

A nominal tense logic L = hNTL(G, H), Ci is an element of the class C ⇧ 0 2 def ,
there is a set3 of restricted ⇧ 0 2 -formulae such that C is exactly the set of frames satisfying each formula from (in the first-order sense). The class C of modal frames is also said to be C ⇧ 0 2 -definable. The class C ⇧ 0 2 is quite large. By manipulation at the first-order level one can show:

1. For any closed (unrestricted) ⇧ 0 2 -formula def = 8x 1 . . . 8x n 9y 1 . . . 9y m ( 1 )
2 ) in PNF such that the only variables in 1 belong to {x 1 , . . . , x n }, there exists a finite conjunction of restricted ⇧ 0 2 -formulae equivalent to . 2. Every primitive first-order formula in the sense of [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF] is logically equivalent to a restricted ⇧ 0 2 -formula. 3. There exist C ⇧ 0 2 -definable classes of frames that contain only infinite frames (see e.g. [START_REF] Blackburn | Nominal tense logic[END_REF]).

Expressivity of the restricted ⇧ 0 2 -formulae is also well-illustrated by the fact that not only are there C ⇧ 0 2 -definable classes of frames that are not modally definable but also all the first-order classes of frames defined by a conjunction of conditions from Figure 2 and Figure 3 in [START_REF] Goré | Tableaux methods for modal and temporal logics[END_REF] are C ⇧ 0 2 -definable. All the first-order definable classes of frames considered in [START_REF] Russo | Modal logics as labelled deductive systems[END_REF][START_REF] Castilho | Modal tableaux with propagation rules and structural rules[END_REF] are C ⇧ 0 2definable and C ⇧ 0 2 contains all the modal logics (in their nominal tense version) defined with Horn clauses from [START_REF] Basin | Natural deduction for nonclassical logics[END_REF]. Furthermore, for any nominal tense logic L = hNTL(G, H), Ci such that C is first-order definable by a finite set of restricted ⇧ 0 2 -formulae, it is known that the L-validity problem can be translated into FOL-validity (using [START_REF] Van Benthem | Modal logic and classical logic[END_REF][START_REF] Gargov | Modal logic with names[END_REF]). However, there is no guarantee that L admits a proof system (based on KE for instance) such that the cut rule satisfies the conditions (CR1), (CR2) and (CR3) -see Section 1. In the present paper, the delimitations of the class C ⇧ 0 2 has been designed in such a way that the sequent calculi (based on KE) admit a cut-rule satisfying the computationnally nice conditions (CR1), (CR2) and (CR3) -other restrictions on the applications of various rules shall be introduced. Those criteria distinguish our work from the standard translation into FOL but other criteria are of course possible as done in [BMV97, Section 4] where enlighting analyses about the behaviour of the falsum ? can be found. To conclude this section, we warn the reader that although C ⇧ 0 2 is undoubtly a very large class, we ignore whether it contains any logic useful in practice.

Sequent-style calculi for nominal tense logics

In this section, L denotes a nominal tense logic hNTL(G, H), Ci in C ⇧ 0 2 characterized by the set of restricted ⇧ 0 2 -formulae.

Preliminaries

Most of the prefixed tableaux calculi for modal logics use prefixes as a compact way to represent sets of positive literals in first-order logic. It partly explains why numerous calculi can be viewed as a "clever translation"4 into classical logic (see e.g. [START_REF] Gent | Analytic proof systems for classical and modal logics of restricted quantification[END_REF]). For instance, in [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF], a prefix is defined as a (non-empty) sequence of natural numbers. A sequence i 1 . . . i n 2 ! ⇤ (n 1) can be understood (for example for the modal logic S4) as the set5 {R(a i1...im , a i1...i m 0 ) : 1  m  m 0  n} of positive literals (the a 's are individual constants). It is therefore inaccurate to believe that since prefixes can be interpreted at the metalevel by worlds, then prefixes and nominals have the same expressive power. Actually, the prefixes are more expressive since the nominals do not contain any information about the accessibility relation. However, formulas involving nominals can encode first-order literals, positive and negative ones as shown below. For any model M = hW, R, mi, it is easy to show that i 1 ) G¬i 2 is true in M i↵ (m(i 1 ), m(i 2 )) 6 2 R. So, i 1 ) G¬i 2 can be used as a negative literal. What seems to be lost here, is a conciseness of the representation: each literal is represented by one nominal tense formula of the same length (modulo some constant) and it is the approach chosen in the calculi defined in Section 3.2. However, since we are dealing with logics whose satisfiability is NP-hard, the following argument shows that conciseness is a secondary issue for mechanization. Indeed, let i 1 . . . i n be a (non-empty) sequence of natural numbers representing a set X of first-order positive literals subset of {R(a i1...im , a i1...i m 0 ) : m, m 0 2 {1, . . . , n}} (it depends on the modal logic we consider but let us treat the general case). The length of i 1 . . . i n , say |i 1 . . . i n |, is naturally defined as the sum of the length (in binary writing) of each natural number occurring in i 1 . . . i n . For instance, |i 1 . . . i n | n and card(X)  n 2 . Let X be the following nominal tense formula V R(ai 1 ...im ,ai 1 ...i m 0 )2X i i1...im ) ¬G¬i i1...i m 0 that encodes the prefix i 1 . . . i n (or equivalently that encodes X). The generalized conjunction V should be here understood as an abbreviation for a certain amount of binary conjunctions.

| X | is in O(|i 1 . . . i n | 3
) and therefore, if a formula has a proof ⇧ with the "concise representation" of the positive literals, then has a proof ⇧ 0 with the representation of literals "in extension" where |⇧ 0 | is in O(|⇧| 3 ). The length of the proof ⇧, denoted |⇧|, is defined as the number of nodes in the tree. In a more general setting, it would be necessary to use a more refined definition of proof complexity which takes into account the length of proof steps. Since the calculi involved in the paper use a very restricted cut-rule (the size of the cut-formula is linear in the size of the conclusion), our definition is su cient for our needs. As no subexponential algorithm for any NP-hard problem is known, such a cubic overhead (| X | 2 O(|i 1 . . . i n | 3 )) is not so significant (even in the worst-case) when dealing with NP-hard problems (and a fortiori with PSPACE-hard problems). Of course, this is highly significant to establish tight complexity upper bounds as done in [START_REF] Hudelmaier | Improved decision procedures for the modal logics K, KT and S4[END_REF]. In [START_REF] Kripke | Semantical analysis of modal logic I: normal modal propositional calculi[END_REF][START_REF] Castilho | Modal tableaux with propagation rules and structural rules[END_REF] and [Heu98, Chapter 4], some of the graphical representations of the sets of (positive) first-order literals enjoy some conciseness property comparable to the one for prefixes.

Definition

The basic syntactic objects in the calculus are sequents. A sequent is an expression of the form ` where and are finite multisets of nominal tense formulae, i.e. unordered collections of formulae that may contain several occurrences of the same formula. We write for { } and let "," denote the multiset union. The length of the sequent ` , denoted | ` |, is the sum of the length of each element from , . The sequent calculus, say GL, for the logic L contains the rules in Figures 123. Other rules depending on are presented when needed. In Figure 2, the rules (ref l), (sym) and (trans) encode properties of identity (reflexivity, symmetry and transitivity). Similarly, the rules (sub `) and (`sub) ("sub" stands for substitution) encode that identical terms can be substituted. The (start)-rule has a special status since in any proof, this rule is applied exactly once, at the root (with the forthcoming restriction (R start )). This initiates the introduction of nominals that behave as prefixes. Observe that i ) is L-valid i↵ is L-valid when i does not occur in .

, i ) ` , i ) (initial sequents) `i ) ` (start)
For the (start)-rule, i does not occur in . We continue here the definition of GL. Let be a finite sequence of formulas of the form i ) j, i ) ¬G¬j, i ) ¬j, i ) G¬j. Those formulae precisely "encodes" positive and negative first-order literals whose (binary) predicate symbol is either = or R. We define the sequent ( ` ) ⌦ inductively on the length of as follows ( denotes the empty string and ⌦ is simply an operator that inserts formulae in sequents):

-( ` ) ⌦ def = ` ; -( ` ) ⌦ (i ) j). 0 def = ( , i ) j ` ) ⌦ 0 ; -( ` ) ⌦ (i ) G¬j). 0 def = ( , i ) G¬j ` ) ⌦ 0 ; Fig. 2. Common core of (introduction) rules in GL ` , i ) , i ) ` ` (P B) Fig. 3. Principle of bivalence -( ` ) ⌦ (i ) ¬j). 0 def = ( ` , i ) j) ⌦ 0 ; -( ` ) ⌦ (i ) ¬G¬j). 0 def = ( ` , i ) G¬j) ⌦ 0 .
Let be a restricted ⇧ 0 2 -formula of the form

8x 1 , . . . , x n 9y 1 , . . . , y m s 1 0 P 1 0 (z 1 1,0 , z 1 2,0 ) ^. . . ^sl(0) 0 P l(0) 0 (z l(0) 1,0 , z l(0) 2,0 ) ) W k i=1 s 1 i P 1 i (z 1 1,i , z 1 2,i ) ^. . . ^sl(i) 0 P l(i) 0 (z l(i) 1,i , z l(i)
2,i ) where 1. each P j i belongs to {=, R}; each s j i belongs to { , ¬};

2. each z ↵,0 (1  ↵  2, 1   l(0)) belongs to {x 1 , . . . , x n }; 3. each z ↵,i (1  ↵  2, 1  i  k, 1   l(i)) belongs to {x 1 , . . . , x n , y 1 , . . . , y m }.
We shall now define the ( )-rule that mimicks the syntactic structure of . For any i, j 2 For N 0 , for any s, s 0 2 { , ¬} such that s 6 = s 0 and for any P 2 {=, R}, let us define the formula ⌃(sP, i, j) as follows:

⌃(sP, i, j) def = ⇢ i ) s 0 G¬j if P = R; i ) sj otherwise.
Roughly speaking, a literal sP (x k , x k 0 ) in shall be encoded by ⌃(sP, i k , i k 0 ). For any formula in , we add the ( )-rule in Figure 4 to GL. The conditions

( ` ) ⌦ 1 . . . ( ` ) ⌦ k ( ` ) ⌦ 0 ( ) 1. 0 = ⌃(s 1 0 P 1 0 , i 1 1,0 , i 1 2,0 ), . . . , ⌃(s l(0) 0 P l(0) 0 , i l(0) 1,0 , i l(0) 2,0 ); 2. for 1  u  k, u = 0.⌃(s 1 u P 1 u , i 1 1,u , i 1 2,u ). . . . .⌃(s l(u) u P l(u) u , i l(u) 1,u , i l(u)
2,u ); 3. for any ↵, ↵ 0 2 {1, 2}, q, q 0 2 {1, . . . , k}, r 2 {1, . . . .l(q)} and r 0 2 {1, . . . .l(q 0 )}, (a) z r ↵,q = z r 0 ↵ 0 ,q 0 i↵ i r ↵,q = i r 0 ↵ 0 ,q 0 ; (b) if z r ↵,q is equal to some y i , then i r ↵,q does not occur in the conclusion. 1. and 2. in Figure 4 relate the ( )-rule with the structure of (without taking care of the variables). Condition 3.(a) roughly states that each variable occurring in corresponds to a unique nominal in the application of the ( )-rule.

Condition 3.(b) states that the nominals corresponding to the y i 's are new on the branch. The ( )-rule can be viewed as a generalization of the "⇢-rule" in [START_REF] Baldoni | Normal Multimodal Logics: Automated Deduction and Logic Programming[END_REF] and of the "Horn relational rule" in [START_REF] Basin | Labelled propositional modal logics: Theory and practice[END_REF][START_REF] Basin | Natural deduction for nonclassical logics[END_REF]. More generally, the ( )-rules merely encodes the logical consequence relation of the first-order relational theory of L (as also done in [START_REF] Gent | Analytic proof systems for classical and modal logics of restricted quantification[END_REF]). Furthermore, since the definition of the ( )-rules is purely syntactic, it is not guaranteed that for logics L, L 0 in C ⇧ 0 2 characterized by and 0 respectively, if and 0 define the same class of frames, then GL and GL 0 have exactly the same rules.

` , i ) j, i ) G¬j ` , i ) G¬j ` , i ) G¬j, i ) j ` , i ) j
A proof ⇧ in GL is a tree whose nodes are labelled by sequents satisfying the following conditions: the topmost sequents of ⇧ are initial sequents and every sequent of ⇧, except the lowest one is an upper sequent of an inference whose lower sequent is also in ⇧. A formula is provable in GL def , there is a proof ⇧ in GL such that ` is the lowest sequent of ⇧.

Soundness, restrictions and completeness

Lemma 1. Let ` be a sequent provable in GL. Then, for any L-model M, for all 2 , is true in M implies that 0 is true in M for some 0 2 . The proof is by induction on the length of the derivation. It is more standard to prove soundness by using the notion of satisfiability in a model rather than the notion of truth in a model as done here.

Theorem 1. If 2 NTL(G, H) is provable in GL, then is L-valid.
The system GL is not minimal since for instance, the (`NOM = )-rule, the (NOM H `)-rule and the (NOM G `)-rule are derivable from the rest of GL. These rules are included for the sake of symmetry. The system GL is considerably improved for the mechanization by imposing the restrictions (R init ), (R start ), (R = ), (R no renaming ), (R P B ), (R NOM ), (R witness ), (R sub 0 ) and (R ) for 2 defined below. In the rest of the paper, by GL, we mean the calculus with such restrictions. First, any nominal j that occurs on a branch of a (possibly partial) proof whose root is labeled by is a p-name (standing for "implicit prefix") def , j has been placed on the branch by application of a rule that introduces new nominals. The notion of p-names is similar to that of Skolem constants.

-(R init ) for the initial sequent is: any 0 occurring in , i ) ` , i ) is of the form j ) 00 where j is a p-name, 00 is either a subformula of (syntactically) equal to an atomic proposition in the case when j ) 00 = i ) or a p-name, or a nominal occurring in the root sequent ` or a formula of the form G¬j 0 with j 0 a p-name.

-(R start ) for the (start)-rule is: is not of the form j ) 0 where j is a p-name. -(R = ) concerns the rules (ref l), (sym), (trans), (`sub) and (sub `): all the names i, j, k are p-names.

-(R no renaming ) is: in (`G) and in (`H) is not a negated p-name.

-(R P B ) is: i is a p-name and is either a subformula in of secondary disjunctive force or G¬j with j a p-name or a p-name j.

-(R NOM ) concerns the rules (`NOM = ), (NOM = `), (`NOM G ), (NOM G ), (`NOM H ), (NOM H `): i and i 0 are p-names whereas j is not a p-name.

-(R witness ) concerns the rules (G `) and (H `): i and j are p-names.

-(R sub 0 ) is: in the (sub 0 `)-rule and the (`sub 0 )-rule, i, j and j 0 are p-names.

-The restriction (R ) for the ( )-rule for 2 is: all the nominals occurring in 0 are p-names.

The sequent calculus GL (in its restricted form) has the following separation property: any p-name i occurring in a branch does not occur in a formula j ) occurring on the same branch, except when either j = i or = G¬i or = i. This separation property illustrates the control on the use of nominals imposed by the above restrictions.

Theorem 2. If 2 NTL(G, H) is L-valid, then is provable in GL.
The proof of Theorem 2 (using Schütte's method) is based on a similar proof for classical logic. In Section 4, we formally state in which sense GL is equivalent to a calculus for a fragment of classical logic.

Sequent calculi for fragments of classical logic with relational theories

In this section, we define a first-order Gentzen-style calculus GF OL L (based on the calculus KEQ [d'A90, Section 3.5]) such that GL and GF OL L can be viewed as syntactic variants. This is the opportunity to formally present (once and for all) how a tableaux calculus can be viewed as a translation into classical logic. Let us briefly recall the translation ST ("Standard Translation") defined in [START_REF] Van Benthem | Modal logic and classical logic[END_REF][START_REF] Gargov | Modal logic with names[END_REF] of nominal tense formulae into the first-order language (here t is either a variable or a constant): ST (p j , t)

def = P j (t); ST (i j , t) def = t=a j ; ST (¬ , t) def = ¬ST ( , t); ST ( 0 , t) def = ST ( , t) ST ( 0 , t) for 2 {^, )}; ST (G , t) def = 8 x 0 (R(t, x 0 ) ) ST ( , x 0 )) where x 0 is a new variable; ST (H , t) def = 8 x 0 (R(x 0 , t) ) ST ( , x 0 )) where x 0 is a new variable. It is known that is L-valid i↵ ) 8x 0 ST ( , x 0 ) is FOL-valid.
The previous statement assumes that is a finite conjunction. By contrast, the developments in this section does not assume that is finite. The rules of the calculus GF OL L are those presented in Figure 5 -Figure 6 (other rules are added later on). Like the notion of p-name in GL, an individual constant a occurring on a branch is said to be a p-constant (or Skolem constant) def , a does not occur in the root sequent of the proof (possibly in construction) and it has been introduced on the branch by a rule putting new constants on the branches. We write (a k ) [resp. (x)] to denote the formula whose a k is a p-constant occurring in it [resp. whose x is a free individual variable occurring in it.].

, ` , (initial sequents) under the proviso: any formula 0 in , , is (1) either a subformula 00 (a) of 8x0 ST ( , x0) where a is the unique p-constant in 00 (a) and in the case when = 00 , is atomic (2) or a formula a=b where a is a p-constant and b is either a p-constant or a constant occurring in 8x0 ST ( , x0) (3) or a formula R(a, b) where a and b are p-names.

` , , ` `

(P B)
where either is a formula of secondary disjunctive force occurring below in the proof containing a unique p-constant or is of the form a k =a k 0 or R(a k , a k 0 ) where a k and

a k 0 are p-constants. `ST ( , a k ) `8x0 ST ( , x0) (start)
the application of (start) is under the proviso that a k does not occur in ST ( , x) (or equivalently, i k does not occur in ) and 8x0 ST ( , x0) does not contain p-constants. For instance, the rules (8 `)1 and (8 `)2 can be seen as derived rules in the calculus KEQ [d'A90] using the rules from KEQ recalled below

, 8x (x), (a) ` , 8x (x) ` , 1 , 2 , ` , 1 , 1 ) 2 , `
This explains why the universal quantification in modal logic can be naturally encoded in KEQ .

Let be a finite sequence of formulas of the form R(a, a 0 ), ¬R(a, a 0 ), a=a 0 , ¬(a=a 0 ). We define the sequent ( ` ) ⌦ 0 inductively as follows:

-( ` ) ⌦ 0 def = ` ; ( ` ) ⌦ 0 a=a 0 . 0 def = ( , a=a 0 ` ) ⌦ 0 0 ; -( ` ) ⌦ 0 ¬R(a, a 0 ). 0 def = ( ` , R(a, a 0 )) ⌦ 0 0 ; -( ` ) ⌦ 0 ¬(a=a 0 ). 0 def = ( ` , a=a 0 ) ⌦ 0 0 ; -( ` ) ⌦ 0 R(a, a 0 ). 0 def = ( , R(a, a 0 ) ` ) ⌦ 0 0 .
Let be a restricted ⇧ 0 2 -formula in (we use the notations from Section 3). The rule associated to is presented in Figure 7.

By construction, the calculi GL and GF OL L have (almost) the same amount of rules and there is a natural correspondence between the rules of GL and GF OL L . For instance, the (8 `)1 -rule in GF OL L correspond to the (G `)-rule in GL and the (sub `)-rule and (sub 0 `)-rule in GL correspond to the (sub f ol )rule in GF OL L .

Let 2 For and ⇧ be a proof of 8x 0 ST ( , x 0 ) in GF OL L . By induction on the length of ⇧ one can show that any formula occurring in ⇧ has at most two p-constants occurring in it. Moreover, if is not an atomic formula and we have been able to consider most of the classes of modal frames first-order definable that can be found in the literature. Using standard correspondences, it is easy to define tableaux calculi for nominal tense logics from our sequent-style calculi. Extensions of the calculi to cope with the logical consequence relations are also possible. Moreover, by appropriately modifying the (start)-rule, one can deal with finite configuration in the sense of [Rus96, Chapters 2 and 3]. Similarly, prefixed calculi (either sequent-based or tableaux-based) could be easily defined for the corresponding (non nominal) tense logics. Because of lack of space, such developments are omitted here but they are not di cult to derive from the present paper. Similarly, the design of decision procedures from our calculi was out of the scope of this paper but it is a question worth being investigated in the future.

The adequateness of our framework for mechanization cannot be stated without further investigations although it seems theoretically appealing (see for instance in Section 3.3 how the application of rules can be restricted). There is no reason to be overly optimistic since we have shown that the non prefixed sequent calculi are syntactic variants of restricted calculi for classical logic (augmented with relational theories). This property is shared by numerous calculi from the literature. As a conclusion, it is an open question whether any general framework defining sequent-style proof systems for modal (or nominal tense, ...) logics characterized by first-order definable classes of modal frames (take for instance C ⇧ 0 2 ) is bound to define syntactic variants of calculi for fragments of classical logic augmented with relational theories.

  R, mi such that hW, Ri is a frame and m is a mapping m : For 0 [For N 0 ! P(W ) where for any i 2 For N 0 , m(i) is a singleton. Let M = hW, R, mi be a model and w 2 W . The formula is satisfied by the world w 2 W in M def , M, w |= where the satisfaction relation |= is inductively defined as follows: M, w |= p def , w 2 m(p), for every p 2 For 0 [ For N 0 ; M, w |= G def , for every w 0 2 R(w), M, w 0 |= ; M, w |= H def , for every w 0 2 R 1 (w), M, w 0 |= (R 1 is the converse of R). We omit the standard conditions for the propositional connectives. A formula is true in a model M (written M |= ) def , for every w 2 W, M, w |= . A formula is true in a frame F (written F |= ) def , is true in every model based on F. In what follows, by a logic L we understand a pair hNTL(H, G), Ci where C is a non-empty class of modal frames. A formula is said to be L-valid def

Fig. 1 .

 1 Fig. 1. Initial sequents and the rule (start)

Fig. 4 .

 4 Fig. 4. ( )-rule for 2

Example 1 .

 1 Let L 6 = def = hNTL(G, H), C 6 = i be the nominal tense logic such that def = {8x, y R(x, y) ) ¬(x=y), 8x, y ¬(x=y) ) R(x, y)}. The tense operators G and H are actually equivalent and G is merely the di↵erence modal operator [6 =]. The rules of GL 6 = are those in Figures 1-3 plus the rules defined from :

Fig. 5 .

 5 Fig. 5. First bunch of rules for GF OLL

The metavariables for atomic propositions [resp. for nominals] are p, q, . . . [resp. i, j, . . .]. When p [resp. i] is subscripted by some natural number, we mean exactly the members from For0 [resp. from For N

The metavariables for individual constants [resp. for individual variables] are a, b, . . . [resp. x, y, . . .]. When a [resp. x and y] are subscripted by some natural numbers we mean exactly the members from {a k : k 2 !} [resp. from {x k : k 2 !}[{y k : k 2 !}].

should be understood as a (possibly infinite) conjunction.

[START_REF] Beckert | Free variable tableaux for propositional modal logics[END_REF] is one of the rare papers where such a relationship is explicitly recognized.

Since ! ⇤ and ! have the same cardinality, without any loss of generality, we can assume that the individual constants and the nominals are respectively of the form a and i where 2 ! ⇤ .

Acknowledgments The author thanks Rajeev Goré for suggestions about a preliminary version of this work and for many discussions about prefixed tableaux and related matters while being an International ARC Fellow at the A.R.P. Thanks are also due to the referees for many useful suggestions and remarks and to Nicolas Peltier for reading a preliminary version.

in (`H) and (`G), j does not occur in the conclusion

under the proviso that b does not occur in the lower sequent.

,

in the above rules, a k 1 and a k 2 are p-constants and a k is not a p-constant.

, a=a ` ` a occurs in , , a=b, b=a, ` , a=b ` , a=b, b=b 0 , a=b 0 , ` , a=b, b=b 0 ` , a=b ` , (a), (b) , a=b ` , (a) (`sub f ol ) , a=b, (a), (b) ` , a=b, (a) ` (sub f ol `)

In the above rules, a, b and b 0 are p-constants Fig. 6. Common core of (introduction rules) for GF OLL

2,0 ) and all the constants in 0 are pconstants; 2. for 1  u  k, u = 0.s

2,u ); 3. for any ↵, ↵ 0 2 {1, 2}, q, q 0 2 {1, . . . , k}, r 2 {1, . . . .l(q)} and r 0 2 {1, . . . .l(q 0 )}, (a) z r ↵,q = z r 0 ↵ 0 ,q 0 i↵ a r ↵,q = a r 0 ↵ 0 ,q 0 ; (b) if z r ↵,q is equal to some y i , then a r ↵,q does not occur in the conclusion. whose predicate symbol is binary, then exactly one p-constant occurs in unless is the root formula 8x 0 ST ( , x 0 ) itself. This is reminiscent of the facts that in standard modal logic, one can deal with only one world at a time and two individual variables are su cient for encoding the quantification 2 in first-order logic. Theorem 3 below helps understanding the relationships between GL and GF OL L .

(II) Let ⇧ be a proof of 8x 0 ST ( , x 0 ) in GF OL L for some nominal tense formula . Then, there is a proof

Concluding remarks

The results of the previous sections can be extended to the polymodal case. Indeed, it is easy to consider for some countable set I of "modal terms", the family {G i : i 2 I} [ {H i : i 2 I} of tense operators by appropriately considering polymodal Kripke models. The class C I ⇧ 2 0 is defined as the class of polymodal logics such that the class of frames is determined by a (possibly infinite) set of restricted ⇧ 0 2 -formulae over the vocabulary containing {R i : i 2 I}. This extension does not generate any new technical problems and it is quite powerful as shown below. Let I 0 = {c 0 , . . . , c i , . . .} be a set of modal constants and I be the set of modal terms t inductively defined as follows: t

We wish to interpret the operators , 1 , [, \ and and the identity constant id as in the Relation Calculus. Although it is known that the Relation Calculus can be translated in classical logic, surprisingly, we can also capture such a semantics in our framework using only restricted ⇧ 0 2 -formulae. So, by using our framework we can deal with nominal (poly)tense logics admitting the operators , 1 , \, [, and this is done uniformly 6 (this list of operators is not exhaustive). By contrast, in [Bal98, Chapter VI], only the operators [ and and the constant id are treated.

In this paper, we defined sequent calculi for nominal tense logics. The idea of using "implicit prefixes" in the calculi, due to [START_REF] Konikowska | A logic for reasoning about relative similarity[END_REF], allows a great flexibility


Michiel Postema

Ayache Bouakaz

Chien Ting Chin

Nico De Jong

OPTICALLY OBSERVED MICROBUBBLE COALESCENCE AND COLLAPSE

Understanding the mechanisms of microbubble destruction is needed for the development of ultrasound guided drug and gene delivery methods and for the improvement of diagnostic ultrasonic contrast agent (UCA) detection methods. We performed 482 experiments on the coalescence and collapse mechanisms of a soft-shelled and a hard-shelled contrast agent, by subjecting an experimental lipid-shelled UCA and the hard-shelled UCA Quantison TM to 500 kHz, high-pressured ultrasound (MI≈1.0), and recording microscopic images of these events with a fastframing camera. Results showed that bubble fragmentation into smaller bubbles is the primary mechanism for lipid-shelled contrast microbubble destruction during the first cycles after ultrasound arrival. In 28% of our experimental events with a lipid-shelled UCA, we observed bubble coalescence. The coalescence mechanism was observed to be analog to the process desribed for larger gas bubbles. Repetitive coalescence and fragmentation was clearly recorded with a fast-framing camera. We also demonstrated the formation and collapse of large lipid-shelled bubbles and bubble clusters. Furthermore we showed that sonic cracking is feasible for the hard-shelled contrast agent Quantison TM .

I. INTRODUCTION

Ultrasonic contrast agent (UCA) bubble destruction has been under investigation for its potential application in high MI imaging techniques and in drug and gene delivery. Recently Van Wamel et al. demonstrated the molecular uptake of ovary cells in vitro, induced by ultrasound, with and without the presence of contrast agent bubbles [START_REF] Van Wamel | Effects of diagnostic ultrasound parameters on molecular uptake and cell viability[END_REF]. Kimmel presented his investigation on angiogenesis in vitro and in vivo in fish epidermis [START_REF] Kimmel | Micro-alterations and enhanced transport in cellular tissues exposed to therapeutic ultrasound[END_REF]. He concluded that bubble collapse and jet formation were responsible for the observed rupture and the enhanced permeability. The success of these two and other such new therapeutic techniques in drug and gene delivery is directly related to our understanding of bubble collapse and coalescence. Dayton et al. defined the following mechanisms of rapid bubble destruction: rapid destruction due to diffusion, fragmentation into smaller bubbles, and formation of a shell defect causing gas escape [START_REF] Dayton | Simultaneous optical and acoustical observations of contrast agents[END_REF]. Takeuchi introduced the term sonic cracking for the latter mechanism [START_REF] Takeuchi | A sequence of microscopic image frames collected during insonification of a hardshell model contrast agent[END_REF]. [START_REF] Jong | Optical imaging of contrast agent microbubbles in an ultrasound field with a 100-MHz camera[END_REF], and coalescence [START_REF] Postema | Real-time optical imaging of individual microbubbles in an ultrasonic field[END_REF]. Chomas et al. noted that fragmentation occurs within 0.5 ns of peak compression [START_REF] Chomas | Threshold of fragmentation for ultrasonic contrast[END_REF].

Brennen stated that most unstable situations occur when the bubble is contracting and decelerating [START_REF] Brennen | Fission of collapsing cavitation bubbles[END_REF]. Moreover he related the forming of a re-entrant jet from a collapsing bubble, to the bubble shattering into fragments when the jet impacted the other side of the bubble surface. An optical image sequence of jet occurrence in a contrast microbubble, was demonstrated by Postema et al. [START_REF] Postema | A sequence of microscopic image frames of a freely flowing contrast agent microbubble[END_REF].

Apparently water was propelled into the freely flowing microbubble.

We studied the destruction mechanisms of contrast agents by subjecting two different contrast agents to high-pressured ultrasound, and recording microscopic images of these events with a fast-framing camera.

II. EXPERIMENTAL METHODS

Our experimental setup for taking pictures of insonified contrast bubbles was extensively described in [START_REF] Postema | Real-time optical imaging of individual microbubbles in an ultrasonic field[END_REF]. A Ø 200 μm capillary hose, through which contrast agent was flowing, was fixed in the focal area of a V389-SU 500 kHz single-element transducer (Panametrics Inc., Waltham, MA) transducer. The optical observations of the insonified UCA were recorded with an Imacon 468 fast framing camera (DRS Hadland, Ltd., Tring, UK), operating at 3 MHz. In all observations, the ultrasonic wave arrived at the focal area between the first two frames. Seven frames were taken during ultrasound insonification, spanning a full ultrasound cycle. Each frame corresponded to an 88 × 58 μm 2 area.

UCA bubbles were insonified by 10 cycles of 500 kHz ultrasound at acoustic pressures corresponding to mechanical indices between 0.9 and 1.2.

We investigated the destruction mechanisms of a soft-shelled and a hard-shelled UCA. The softshelled agent was an experimental UCA, supplied by Bracco Research SA, Geneva, Switzerland. It consists of phospholipid-encapsulated gas bubbles ranging in diameter from 1 to 6 μm with a median of 2 μm. Undiluted UCA (5 ml of a 0.9% NaCl dilution, added to a 25 mg vial) was inserted through the capillary hose using either a syringe pressed by hand or a hose operated by a gravity fed or pumped infusion. The hard-shelled agent was Quantison TM (Quadrant Healthcare plc, Nottingham, UK). The shell consists of human serum albumin and ranges in thickness from 200 to 300 nm [START_REF] Frinking | Acoustic modeling of shell-encapsulated gas bubbles[END_REF]. It has a narrow size distribution with a mean diameter of 3.2 μm. 0.35 mg Quantison TM was diluted in 5 ml isotonic water. This dilution was poured into the container and covered with a microscopic cover slip. We performed 482 experiments with the experimental UCA, and 57 experiments with Quantison TM .

III. RESULTS AND DISCUSSION

Coalescence -The bubble coalescence process was described by Dhainaut as follows [START_REF] Dhainaut | Literature study on observations andexperimentsoncoalescenceandbreakupof bubbles and drops[END_REF]. First, two bubbles collide, e.g. when expanding. Upon contact, there is a flattening of the bubble surface contacts trapping part of the bubble shells. The shell parts separating the two bubbles drain until the separation reaches a critical thickness. An instability mechanism will result in rupture of the separation and the formation of a coalesced bubble. One hundred and thirty three of our experiments showed bubble coalescence clearly according to this mechanism. An example of the phenomenon is giving in Figure 1. The microbubble in the upper half at t = -5 μs, apparently split into two parts during the first cycles of ultrasound, leaving two thin, banana-shaped parts in the frames at 0 μs and 0.33 μs. At 0.66 μs and 0.99 μs the bubbles were still separated by a bubble wall. This separation had already disappeared at 1.32 μs, while the shape of the merged bubble changed from ellipsoid to almost circular. At 1.99 μs the bubble appeared circular, though hardly visible. Thus, the coalescence mechanism is analog to the process described by [START_REF] Dhainaut | Literature study on observations andexperimentsoncoalescenceandbreakupof bubbles and drops[END_REF]. Bubble coalescence was only clearly observed with the experimental UCA, and not with Quantison TM . The hard-shelled Quantison TM bubbles oscillated with too small excursions to be detected, as predicted by theory [START_REF] Jong | Basic acoustic properties of microbubbles[END_REF]. For the concentration used, the distances between the Quantison TM bubbles were much larger than the maximal excursions, and therefore bubble collision during the expansion phase may not occur. Due to coalescence, the experimental UCA microbubbles obtained sizes closer to resonance.

Fragmentation -We recorded 83 events demonstrating bubble fragmentation into smaller bubbles.

An example is given in Figure 2. At t = 0 μs the two bubbles in the middle of the frame had already fragmented into six bubbles. During expansion phase they coalesced to one big, asymmetric bubble, visible at t = 0.99 μs. During compression (t = 1.65 μs) it fragmented into smaller bubbles. Such repetitive coalescing and fragmenting behavior was clearly recorded in 12 events. This suggests that the destruction behavior of contrast microbubbles is more complex than previously assumed. Bubble fragmentation was only observed with the experimental UCA, and not with Quantison TM . We conclude that its bubble wall velocity and acceleration are too low to induce instabilities big enough for fission. In 2 events we clearly observed jets. We did not observe fragmentation in the same events however.

Sonic cracking -We observed the sonic cracking mechanism in 17 experiments, all of which were performed with Quantison TM . In total we recorded 38 different bubbles releasing free gas. Figure 3 shows an example of the sonic cracking phenomenon of two Quantison TM microbubbles. After cracking, the gas escaped. The cracked bubble in the upper right of the frames had already visible gas escape at t = 0.33 μs, whereas the cracked bubble in the lower right of the frames had the first visible sign of gas escape at t = 0.66 μs. On the recorded images the free gas expanded to up to five times the original diameter of a Quantison TM bubble. In all 57 experiments with Quantison TM , the number of cracking bubbles per event is low compared to the number of bubbles present. The highest cracking ratio observed was 8 cracking bubbles on a total number of 31. Tiny flaws in the bubble shell, may account for the reason why certain bubbles crack and others stay intact. The mechanism of sonic cracking itself is not yet understood.

Other mechanisms -Only 15 events were recorded that demonstrated other destruction mechanisms than fragmentation into smaller bubbles or sonic cracking, e.g. asymmetric collapse without fragmentation.

Since we were only looking at early cycles of the ultrasonic waves, this limits our conclusion that fission is the primary mechanism for bubble destruction.

IV. CONCLUSIONS

At before-mentioned acoustic frequency and pressures, we found bubble fragmentation into smaller bubbles the primary mechanism for lipid-shelled contrast microbubble destruction during the first cycles after ultrasound arrival. In 28% of our experimental events with a lipid-shelled UCA, we observed bubble coalescence. The coalescence mechanism was observed to be analog to the process desribed for larger gas bubbles. Due to coalescence, the experimental UCA microbubbles obtained sizes closer to resonance. Repetitive coalescence and fragmentation was clearly recorded with a fastframing camera. We demonstrated the formation and collapse of large lipid-shelled bubbles and bubble clusters. This coalescence and collapse mechanism of ultrasound contrast bubbles is analog to a previously presented mechanism on destructive properties of cavitation bubbles. We showed that sonic cracking is feasible for the hard-shelled contrast agent Quantison TM .

  Postema et al. observed bubble destruction, like De Jong et al.

V. ACKNOWLEDGMENTS

This work has been supported by the Technology Foundation STW (RKG.5104).

List of Figures