Serenella Cerrito

Marta Cialdea Mayer

A Tableau Based Decision Procedure for an Expressive Fragment of Hybrid Logic with Binders, Converse and Global Modalities

In this paper we provide the first (as far as we know) direct calculus deciding satisfiability of formulae in negation normal form in the fragment of FHL (full hybrid logic with the binder, including the global and converse modalities), where no occurrence of a universal operator is in the scope of a binder. By means of a satisfiability preserving translation of formulae, the calculus can be turned into a satisfiability decision procedure for the fragment FHL \ ✷↓✷, i.e. formulae in negation normal form where no occurrence of the binder is both in the scope of and contains in its scope a universal operator.

The calculus is based on tableaux and termination is achieved by means of a form of anywhere blocking with indirect blocking. Direct blocking is a relation between nodes in a tableau branch, holding whenever the respective labels (formulae) are equal up to (a proper form of) nominal renaming. Indirect blocking is based on a partial order on the nodes of a tableau branch, which arranges them into a tree-like structure.

Introduction

Hybrid logic is an extension of modal (propositional, possibly multi-modal) logic K by means of three constructs: nominals (propositions which hold in exactly one state of the model), the satisfaction operator @ (allowing one to state that a given formula holds at the state named by a given nominal), and the binder ↓, accompanied by state variables, which allows one to give a name to the current state (see [START_REF] Areces | Hybrid logics[END_REF] for an overview of the subject). The notation HL(Op 1 , . . . , Op n ) is commonly used to denote the extension of the modal logic K by means of the operators Op 1 , . . . , Op n . In particular, HL(@, ↓, E, ✸ -) and HL(@, E, ✸ -) include the existential global modality E (and its dual A) and the converse 1 operator ✸ -(and its dual ✷ -). In the following, HL(@, ↓, E, ✸ -) will be called full hybrid logic (like in [START_REF] Cate | On the complexity of hybrid logics with binders[END_REF]), abbreviated by FHL.

The satisfiability problem for formulae of hybrid logic without the binder is decidable, even in the presence of the global and converse modalities. But an unrestricted addition of the binder causes a loss of decidability [START_REF] Areces | A road-map on complexity for hybrid logics[END_REF][START_REF] Blackburn | Hybrid languages[END_REF]. 1However, similarly to what happens for first order logic, one can obtain decidable fragments of hybrid logic with the binder by imposing syntactic restrictions on the way formulae are built. Restricted uses of the binder are of interest also in the context of description logics [START_REF] Horrocks | Hybrid logics and ontology languages[END_REF][START_REF] Marx | Narcissists, stepmothers and spies[END_REF], formalisms that are widely used for knowledge representation, in particular as a basis of ontology languages. Beyond nominals, "binder and state variables are another feature from hybrid logic that would clearly be useful in an ontology language" [START_REF] Horrocks | Hybrid logics and ontology languages[END_REF].

Some decidability results are proved in [START_REF] Cate | On the complexity of hybrid logics with binders[END_REF]. In particular, it is proved that the source of undecidability is the occurrence of a specific modal pattern in formulae in negation normal form (NNF). A pattern π is a sequence of operators, and a formula is a π-formula, where π = Op 1 . . . Op n , if it is in NNF and contains some occurrence of Op 1 with an occurrence of Op 2 in its scope, that in turn has an occurrence of Op 3 in its scope, etc. For simplicity, when the ✷ operator is used in a pattern, it actually stands for any universal operator, i.e. one of the modalities ✷, ✷ -or A. In particular, a ↓✷-formula is a hybrid formula in NNF where some occurrence of a universal operator is in the scope of a binder; and a ✷↓✷-formula is a hybrid formula in NNF containing a universal operator in the scope of a binder, which in turn occurs in the scope of a universal operator. Finally, if π is a pattern, the fragment HL(Op 1 , . . . , Op k ) \ π is constituted by the class of NNF hybrid formulae in HL(Op 1 , . . . , Op k ) excluding π-formulae.

An important decidability result proved in [START_REF] Cate | On the complexity of hybrid logics with binders[END_REF] is the following:

(⋆) The satisfiability problem for FHL \ ✷↓✷ is decidable.

This result is tight, in the sense that there is no pattern π that contains ✷↓✷ as a subsequence and such that the satisfiability problem for FHL \ π is still decidable. Therefore, the fragment FHL \ ✷↓✷ is particularly interesting. The expressive power of the considered fragment, though obviously weaker than FHL, allows one to represent interesting graph properties. For instance, A↓x.✸x forces any structure satisfying it to be reflexive, and A↓x.✸ -✸¬x is true in structures where any state has at least a sibling. The formula ↓x.✷✸x represents a "local symmetry" property: it holds in a state which is the origin of symmetric edges only. Anagously, ↓x.✷✷✸ -x expresses "local transitivity", and ↓x.✸✸✷ -¬x holds in a state whenever it can access another state in two steps, but not directly (a simplified form of the stepmother relation described in [START_REF] Marx | Narcissists, stepmothers and spies[END_REF]).

For the aim of the present work, it is important to recall how result (⋆) is proved in [START_REF] Cate | On the complexity of hybrid logics with binders[END_REF]: there exists a polynomial satisfiability preserving translation of formulae in FHL \ ✷↓✷ into FHL \ ↓✷. The standard translation ST of FHL into first order classical logic [START_REF] Areces | A road-map on complexity for hybrid logics[END_REF][START_REF] Cate | On the complexity of hybrid logics with binders[END_REF] maps, in turn, formulae in the latter fragment into universally guarded formulae (in polynomial time), that have a decidable satisfiability problem [START_REF] Grädel | On the restraining power of guards[END_REF].

Thus, the above sketched approach to proving result (⋆) shows also that any decision procedure for formulae in FHL \ ↓✷ can easily be turned into a decision procedure for formulae in the largest fragment FHL \ ✷↓✷, by preprocessing formulae. In particular, satisfiability of formulae in the fragment FHL \ ✷↓✷ can be tested by translation [START_REF] Grädel | On the restraining power of guards[END_REF][START_REF] Cate | Guarded fragments with constants[END_REF][START_REF] Cate | On the complexity of hybrid logics with binders[END_REF],2 by use of any calculus for the guarded fragment, such as the tableau calculi defined in [START_REF] Hirsch | A tableau algorithm for the clique guarded fragment[END_REF][START_REF] Hladik | Implementation and evaluation of a tableau algorithm for the guarded fragment[END_REF], or the resolution based decision procedure for guarded clauses with equality given in [START_REF] Ganzinger | A superposition decision procedure for the guarded fragment with equality[END_REF]. Though the translation can be obtained in polynomial time, translation based proof methods do not have the possibility to exploit the specificity of the hybrid language, since guarded logic is strictly more expressive than the considered fragment of HL.

This work provides the first (as far as we know) direct calculus deciding satisfiability of formulae in FHL \ ↓✷. A preprocessing step, rewriting formulae into equisatisfiable ones, turns the calculus into a decision procedure for satisfiability of FHL \ ✷↓✷. This paper revises and extends [START_REF] Cerrito | A tableaux based decision procedure for a broad class of hybrid formulae with binders[END_REF], where only the fragment HL(@, ↓) \ ✷↓✷ is considered. Moreover, it includes full proofs, that are only sketched in [START_REF] Cerrito | A tableaux based decision procedure for a broad class of hybrid formulae with binders[END_REF]. The work is organized as follows. In Section 2 we recall the syntax and semantics of FHL. In Section 3 we define the tableau system for HL(@, ↓, ✸ -), which is extended to the global modalities in Section 4. Section 5 proves that the full calculus terminates and is complete with respect to unsatisfiability, under the assumption that the input formula is in FHL \ ↓✷. Section 6 concludes the paper pointing out differences and similarities with related works.

Hybrid Logic

In this work, for the sake of simplicity, we consider only uni-modal logic, but the extension to the multi-modal case is immediate.

Let PROP (the set of propositional letters) and NOM (the set of nominals) be disjoint sets of symbols. Let VAR be a set of state variables. Hybrid formulae F in FHL are defined by the following grammar:

F := p | a | x | ¬F | F ∧ F | F ∨ F | ✸F | ✷F | ✸ -F | ✷ -F | EF | AF | a: F | x: F | ↓x.F
where p ∈ PROP, a ∈ NOM and x ∈ VAR. In this work, the notation t: F is used (for t ∈ NOM∪VAR) rather than the more usual one @ t F . We use metavariables a, b, c, d, possibly with subscripts, for nominals, while x, y, z are used for state variables.

A formula of the form a: F is called a satisfaction statement, whose outermost nominal is a, F is its body, and the satisfaction symbol applied to a and F is the outermost satisfaction symbol of the statement. The operators ✸, ✸ -and E are called existential modalities, and ✷, ✷ -and A are universal modalities. Formulae of the form ✸F , ✸ -F and EF are existential formulae, while ✷F , ✷ -F and AF are universal formulae. The operator ↓ is a binder for state variables. A variable x is free in a formula if it does not occur in the scope of a ↓x. A formula is ground if it contains no free variables.

A subformula of a formula F is a substring of F (possibly F itself) that is itself a formula. An instance of a formula F is an expression obtained by uniformly replacing every free variable of F with some nominal. A subformula may contain free variables, while an instance is always a ground formula. Obviously, if a subformula F of G does not contain any free variable, then F is both a subformula of G and an instance of a subformula of G.

If F is a formula and a a nominal, the notation F [a/x] is used to denote the formula that is obtained from F replacing a for every free occurrence of the variable x. Analogously, if a and b are nominals, F [b/a] is the formula obtained from F replacing b for every occurrence of a.

An interpretation M is a tuple W, R, N, I where W is a non-empty set (whose elements are the states of the interpretation), R ⊆ W × W is a binary relation on W (the accessibility relation), N is a function NOM → W and I a function W → 2 PROP . We shall write wRw ′ as a shorthand for w, w ′ ∈ R.

A variable assignment σ for M is a function VAR → W . If x ∈ VAR and w ∈ W , the notation σ w

x stands for the variable assignment σ ′ such that: σ ′ (y) = σ(y) if y = x and σ ′ (x) = w.

If M = W, R, N, I is an interpretation, w ∈ W , σ is a variable assignment for M and F is a formula, the relation M w , σ |= F is inductively defined as follows:

1. M w , σ |= p if p ∈ I(w), for p ∈ PROP.

′ such that wRw ′ , M w ′ , σ |= F . 11. M w , σ |= ✸F if there exists w ′ such that wRw ′ and M w ′ , σ |= F . 12. M w , σ |= ✷ -F if for every w ′ such that w ′ Rw, M w ′ , σ |= F . 13. M w , σ |= ✸ -F if there exists w ′ such that w ′ Rw and M w ′ , σ |= F . 14. M w , σ |= AF if M w ′ , σ |= F for all w ′ ∈ W . 15. M w , σ |= EF if M w ′ , σ |= F for some w ′ ∈ W .
A formula F is satisfiable if there exist an interpretation M, a variable assignment σ for M and a state w of M, such that M w , σ |= F . Two formulae F and G are logically equivalent (F ≡ G) when, for every interpretation M, assignment σ and state

w of M, M w , σ |= F if and only if M w , σ |= G. A formula F holds in a state w of a model M (M w |= F ) iff M w , σ |= F for every variable assignment σ.
It is worth pointing out that, if t ∈ VAR ∪ NOM and F is a formula:

¬(t: F ) ≡ t: ¬F ¬↓x.F ≡ ↓x.¬F ¬✸F ≡ ✷¬F ¬✷F ≡ ✸¬F ¬✸ -F ≡ ✷ -¬F ¬✷ -F ≡ ✸ -¬F ¬EF ≡ A¬F ¬AF ≡ E¬F
Therefore, considering only formulae in negation normal form (NNF -where negation appears only in front of atoms) does not restrict the expressive power of the language.

3 Tableaux for HL(@, ↓, ✸ -)

The Expansion Rules

A tableau branch is a sequence of nodes n 0 , n 1 , . . . , where each node is labelled by a ground satisfaction statement, and a tableau is a set of branches. If n occurs before m in a branch, we shall write n < m. The label of the node n will be denoted by label(n). The notation (n) a: F will be used to denote the node n, and simultaneously say that its label is a: F . A tableau for a formula F is initialized with a single branch, constituted by the single node (n 0 ) a 0 : F , where a 0 is a new nominal. The formula a 0 : F is the initial formula of the tableau, which is assumed to be ground and in NNF.

A tableau is expanded by application of the rules in Table 1, which are applied to a given branch. The rules are standard, and their reading is standard too: a rule is applicable if the branch contains a node (two nodes) labelled by the formula(e) shown as premiss(es) of the rules. The rule ∨ replaces the current branch B with two branches, each of which is obtained by adding B a new node, labelled, respectively, by the formulae shown on the left and right below the inference line. The equality rule (=) does not add any node to the branch, but modifies the labels of its nodes. The schematic formulation of this rule in Table 1 indicates that it can be fired whenever a branch B contains a nominal equality of the form a: b (with a = b); as a result of the application of the rule, every node label F in B is replaced by F [b/a]. All the other rules extend the branch with the addition of one or two nodes, labelled by the conclusion(s).

Since we assume that the initial formula of a tableau is ground and in NNF, an easy inspection of the expansion rules shows that node labels in any branch are always ground formulae in NNF.

The ✷ and ✷ -rules are called universal rules. They have two premisses, which must both occur in the branch, in any order. Their leftmost premiss is called the major premiss, the rightmost one the minor premiss. The minor premiss is a relational formula, i.e. a satisfaction statement of the form a: ✸b (where b is a nominal).

The ✸ and ✸ -rules are called blockable rules, formulae of the form a: ✸F , where F is not a nominal, and a: ✸ -F are blockable formulae and a node labelled by a blockable formula is a blockable node.

The first node of a branch B is called the top node and its label the top formula of B. Nominals occurring in the top formula are called top nominals. If the top node of B is n 0 , the branch is said to be rooted at n 0 . The notion of top nominal is relative to a tableau branch, because applications of the equality rule may change the top formula, hence the set of top nominals.

If a node n is added to a branch B by application of the rule R to the node m, then we write m ❀ R n. In the case of rules with two conclusions, we write

m ❀ R (n, k), or, sometimes, m ❀ R n and m ❀ R k. If R is a two-premiss rule we write (m, k) ❀ R n.
The application of the equality rule does not change nodes, but only their

a: (F ∧ G) a: F a: G (∧) a: (F ∨ G) a: F | a: G (∨) a: b: F b: F (@) a: ↓x.F a: F [a/x] (↓) [B] a: b B[b/a] (=) (not applicable if a = b) a: ✷F a: ✸b b: F (✷) a: ✸F a: ✸b b: F (✸)
where b is a fresh nominal (not applicable if F is a nominal)

a: ✷ -F b: ✸a b: F (✷ -) a: ✸ -F b: ✸a b: F (✸ -)
where b is a fresh nominal A formula a: F is said to occur in a tableau branch B (or a: F ∈ B) if for some node n of the branch, label(n) = a: F . Similarly, a nominal occurs in a branch B if it occurs in the label of some node of B. Finally, a nominal a labels a formula F in B if a: F ∈ B.

Restrictions on Rule Application

Termination is achieved by means of a loop-checking mechanism using nominal renaming. The need for nominal renaming is due to the fact that, in the presence of the binder, non-top nominals may occur in the body of any node label, which therefore is not necessarily a subformula of the top formula. In order to define this mechanism, some preliminary definitions are needed. Mappings are extended to act on formulas in the obvious way: if π is a mapping and F a formula, π(F ) is the formula obtained by substituting π(a) for a in F , for every nominal a.

A mapping π for B maps a formula F to a formula G if:

1. π(F ) = G;
2. π is the identity for all nominals which do not occur in F .

A formula F can be mapped to a formula G in B if there exists a mapping π for B mapping F to G.

Since a mapping π is the identity almost everywhere, it can be represented by a finite set of pairs of the form {b 1 /a 1 , . . . , b n /a n } where a i = b i , whenever π(a i ) = b i and π(c) = c for all c ∈ {a 1 , . . . , a n }.

The application of the blockable rules is restricted by blocking conditions: a direct blocking condition, which forbids the application of a blockable rule to a node n, whenever the label of a previous node can be mapped to label(n); and also an indirect blocking condition. The latter is necessary because, since a node may be (directly) blocked in a branch after it has already been expanded, all the nodes which, in some sense, depend from such an expansion must be blocked too. So, a notion of indirect blocking is needed, which in turn requires a new partial order on nodes. The following definition introduces a binary relation on nodes, which organizes them into a family of trees. In other terms, when a blockable rule is applied to a node n, a first pair of children of n w.r.t. ≺ B is generated. The application of non-blockable rules generates siblings, where, in the case of the two universal rules, it is the minor premiss which is added a sibling. Intuitively, when n ≺ B m, n is the node which is taken to be the main "responsible" of the presence of m in the branch: the first "children" of a node n are nodes obtained from n by application of a blockable rule. And, if a node m is obtained from m ′ (as the minor premiss, in the case of the universal rules) by means of a non-blockable rule, then they are siblings w.r.t. ≺ B .

Inductive cases. If m ≺ B n, then: 1. if n ❀ R k, where R ∈ {∨, @, ↓, ∧}, then m ≺ B k; 2. if label(n) is a relational formula and for some n ′ , (n ′ , n) ❀ R k, where R is a universal rule, then m ≺ B k. If m ≺ B n
Example 1. As an example, consider the tableau branch for Before defining the blocking conditions we prove some properties of ≺ B : i.e. that any node has at most one parent and only blockable nodes may have children. Consequently, ≺ B arranges the nodes of a branch into a forest of trees, where non-terminal nodes are blockable nodes. For instance, the nodes of the tableau branch B of Example 1 are arranged into four trees: three of them consist of a single node (respectively: 0, 1 and 3), while the fourth one is rooted at 2 and is shown in Figure 2. Lemma 1. Let B be a tableau branch.

1. For each node n in B, there exists at most one node m such that m ≺ B n. Therefore, there is exactly one maximal chain

n 1 ≺ B n 2 ≺ B . . . ≺ B n k = n
where n 1 is a root node.

2. If for some n, m ≺ B n, then m is a blockable node. Therefore, for any chain

n 1 ≺ B n 2 ≺ B . . . ≺ B n k ≺ B n k+1 n 1 , . . . , n k are all blockable nodes.
Proof. The first item can easily be proved by induction on the definition of ≺ B .

The second follows directly from the definition.

As a further remark on the relation ≺ B , it is worth pointing out that two siblings are not necessarily labelled by satisfaction statements whose outermost nominal is the same (because, for instance, of the ✸ rule, like nodes 4-7 of Figure 1, or the @ rule, like nodes 14 and 15 of the same figure), and, vice-versa, not all nodes labelled by formulae of the form b: F for a given nominal b are necessarily siblings. In particular, this fact can be caused by applications of the equality rule. For example, let us assume that, in a given branch B, n 1 ≺ B (m) a: F and n 2 ≺ B (k) b: G; if then the equality rule replaces a with b, we still have, in the new branch

n 1 ≺ B (m) b: F and n 2 ≺ B (k) b: G. So, if n 1 = n 2 ,
m and k are not siblings, although the outermost nominal of their labels is the same.

The notions of direct and indirect blocking can now be defined.

Definition 4 (Direct and indirect blocking). Let B be a tableau branch. The set of directly and indirectly blocked nodes in B is defined by induction on the (total) order < on the nodes of B:

• n is blocked if it is either directly or indirectly blocked.

• n is directly blocked by m if n is a blockable node, m < n, m is not blocked and label(m) can be mapped to label(n) in B; n is directly blocked in B if it is directly blocked by some m in B.

• n is indirectly blocked if it is not directly blocked and it has an ancestor w.r.t. ≺ B which is blocked.

An indirectly blocked node is called a phantom node (or, simply, a phantom).

The tableau branch B represented in Figure 1 represents a blocking case: node 17 is directly blocked by 7, because b and c are compatible in

B (Φ B (b) = Φ B (c) = {p}).
The blocking relation is dynamic, i.e. blockings are not established forever, since they are relative to a tableau branch, and can be undone when expanding the branch. What may happen is that a node may be blocked in a branch B and then unblocked after expanding B, because the addition of new nodes or changes in node labels may destroy nominal compatibility. Similarly, when the equality rule affects either the label of a blocked node n or that of its blocking node, n is not automatically kept blocked. Possibly, a new blocking can be introduced (but compatibilities must be checked again), by means of a different mapping.

It is worth pointing out that, in the presence of the binder, termination requires indirect blocking, even when the input formula contains no converse modalities (see Example 5 in Section 3.3).

The application of the expansion rules is restricted by the following conditions:

Definition 5 (Restrictions on the expansion rules). The expansion of a tableau branch B is subject to the following restrictions:

R1. no node labelled by a formula already occurring in B as the label of a nonphantom node is ever added to B;

R2. a node n labelled by a: ✸F (or a: ✸ -F ) cannot be expanded if B contains non-phantom nodes labelled by a: ✸b (b: ✸a) and b: F for some nominal b.

R3. a phantom node cannot be expanded by means of a single-premiss rule (including the equality rule), nor can it be used as the minor premiss of the universal rules;

R4. a blockable node n cannot be expanded if it is directly blocked in B.

Restriction R1 amounts to saying that:

1. a node n (or pair of nodes n, m) cannot be expanded in B if the expansion of n (and m) would produce a single node, whose label would be a formula which already occurs in B as the label of a non-phantom node;

2. the ∧ rule cannot be applied to a node (n) a: F ∧ G whenever both a: F and a: G are already the labels of non-phantom nodes in B;

3. if a node (n) a: F ∧ G can be expanded, but a: F (or a: G, but not both) is already the label of a non-phantom node, then only one new node is added to the branch, with label a: G (or a: F ); 4. if label(n) = a: F ∧ F , then, when n is expanded, a single node is added to the branch, labelled by a: F .

It is worth pointing out, moreover, that:

• an effect of the equality rule is that siblings may share the same label, notwithstanding restriction R1. This is shown by Example 2 below.

• Restriction R3 does not forbid firing the universal rules with a nonphantom minor premiss, even if the major premiss is a phantom node.

• The interplay among restrictions R2, R3 and R4 ensures that any blockable node n can be expanded at most once in a tableau (see Lemma 2 in Section 4).

• Termination would not be guaranteed if restriction R1 were replaced by the condition that a node (or pair of nodes) is never expanded more than once in the branch. This is shown by Example 3, given below. Example 3. The construction of the tableau branch for the formula a: (✸b ∧ ✷a: ✸b), in Figure 4 satisfies the requirement that no node or pair of nodes is ever expanded more than once, but violates restriction R1. Obviously, tableau construction does not terminate.

(p ∧ y)) 0 ❀ ↓ 1 (2) b: ✸b 1 ❀ ✸ 2 (3) b: (p ∧ ↓y.b: (p ∧ y)) 1 ❀ ✸ 3 (4) b: p 3 ❀ ∧ 4 (5) b: ↓y.b: (p ∧ y) 3 ❀ ∧ 5 (6) b: b: (p ∧ b) 5 ❀ ↓ 6 (7) b: (p ∧ b) 6 ❀ @ 7 (8) b: p 7 ❀ ∧ 8 (9) b: b 7 ❀ ∧ 9
(0) a 0 : a: (✸b ∧ ✷(a: ✸b)) (1) a: (✸b ∧ ✷(a: ✸b))

0 ❀ @ 1 (2) a: ✸b 1 ❀ ∧ 2 (3) a: ✷(a: ✸b) 1 ❀ ∧ 3 (4) b: a: ✸b (3, 2) ❀ ✷ 4
(5) a: ✸b 4 ❀ @ 5 (6) b: a: ✸b (3, 5) ❀ ✷ 6 (7) a: ✸b 6 ❀ @ 7 . . . A branch is closed whenever it contains, for some nominal a, either a pair of nodes (n) a: p, (m) a: ¬p for some p ∈ PROP, or a node (n) a: ¬a. As usual, we assume that a closed branch is never expanded further on. A branch which is not closed is open. A branch is complete when it cannot be further expanded. For instance, the tableau branch represented in Figure 1 is complete and open.

Examples

This section concludes with some further examples. In each of them, B denotes the considered branch, and the notation B n is used to denote the branch segment up to node n, while Φ n abbreviates Φ Bn . Example 4. This example illustrates the dynamic nature of the blocking relation, even without any application of the equality rule. Figure 5 where the first applications of the ∧-rule are collapsed into one. The relation ≺ B in this branch can be represented by the trees in Figure 6, and the single-node tree 0. When the construction proceeds, expanding the non-blocked node 19, and nodes 21-23 are added to the branch, c and b are no more compatible (Φ 23 (c) = {p} while Φ 23 (b) is still empty), so node 20 is unblocked and it is expanded, producing 24-26 and the branch closes.

(0) a 0 : F (1) a 0 : ✸↓x.✸x: p 0 ❀ ∧ 1 (2) a 0 : ✸↓y.✸y: ¬p 0 ❀ ∧ 2 (3) a 0 : ✸↓z.(✸z: p ∧ ✸z: ¬p) 0 ❀ ∧ 3 (4) a 0 : ✸a 1 ❀ ✸ 4 (5) a: ↓x.✸x: p 1 ❀ ✸ 5 (6) a: ✸a: p 5 ❀ ↓ 6 (7) a: ✸a 1 6 ❀ ✸ 7 (8) a 1 : a: p 6 ❀ ✸ 8 (9) a: p 8 ❀ @ 9 (10) a 0 : ✸b 2 ❀ ✸ 10 (11) b: ↓y.✸y: ¬p 2 ❀ ✸ 11 (12) b: ✸b: ¬p 11 ❀ ↓ 12 (13) b: ✸b 1 12 ❀ ✸ 13 (14) b 1 : b: ¬p 12 ❀ ✸ (15) b: ¬p 14 ❀ @ (16) a 0 : ✸c 3 ❀ ✸ 16 (17) c: ↓z.(✸z: p ∧ ✸z: ¬p) 3 ❀ ✸ 17 (18) c: ✸c: p ∧ ✸c: ¬p 17 ❀ ↓ 18 (19) c: ✸c: p 18 ❀ ∧ (20) c: ✸c: ¬p 18 ❀ ∧ (21) c: ✸c 1 19 ❀ ✸ (22) c 1 : c: p 19 ❀ ✸ (23) c: p 22 ❀ @ (24) c: ✸c 2 20 ❀ ✸ (25) c 2 : c: ¬p 20 ❀ ✸ (26) c: ¬p 25 ❀ @
After the addition of node 23, a and c become compatible, so that in B 23 node 19 is blocked by 6, and 21-23 are phantom nodes. Since 20 is not a descendant of 19 w.r.t. ≺ B , it is not a phantom, thus it can be expanded. Example 5. This example shows the need of indirect blocking (restriction R3) to ensure termination (even in the absence of the converse modalities). Let F = a: ((✷↓x.✸↓y.(x: p ∧ a: ✸y)) ∧ ✸q)

Figure 7 shows a complete branch in a tableau for F .

(1) a 0 : F (2) a: ((✷↓x.✸↓y. ). Therefore its children w.r.t. ≺ B33 , i.e. 27-33, are all phantom nodes, and, in particular, node 33 cannot participate, with node 3, to an expansion via the ✷ rule.

(x: p ∧ a: ✸y)) ∧ ✸q) 1 ❀ @ 2 (3) a: ✷↓x.✸↓y. (x: p ∧ a: ✸y) 2 ❀ ∧ 3 (4) a: ✸q 2 ❀ ∧ 4 (5) a: ✸b 4 ❀ ✸ 5 (6) b: q 4 ❀ ✸ 6 (7) b: ↓x.✸↓y. (x: p ∧ a: ✸y) (3, 5) ❀ ✷ 7 (8) b: ✸↓y.(b: p ∧ a: ✸y) 7 ❀ ↓ 8 (9) b: ✸b 1 8 ❀ ✸ 9 (10) b 1 : ↓y.(b: p ∧ a: ✸y) 8 ❀ ✸ 10 (11) b 1 : (b: p ∧ a: ✸b 1 ) 10 ❀ ↓ 11 (12) b 1 : b: p 11 ❀ ∧ 12 (13) b 1 : a: ✸b 1 11 ❀ ∧ 13 (14) b: p 12 ❀ @ 14 (15) a: ✸b 1 13 ❀ @ 15 (16) b 1 : ↓x.✸↓y. (x: p ∧ a: ✸y) (3, 15) ❀ ✷ 16 (17) b 1 : ✸↓y.(b 1 : p ∧ a: ✸y) 16 ❀ ↓ 17 (18) b 1 : ✸b 2 17 ❀ ✸ 18 (19) b 2 : ↓y.(b 1 : p ∧ a: ✸y) 17 ❀ ✸ 19 (20) b 2 : (b 1 : p ∧ a: ✸b 2 ) 19 ❀ ↓ 20 (21) b 2 : b 1 : p 20 ❀ ∧ 21 (22) b 2 : a: ✸b 2 20 ❀ ∧ 22 (23) b 1 : p 21 ❀ @ 23 (24) a: ✸b 2 22 ❀ @ 24 (25) b 2 : ↓x.✸↓y. (x: p ∧ a: ✸y) (3, 24) ❀ ✷ 25 (26) b 2 : ✸↓y.(b 2 : p ∧ a: ✸y) 25 ❀ ↓ 26 (27) b 2 : ✸b 3 26 ❀ ✸ 27 (28) b 3 : ↓y.(b 2 : p ∧ a: ✸y) 26 ❀ ✸ 28 (29) b 3 : (b 2 : p ∧ a: ✸b 3 ) 28 ❀ ↓ 29 (30) b 3 : b 2 : p 29 ❀ ∧ 30 (31) b 3 : a: ✸b 3 29 ❀ ∧ 31 (32) b 2 : p 30 ❀ @ 32 (33) a: ✸b 3 31 ❀ @ 33
Without restriction R3, the construction of the branch would go on forever, since the following nodes could be added: This section shows how to extend the calculus defined in Section 3 to the global modalities A and E, obtaining a terminating and complete system for the fragment FHL \ ↓✷, i.e. formulae in NNF of HL(@, ↓, E, ✸ -) where no universal modality (✷, ✷ -and A) occurs in the scope of a binder. Table 2 shows the new expansion rules that are added to the calculus. Blockable rules now include the E rule. Moreover, formulae of the form a: EF are among the blockable formulae, and nodes labelled by such formulae are among the blockable nodes. The A rule is a universal rule. When the A rule is applied to produce a node labelled by b: F , we say that it focuses on the nominal b and b is the focused nominal of the expansion.

a: AF b: F (A) a: EF b: F (E)
where b occurs in the branch where b is a fresh nominal Table 2: The expansion rules for the global modalities

The definitions of nominal compatibility and mappings (Definitions 1 and 2) do not change. In particular, though A is a universal modality like ✷ and ✷ -, the sets Φ B (a) do not include formulae of the form AF .

The rules A and E are quite natural and standard. The extension of restriction R2 to the new blockable rule is also straightforward, and will be given later on; restriction R4 already applies also to the E rule, since it is included among the blockable ones. Actually, the blocking condition for the E rule could be made more general, establishing that, in order for (m) b: EG to block (n) a: EF directly in B i , it is sufficient that G can be mapped to F in B i (i.e. the outermost nominal might be ignored). The completeness argument in Section 5.2 would however need the addition of corresponding distinguishing cases in many points, which would make it heavier.

What is less obvious is how to extend the relation ≺ B , so as to preserve the main properties which ensure termination, and to define its interplay with restrictions on the application of the A rule, while preserving the properties needed to show completeness.

In order to give a better understanding of the definitions that follow, it may be useful to summarize the main guidelines of the termination and completeness proofs (whose details are given in Section 5).

Termination is proved by showing that the nodes of a branch B are arranged by ≺ B into a bounded sized set of trees, each of which has bounded width and bounded depth. Hence any tableau branch B has a number of nodes that is bounded by a function of the size of the initial formula.

In order to prove completeness, it is shown how to extend a subset N 0 of any complete and open branch B in such a way that every directly blocked node is added a suitable "witness". The label of each newly added node is obtained from a node in N 0 by suitably renaming non-top nominals. A model of the initial formula can then be extracted from such an extension. The set N 0 is the union of the non-phantom nodes in B and the nodes of the form (n) a: F for F ∈ Cmp(B) and a occurring in some non-phantom node in B. It is shown to enjoy a form of saturation property for non-phantom nodes: it is consistent (there are no labels of the form a: ¬a, or both a: p and a: ¬p), it does not contain non-trivial equalities, and, for any node or pair of nodes in N 0 that could be the premiss(es) of some expansion rule other than blockable ones, its expansion(s) are also in N 0 .

For the aims of the present section, what is important to point out is that the following two properties must be guaranteed. The first of them is needed to prove termination, and the second is the saturation property for non-phantom nodes used to prove completeness.

1. The number of siblings of any node n is bounded by a function of the size of the initial formula. It is worth pointing out that in order for such a property to hold, it is essential that the conclusions of the ✷ and ✷ - rules are siblings of the respective minor premisses, and not the major one, because the latter (labelled by a universal formula) can in principle be used to produce an infinite number of expansions.

2. Let B be a complete and open branch. Then for any node or pair of nodes that could be the premiss(es) of some expansion rule other than blockable rules (without violating R3), its expansion(s) is (are) the label(s) of nonphantom node(s) in B. Considering in particular the A rule, this means that, whenever B contains a non-phantom node whose label has the form a: AF , then, for any nominal b occurring in some non-phantom node of B, the branch also contain a non-phantom node labelled by b: F .

So, the main subtlety in the extension to the global modalities is the definition of ≺ B . Like in the case of the other universal modalities, when a node (n) a: AF is expanded generating (m) b: F , it cannot be established that m and n are siblings w.r.t. ≺ B . Otherwise, it could not be ensured that a universal node has a bounded number of siblings (property 1 above). But, contrarily to the ✷ and ✷ -rules, the A rule lacks a minor premiss, to play the role of "producer" of the conclusion.

We cannot simply take the first node where the focused nominal occurs, to play the role of "minor premiss" of the A rule, for two reasons. Let us assume that a node n is expanded via the A rule producing the new node (m) b: F , and let k be the first node in the branch where b occurs. If k is the minor premiss of the inference, then m and k are siblings; this implies that if k is a phantom, then m is a phantom too, so that:

• restriction R1 does not prevent firing the A rule again and again on n focusing on the same nominal b;

• if b also occurs in a non-phantom node in the branch, the branch would not contain a non-phantom node labelled by b: F , while this is necessary in order to prove completeness (property 2 above).

The leading intuition in determining which node plays the same role for the A rule as the minor premisses of the ✷ and ✷ -rules, is to take it as the first non-phantom node containing the focused nominal, in the branch where the rule is applied (i.e. just before the addition of the new node).

Although this is quite a simple and intuitive idea, its formal definition is rather intricate, because the notion of "the first non-phantom node containing the focused nominal" depends on the notion of phantom node, which is in turn defined in terms of ≺ B . Luckily, there is no true circularity here, since, when properly defined, the relation ≺ B does not depend on the phantom nodes in B itself, but on the phantom nodes in the branch B ′ from which B is obtained by application of an expansion rule. Such a proper definition requires several notions to be defined simultaneously by induction on the sequence of branches B 0 , B 1 , . . . built during tableau construction. Definition 6. Let B 0 , B 1 , . . . , B i be a sequence of branches such that B 0 is the initial single-node tableau and for all j = 1, . . . , i, B j is obtained by application of an expansion rule to B j-1 . Then the notion of minor premiss of an application of the A rule, the relation ≺ Bi , and the set of directly and indirectly blocked nodes in B i are defined by induction on i as follows:

(i = 0) The relation ≺ B0 is empty, no nodes are blocked in B 0 , and, obviously, there are no minor premisses of applications of the A rule.

(i > 0) Let ≺ Bi-1
, the set of directly and indirectly blocked nodes in B i-1 , and the minor premisses of applications of the A rule up to B i-1 be defined. Then:

1. Each minor premiss of an application of the A rule in B i-1 is also the minor premiss of the same application of the A rule in B i . Moreover, if B i is obtained from B i-1 by means of an application of the A rule focusing on the nominal b, and if b occurs in some node which is non-phantom in B i-1 , then the minor premiss of the new application of the A rule in B i is the first non-phantom node in B i-1 where b occurs. Otherwise, if b occurs only in phantom nodes of B i-1 , such an application of the A rule has no minor premiss. 42. For any pair of nodes n, m in B i , n ≺ Bi m if either n ≺ Bi-1 m, or one of the following cases applies:

(a) B i is obtained from B i-1 by application of a blockable rule to n, which causes the addition of the node(s) m 0 (and m 1 ), and m = m i (i = 0, 1). (b) for some k, n ≺ Bi-1 k and B i is obtained from B i-1 by application of an expansion rule R ∈ {∨, @, ↓, ∧} to k, causing the addition of m to B i ; (c) for some k, n ≺ Bi-1 k and B i is obtained from B i-1 by application of an expansion rule R ∈ {✷, ✷ -} whose minor premiss is k, and causing the addition of m to B i ; (d) for some k, n ≺ Bi-1 k and B i is obtained from B i-1 by application of the A rule causing the addition of m to B i and k is the minor premiss of the A inference in B i .

3. The set of blocked nodes in B i is defined by induction on < as follows:

• n is blocked in B i if it is either directly or indirectly blocked in B i . • n is directly blocked by m in B i if it is a blockable node, m < n, m is not blocked in B i and label(m) can be mapped to label(n) in B i ; n is directly blocked in B i if it is directly blocked by some m in B i . • n is indirectly blocked (a phantom) if it is not directly blocked in B i
and it has an ancestor w.r.t.

≺ Bi which is blocked in B i .
The relation of being the minor premiss of an application of the A rule is static: if n is the minor premiss of a given application of the A rule in the branch B i , it stays the minor premiss of that rule application in B i+1 , even if n becomes a phantom in B i+1 (see Example 6 below). Consequently, the relation ≺ B is static: if a node is produced by an application of the A rule, its parent w.r.t. ≺ B is established according to the phantom/non-phantom status of the nodes in the branch just before the application of the rule. In particular, if n ❀ A m and the focused nominal of the A inference is a top nominal when the rule is applied, then m is a root node, since the minor premiss of the inference is the top node of the branch. The use of an auxiliary induction on < in item 3 of Definition 6 is required by the fact that blocks may change when a branch is expanded, therefore they must be determined again starting from the top node; also this fact is illustrated by Example 6.

With Definition 6, Lemma 1 still holds: ≺ B arranges the nodes of a branch B into a forest of trees, where any non-terminal node is a blockable node.

The application of the expansion rules are restricted by R1-R4 as before (keeping in mind that a node (n) a: EF is a blockable node). Moreover, the following restrictions are added: R5. a node (n) a: EF cannot be expanded in a branch B, if it already contains a non-phantom node labelled by b: F for some nominal b;

R6. the A rule cannot focus on a nominal which only occurs in phantom nodes in the branch.

Example 6. The following example shows how minor premisses of the A rule are computed, and the fact that the notion of minor premiss and the relation ≺ B are static, contrarily to direct and indirect blocks. It also shows that it may happen that the A rule is applied more than once to the same node, focusing on the same nominal. Figure 8 shows the development of a (still incomplete) one-branch tableau for the formula

F = a: (A↓x.a: x ∧ Ap ∧ A✸q)
The first application of the @ rule is not shown in the figure, and the two applications of the ∧ rule that follow are collapsed into one. In the example, the same notational conventions as in Section 3.3 are used. Moreover, when a node k is obtained by application of the A rule to a node n, with minor premiss m, we write (n, m) ❀ A k.

The branch B ′ on the right is obtained from the branch B on the left by application of the equality rule to node 17, replacing b 3 for a, and then expanded further on with the addition of the last two nodes. The focused nominal of the first application of the A rule in B is a, and the top node is the first non-phantom node where a occurs, so 0 is the minor premiss of the inference. Since 0 is a root node, 4 is also a root node. So, 0-4 are root nodes (both in B and B ′ ). When 4 is expanded, 4 ≺ B {5, 6} (and the relation remains the same in B ′ : 4 ≺ B ′ {5, 6}).

B (0) a 0 : F (1) a: A↓x.a: x 0 ❀ @,∧ 1 (2) a: Ap 0 ❀ @,∧ 2 (3) a: A✸q 0 ❀ @,∧ 3 (4) a: ✸q (3, 0) ❀ A 4 (5) a: ✸b 1 4 ❀ ✸ 5 (6) b 1 : q 4 ❀ ✸ 6 (7) b 1 : p (2, 5) ❀ A 7 (8) b 1 : ✸q (3, 5) ❀ A 8 (9) b 1 : ✸b 2 8 ❀ ✸ 9 (10) b 2 : q 8 ❀ ✸ 10 (11) b 2 : ✸q (3, 9) ❀ A 11 (12) b 2 : ✸b 3 11 ❀ ✸ 12 (13) b 3 : q 11 ❀ ✸ 13 (14) b 3 : ✸q (3, 12) ❀ A 14 (15) b 3 : ↓x.a: x (1, 12) ❀ A 15 (16) b 3 : a: b 3 15 ❀ ↓ 16 (17) a: b 3 16 ❀ @ 17 B ′ (0) a 0 : F [b 3 /a] (1) b 3 : A↓x.x: b 3 0 ❀ @,∧ 1 (2) b 3 : Ap 0 ❀ @,∧ 2 (3) b 3 : A✸q 0 ❀ @,∧ 3 (4) b 3 : ✸q (3, 0) ❀ A 4 (5) b 3 : ✸b 1 4 ❀ ✸ 5 (6) b 1 : q 4 ❀ ✸ 6 (7) b 1 : p (2, 5) ❀ A 7 (8) b 1 : ✸q (3, 5) ❀ A 8 (9) b 1 : ✸b 2 8 ❀ ✸ 9 (10) b 2 : q 8 ❀ ✸ 10 (11) b 2 : ✸q (3, 9) ❀ A 11 (12) b 2 : ✸b 3 11 ❀ ✸ 12 (13) b 3 : q 11 ❀ ✸ 13 (14) b 3 : ✸q (3, 12) ❀ A 14 (15) b 3 : ↓x.x: b 3 (1, 12) ❀ A 15 (16) b 3 : b 3 : b 3 15 ❀ ↓ 16 (17) b 3 : b 3 16 ❀ @ 17 (18) b 2 : p (2, 9) ❀ A 18 (19) b 3 : ✸q (3, 0) ❀ A 19
The minor premiss of the application of the A rule producing node 7 is the first non-phantom node where b 1 occurs in B 6 , i.e. 5. Node 5 is also the minor premiss of the application of the A rule producing 8, therefore also 4 ≺ B {7, 8}.

In the branch B, none of the blockable nodes 8, 11 and, later on, 14 are ever blocked by 4, because a is a top nominal in B. So, in particular, node 8 can be expanded, producing 9 and 10, and 8 ≺ B {9, 10}. Since 9 is the first non-phantom node where b 2 occurs in B 10 , the minor premiss of the A inference producing 11 is 9, and 8 ≺ B 11.

Node 18 , b 3 occurs in some non-phantom nodes, 3 is not a phantom and 14 is a phantom (so, there are no non-phantom nodes labelled by b 3 : ✸q); the A rule can be fired on 3 focusing again on b 3 , and producing 19. The minor premiss of the inference is the top node, therefore 19 is a root node.

In general, with the exception of the A rule, every node (or pair of nodes) can be expanded at most once in a branch. And a node cannot be expanded more than once by the A rule with the same minor premiss and the same focused nominal. What will be needed, in the sequel, is, however, only the one-time expandability property for blockable nodes, which was already pointed out in Section 3: Lemma 2. A blockable node is expanded at most once in a branch.

Proof. Let n be any blockable node. If either n ❀ ∇ (k 1 , k 2 ), for ∇ ∈ {✸, ✸ -}, or n ❀ E k 1 (i.e. n has already been expanded), then also n ≺ B k i (for i = 1, 2 or i = 1). A new expansion of n would not violate restrictions R2 and R5 only if k i is a phantom in the current branch (for i = 1, 2 or i = 1). But if k i is a phantom, then n is necessarily blocked, so that it cannot be expanded by either restriction R3 or R4. If, later on, n becomes non blocked again, then k i becomes non-phantom (for i = 1, 2 or i = 1), so that, again, either R2 or R5 forbids a second application of the blockable rule to n.

Thanks to restriction R6, any application of the A rule has a minor premiss. The necessity of this restriction to ensure termination is shown by the following example.

Example 7. Figure 9 shows a complete and open one-branch tableau for F = A↓x.Ex: p. In this branch B, 0, 1 and 2 are root nodes, 2 ≺ B {3, 4, 5, 6}, 6 ≺ B {7, 8, 9, 10}, and 10 ≺ B {11, 12}. In particular, the minor premiss of the application of the A rule producing node 1 is 0, which is a root node, therefore 1 is a root node too. The minor premiss of the inference producing node 5 is the first non-phantom node where a 1 (the focused nominal) occurs, i.e. node 3; since 2 ≺ B 3, 2 is also the parent of 5. Anagously, the minor premiss of the A inference producing 9 is node 7 (the first non-phantom node where a 2 occurs), therefore 6 ≺ B 9 because 6 ≺ B 7.

(0) a 0 : A↓x.Ex: p (1) a 0 : ↓x.Ex: p (0, 0) Nodes 6 and 10 are never blocked by 2 because a 0 is a top nominal and mappings do not act on top nominals. In B 10 , node 10 is not blocked by 6, because a 1 and a 2 are not compatible in B 10 : Φ 10 (a 1 ) = {p} = ∅ = Φ 10 (a 2 ). Therefore 10 can be expanded.

❀ A 1 (2) a 0 : Ea 0 : p 1 ❀ ↓ 2 (3) a 1 : a 0 : p 2 ❀ E 3 (4) a 0 : p 3 ❀ @ 4 (5) a 1 : ↓x.Ex: p (0, 3) ❀ A 5 (6) a 1 : Ea 1 : p 5 ❀ ↓ 6 (7) a 2 : a 1 : p 6 ❀ E 7 (8) a 1 : p 7 ❀ @ 8 (9)
But in B 12 , Φ 12 (a 1 ) = {p} = Φ 12 (a 2 ), i.e. a 1 and a 2 are compatible, therefore 10 is now blocked by 6, and its descendants w.r.t. the ≺ B relation, 11 and 12 become phantoms.

Since a 3 occurs only in phantom nodes in B 12 , the A rule cannot focus on it, by restriction R6. So the branch is complete.

In the absence of restriction R6, the A rule could be applied producing a new node labelled by a 3 : ↓x.Ex: p (node 13 below). Such an application of the A rule would lack a minor premiss (because a 3 does not occur in non-phantom nodes), therefore the new node would have no parents, i.e. it would be a root node. And the construction could go on as shown below. Node 14 (a sibling of 13) is also a root node. Before the addition of node 16, a 3 is not compatible with either a 1 or a 2 , therefore 14 can be expanded, and its children 15 and 16 are generated. Now (in B 16 ) 14 is blocked by 6, so 15 and 16 become phantoms. But, again, without restriction R6, the A rule could be applied with no minor premiss, and the new root node 17 could be added to the branch. Another neverending story, where nodes 13, 17 and all the infinitely many nodes generated by further applications of the A rule would be root nodes.

The following last example shows what may happen outside the decidable fragment FHL \ ✷↓✷.

Example 8. The expressive power of FHL allows for formulae whose models are necessarily infinite, such as, for instance:

A✸p ∧ A↓x.✷✷✸ -x ∧ A↓x.✷¬x
(every state has at least one successor, and the accessibility relation is transitive and irreflexive). Such a formula has no finite and complete tableau. Figure 10 shows a one-branch tableau for its subformula F = A✸p ∧ A↓x.✷✷✸ -x.

When node 15 is expanded, it produces nodes (16) c: ✸b 1 and (17) c: a. The equality rule, applied to 17, replaces everywhere c with a. Since c occurs only in nodes 16 and 17, we have shown the changed labels to the right of such nodes only.

Branch construction never terminates because there is an infinite number of formulae of the form b i : ✷F occurring in the branch. In particular, every nominal b i labels different instances of ✷✷✸ -x and ✷✸ -x, therefore, if i = j, b i is not compatible with b j . Consequently, no node labeled by b i : ✸p is ever blocked.

In this case, the infinite construction could be avoided by a smarter form of loop checking, realizing that actually all nominals could denote the same state. But any complete branch for F ∧ A↓x.✷¬x would also contain, for all i, nodes labelled by b i : ¬a and b i : ¬b j for all j < i. We conclude this section formalizing two simple properties that will be used later on. Lemma 3. For any branch B: It is worth remarking that the first item of the above lemma holds, in particular, when either m or m ′ is added by an application of the A rule: if k is the minor premiss of the inference leading to the addition of m (or m ′ ), then also n ≺ B k, and k has the same phantom/non-phantom status in B as m and m ′ .

(0) F (1) a: A✸p 0 ❀ ∧ 1 (2) a: A↓x.✷✷✸ -x 0 ❀ ∧ 2 (3) a: ✸p (1, 0) ❀ A 3 (4) a: ↓x.✷✷✸ -x (2, 0) ❀ A 4 (5) a: ✸b 0 3 ❀ ✸ 5 (6) b 0 : p 3 ❀ ✸ 6 (7) a: ✷✷✸ -a 4 ❀ ↓ 7 (8) b 0 : ✷✸ -a (7, 5) ❀ ✷ 8 (9) b 0 : ✸p (1, 5) ❀ A 9 (10) b 0 : ↓x.✷✷✸ -x (2, 5) ❀ A 10 (11) b 0 : ✷✷✸ -b 0 10 ❀ ↓ 11 (12) b 0 : ✸b 1 9 ❀ ✸ 12 (13) b 1 : p 9 ❀ ✸ 13 (14) b 1 : ✷✸ -b 0 (11, 12) ❀ ✷ 14 (15) b 1 : ✸ -a (8, 12) ❀ ✷ (16) c: ✸b 1 ⇒ = a: ✸b 1 15 ❀ ✸ 16 (17) c: a ⇒ = a: a 15 ❀ ✸ 17 (18) b 1 : ✸p (1, 12) ❀ A (19) b 1 : ↓x.✷✷✸ -x (2, 12) ❀ A (20) b 1 : ✷✷✸ -b 1 19 ❀ ↓ 20 . . . . . .
1. if n ≺ B m and n ≺ B m ′ , then m is a phantom in B if and only if m ′ is a phantom in B;

Termination and Completeness

The tableau calculus defined in Sections 3 and 4 is trivially sound. This section shows that the calculus terminates and is complete, provided that the initial formula is in the fragment FHL \ ↓✷, i.e. is a NNF formula where no universal operator (✷, ✷ -and A) occurs in the scope of a binder. In this section we always assume that the initial formula is a ground formula in such a fragment.

For the purposes of proving termination and completeness, the main property of the considered fragment is that, if a universal formula is a subformula of the initial formula, then it contains no free variables, because it is not in the scope of a binder. As a consequence, for any node label of the form a: G where G is a universal formula, the only nominals occurring in G are top nominals. The first result proved below establishes this fact, along with the standard subformula property.

Definition 7. Let B be a tableau branch and a 0 : F 0 its top formula. Then Subf(B) is the set of the subformulae of F 0 and

Cmp(B) = (Subf(B) ∩ PROP) ∪ {✷G | ✷G ∈ Subf(B)} ∪{✷ -G | ✷ -G ∈ Subf(B)}
Lemma 4 (Subformula properties). For any formula a: F occurring in a branch B which is not a relational formula, F is an instance of a formula in Subf(B). Moreover, if F is a universal formula, then F ∈ Subf(B). Therefore, in particular, for any nominal a, Φ B (a) = {F | a: F ∈ B} ∩ Cmp(B).

Proof. The proof is an induction on the construction of B, which simultaneously proves the following strongest versions of the two properties: if (n) a: F is a node in B and a: F is not a relational formula, then for any subformula F ′ of F : (α) F ′ is an instance of a formula in Subf(B), and

(β) if F ′ is a universal formula, then F ′ ∈ Subf(B).
The one-node branch constituting the initial tableau trivially enjoys the required properties. Below, we show that they are preserved by the expansion rules, assuming that B is obtained from B ′ by application of the rule R. We consider different cases according to the rule R, restricting our attention to the node labels which are either added or modified by R.

1. R is one of the rules ∧, ∨, @, E, applied to (m) b: H, and the node (n) a: F is added to the branch. Then F is a subformula of H, for which α and β hold by the inductive hypothesis; therefore α and β hold for F too, since any subformula of F is also a subformula of H.

2. R = ↓, and the node (n) a: F , where F = G[a/x], is added as the expansion of (m) a: ↓x.G. By the inductive hypothesis, ↓x.G is an instance of some formula ↓x.G ′ ∈ Subf(B). Therefore G[a/x] is an instance of G ′ , which belongs to Subf(B), too. So, α holds for F . Moreover, in the fragment FHL \ ↓✷, F has no universal subformula, so that β is vacuously true.

3. R = ✸ and the nodes (k) b: ✸a and (n) a: F are added as expansions of (m) b: ✸F . The label of k is a relational formula, so only the node n has to be considered. The same reasoning as in case 1 shows that α and β hold for F .

4. If R = ✸ -, the reasoning is the same as in 3, modulo replacement of label(m) by b: ✸ -F and label(k) by a: ✸b.

5. R = ✷, and the rule is applied to (m) b: ✷F and (k) b: ✸a, generating the node (n) a: F . By the inductive hypothesis, ✷F ∈ Subf(B), hence also all the subformulae of ✷F (including F and its subformulae) are in Subf(B). So, α and β hold for F .

6. If R = ✷ -, the reasoning is the same as in 5, but for the fact that label(m) = b: ✷ -F , label(k) = a: ✸b, and the inductive hypothesis ensures that ✷ -F ∈ Subf(B).

7. R = A, and the rule is applied to (m) b: AF , generating the node (n) a: F . By the inductive hypothesis, AF ∈ Subf(B), hence also all its subformulae are in Subf(B). So, α and β hold for F .

F ′ is an instance of a subformula G of F 0 , consequently F ′ [b/c] is an instance of G[b/c], which is a subformula of F 0 [b/c].
Moreover, by the inductive hypothesis, if F ′ is a universal formula, then it is a subformula of F 0 . Therefore,

F ′ [b/c] is a subformula of F 0 [b/c].
If B is any branch in a tableau for F 0 (a 1 , . . . a n ), i.e. a tableau initialized with (n 0 ) a 0 : F 0 (a 1 , . . It is worth pointing out that the use of substitution to treat nominal equalities is essential for this key property to hold. If some kind of "copy rule" were used instead, any complete branch containing an equality a: b and a node labelled by a formula of the form c: ✷F (a), would contain also c: ✷F (b), and, in general, F (b) cannot be ensured to be a subformula of the top formula. Since (at this stage of the proof) the number of nominals occurring in the branch is unbounded, a branch might contain an unbounded number of equalities a : b i , thus an unbounded number of labels of the form c: ✷F (b i ).

Termination

In order to prove termination, we first show that, in the forest of trees induced by ≺ B on the nodes of a branch B, any node has a bounded number of siblings. Let us observe that it would not suffice to show that the number of formulae that can label the siblings of a given node is bounded, because, in principle, a given formula might be the label of an infinite number of nodes (a branch is not a set of formulae), notwithstanding restriction R1. This could happen when distinct node labels become equal by effect of substitution, as already remarked in Section 3 (Example 2).

The relation ✄, which is defined next, introduces an order on the siblings of a given node. Definition 8. Let n, m and k be nodes in B.

• If n ❀ R m, for R = ∧, ∨, @, ↓, then n ✄ m;

• if (m, n) ❀ R k, where R ∈ {✷, ✷ -}, and n is the minor premiss of the inference, then n ✄ k;

• if k ❀ A m and n is the minor premiss of the inference, then n ✄ m.

✄ * is the reflexive and transitive closure of ✄. If n✄ * m, we say that n produces m.

In what follows, |F | is the size of the formula F , counted as the number of symbols in F . Below, we tacitly exploit the trivial fact that the size of the top formula of any branch is the same as the size of the initial formula of the tableau.

The proof of next lemma, which bounds the number of nodes produced by a given node, makes use of the following definition. Definition 9. Let M be a set of nominals, F a formula (possibly containing free variables) and ∆ a set of formulae.

1. Clo(∆) (the closure of ∆) is the set containing all the subformulae of every formula in ∆.

2. An M -instance of F is a ground formula that can be obtained from F by replacing its free variables with elements of M . Proof. As already remarked, Σ(n) may contain nodes labelled by the same formula, so the reasoning is not as simple as it would be if dealing with sets of formulae. However, as shown below, the label of any node in Σ(n) has a matrix taken from a bounded stock of formulae, that is built in the language of the branch at the time n is added to it. Node labels with the same matrix are always equal, at any construction stage of the branch, so that the cardinality of Σ(n) is bounded by the number of such possible matrices.

Any branch B in a tableau is the last element of a sequence of branches, where the first one is the initial tableau, and each of the others is obtained from the previous one by application of an expansion rule. Such a sequence will be called the sequence of branches leading to B.

Let n be any fixed node in a tableau branch B. We shall use the following notations:

1. B 1 is the first branch where n occurs, in the sequence of branches leading to B, and the sequence B 1 , B 2 , . . . , B p = B denotes the subsequence of the sequences of branches leading to B which starts from B 1 .

label

Bi (k) is the label of the node k in the branch B i . This allows one to refer to node labels in different branches.

3. For 1 ≤ i ≤ p, σ i is the composition of the sequence of substitutions applied in the sequence B 1 , . . . , B p , by means of the equality rule, up to B i included. Consequently, for each i > 0, label Bi (n) = σ i (label B1 (n)).

4. M n is the set containing all the nominals occurring in label B1 (n) and all the top nominals in B 1 .

5. Γ n , ∆ n and S n are the sets of formulae defined as follows:

Γ n = {F | F is a universal subformula of the top formula of B 1 } ∆ n = {label B1 (n)} ∪ Γ n S n = (Clo(∆ n )) Mn
i.e. S n contains all the M n -instances of every formula in the closure of ∆ n .

6.

F n = {a: F | a ∈ M n and F ∈ S n } ∪ {a: ✸b | a, b ∈ M n }.
Any element of F n will be called a matrix. Note that only nominals in M n may occur in a matrix.

7. N is the size of the top formula of B, which is obviously equal to the size of the initial formula of the tableau.

It is easy to see that |M n | ≤ N . This holds because, if a 0 : F 0 is the top formula of B 1 , |M n | cannot exceed 1 (for the outermost nominal in label B1 (n)) + the sum of the number of top nominals and the number of variables occurring in a 0 : F 0 (by Lemma 4). Such a sum is not greater than N -1 (the number of symbols in F 0 ) plus 1 for the outermost nominal a 0 .

Moreover, |S n | ≤ N N +2 . This holds because the cardinality of ∆ n is not greater than N , since |Γ n | < N (the top formula of B 1 is not a universal formula, but a satisfaction statement). The size of each element of Γ n is bounded by N , and the same holds for label B1 (n), by Lemma 4. Therefore the set Clo(∆ n ) has no more than N 2 elements. Each element of Clo(∆ n ) has no more than N free variables, and each free variable can be instantiated with elements of M n in no more than N different ways. Therefore, every element of Clo(∆ n ) has no more than N N M n -instances, so that the cardinality of S n is bounded by

N N +2 . Consequently, |F n | ≤ E w (N ) = N 2 + N N +3 :
for each formula a: H with a ∈ M n and H ∈ S n there are no more than N choices for the nominal a and no more than N N +2 choices for the formula H; therefore the cardinality of {a: H | a ∈ M n and H ∈ S n } is bounded by N N +3 . And formulae of the form a: ✸b with a, b ∈ M n can be built in at most N 2 different ways.

Let m be any node in Σ(n

), i.e. n ✄ * m. An element F of F n is called a matrix of m in B i if label Bi (m) = σ i (F ); and F is a matrix of m if it is a matrix of m in all B i
where m occurs, for i = 1, . . . , p. If two nodes m 1 and m 2 have a same matrix, then obviously for all i = 1, . . . , p such that both m 1 and m 2 are in B i , label Bi (m 1 ) = label Bi (m 2 ).

We first prove that:

(α) the label of any node in Σ(n) has a matrix in F n . I.e. if m ∈ Σ(n), then there exists F ∈ F n such that for all i = 1, . . . , p, if m ∈ B i then label Bi (m) = σ i (F ).

The proof is by induction on i. If i = 1 then necessarily m = n, σ 1 = Ø and label B1 (n) ∈ F n . Otherwise, if i > 1, we consider different cases according to the rule applied to obtain B i from B i-1 . Note that in all cases, except for the first one, σ i = σ i-1 and label Bi (m) = label Bi-1 (m) for any node m occurring in B i-1 . Therefore, in all but the first case, a matrix of any node m occurring in B i-1 is still a matrix of m in B i . Therefore, the thesis must be proved only for the newly added nodes; since such nodes do not occur in B j for j < i, it is sufficient to show that they have a matrix in B i . In the treatment of such cases we assume that m is any node in B i which does not belong to B i-1 .

(=) Let m be any node in Σ(n), and let B i be obtained from B i-1 by an application of the equality rule. By the induction hypothesis, there is a formula F ∈ F n such that label Bj (m) = σ j (F ) for all j = 1, . . . , i -1 such that m ∈ B j . We show that any matrix of m in B i-1 is also a matrix of m in B i , so any matrix of m in B 1 , . . . B i-1 , is also a matrix of m in B i .

If B i-1 is expanded by means of the equality rule replacing a with b, then label This holds because, if m ✄ k, then either m and k are both root nodes (and they are both non-phantom) or they are children, w.r.t. ≺ B , of a same node. In the latter case, m and k have the same phantom/non-phantom status (by item 1 of Lemma 3).

Bi (m) = (σ i-1 (F ))[a/b]. Since σ i = σ i-1 •{a/b}, label Bi (m) = σ i (F ), therefore F is still a matrix of m in B i . (∧, ∨) Let n ✄ * k ❀ R m, for R ∈ {∧, ∨}, with label Bi (k) = a: F ′ 1 ⋆ F ′ 2 (for ⋆ ∈ {∧, ∨}), and label Bi (m) = a: F ′ j (j = 1, 2). By the induction hypothesis, since k occurs in B i-1 , a: F ′ 1 ⋆ F ′ 2 = σ i-1 (c: F 1 ⋆ F 2 ) = σ i (c: F 1 ⋆ F 2 ) for some c: F 1 ⋆ F 2 ∈ F n , i.e. c ∈ M n and F 1 ⋆ F 2 ∈ S n . Since S n is closed w.r.t. subformulae, F j ∈ S n , therefore c: F j ∈ F n . Finally, label Bi (m) = a: F ′ j = σ i (c: F j ), therefore c: F j is a matrix of m in B i . (@) Let n✄ * k ❀ @ m,
: F ′ [a/x] = σ i (c: F [c/x]), therefore c: F [c/x] is a matrix of m in B i . (✷) Let n ✄ * k and (k ′ , k) ❀ ✷ m, with label Bi-1 (k ′ ) = label Bi (k ′ ) = a: ✷G, label Bi-1 (k) = label Bi (k) = a:
We can now prove that the cardinality of Σ(n) is bounded by E w (N ), where E w (N ) is the cardinality of F n . Let us assume, by reductio ad absurdum, that Σ(n) has more than E w (N ) elements. Then, by α, there are at least two distinct elements m 1 and m 2 in Σ(n) which have the same matrix F . We may assume w.l.g. that n ≤ m 1 < m 2 . Let B k be the first branch in the sequence B 1 , . . . , B p where m 2 occurs. Since n < m 2 , there is a node k ∈ Σ(n) such that n ✄ * k ✄ m 2 . Given that k produces a node, it is not the major premiss of a universal rule. Moreover, it is not a phantom in B k-1 : a phantom node cannot be the minor premiss of an application of the A rule producing m 2 , nor can it be expanded by one of the other rules without violating restriction R3.

Consequently, by β, m 1 is not a phantom in B k-1 either. But label B k (m 2 ) = σ k (F ) = σ k-1 (F ) = label B k-1 (m 1 ) (σ k = σ k-1 because, clearly, B k-1
has not been expanded by means of the equality rule, which does not add new nodes to the branch). Therefore, the addition of m 2 to B k-1 violates restriction R1.

The next result states that the forest of trees induced by ≺ B on any branch B has a bounded number of trees, and each tree has bounded width. Lemma 6. Let B be a branch in a tableau for F , and let E w (N ), where N = |F |, be the bound given by Lemma 5.

• The number of root nodes in B is bounded by E w (N ).

• For any node n of B, the cardinality of the set of the children of n, i.e. the set

Γ B (n) = {m | n ≺ B m}, is bounded by 2 × E w (N ).
Proof. The first item follows from Lemma 5, since all root nodes are produced by the top node n 0 , i.e. n is a root node only if n 0 ✄ * n. This is due to restriction R6, which guarantees that every application of the A rule has a minor premiss, so that an application of this rule produces a root node only if its minor premiss is a root node.

The second item also follows from Lemma 5, using Lemma 2. The relation n ≺ B m holds if and only if either n ❀ R m, where R is a blockable rule or else there is a node s such that n ≺ B s and s ✄ m. Equivalently, n ≺ B m if and only if for some node k: n ❀ R k, where R is a blockable rule, and k ✄ * m. By Lemma 2, there are at most two nodes k 1 and k 2 such that n ❀ R k i (i.e. n is expanded at most once in the branch). By Lemma 5, each of them has at most E w (N ) siblings, so that the number of children of n is bounded by 2 × E w (N ).

Next, we show that any tree in the forest induced by ≺ B on the nodes of B has a bounded depth. To this aim, we define an equivalence relation among node labels. Definition 10. Let F be a ground formula containing exactly the non-top nominals a 1 , .., a n . Let W = {w 1 , w 2 , . . . , w n } be a set of fresh variables, and let µ be a bijection from {a 1 , .., a n } onto W . A skeleton F S for F is the formula obtained from F by replacing every nominal a j by µ(a j ).

Since a skeleton for a given formula is unique up to free variable renaming, we shall speak of "the skeleton" of a formula, and we consider two skeletons identical if they only differ for the choice of free variable names.

Example 9. The formulae a 1 : ✸↓x.(✷x ∧ ¬a 1 ) and a 2 : ✸↓x.(✷x ∧ ¬a 2 ) have the same skeleton w 1 : ✸↓x.(✷x ∧ ¬w 1 ) (assuming that neither a 1 nor a 2 is a top nominal). However, a 1 : ✸↓x.(✷x ∧ ¬a 2 ) has a different skeleton, that is w 1 : ✸↓x.(✷x ∧ ¬w 2 ). Moreover, if a 3 is a top-nominal, then a 1 : ✸↓x.(✷x ∧ ¬a 3 ) has yet another skeleton, namely w 1 : ✸↓x.(✷x ∧ ¬a 3 ). Definition 11. Let B be a tableau branch, and F 1 , F 2 two node labels in B. Then F 1 ≈ B F 2 if and only if:

1. F 1 and F 2 have the same skeleton F S (w 1 , . . . , w n );

2. if µ i (i = 1, 2)
is the bijection from the non-top nominals in F i onto {w 1 , . . . , w n } establishing that F S is the skeleton of F i , then for all j = 1, . . . , n, µ - 1 (w j ) and µ - 2 (w j ) are compatible in B. The relation ≈ B is obviously an equivalence relation on the (ground) formulae occurring as node labels in B.

The next result establishes a bound on the number of possible skeletons for node labels in a tableau branch. Lemma 7. Let B be a branch whose top formula is F 0 , and N = |F 0 |. The number of distinct possible skeletons for blockable node labels in B is bounded by

N N +1 .
Proof. By Lemma 4, the body of any blockable node label is an instance of a subformula of F 0 (because relational formulae are not blockable). 5Let {a 1 , . . . , a n } be the set of the top nominals of the branch and {x 1 , . . . , x m } the set of the variables occurring in F 0 . Clearly, n + m < N . Let moreover {w 0 , . . . , w m } be a set of fresh variables.

Any skeleton of a blockable node of B is obtained from an expression of the form x 0 : F , where F is a subformula of F 0 and x 0 is a new variable, by replacing the variables x 0 , x 1 , . . . , x m with elements of the set V = {a 1 , . . . , a n , w 0 , . . . , w m }. Since |V | ≤ N , there are no more than N N distinct sequences of length N made up of elements of V . Moreover, the number of variables in the formula x 0 : F is not greater than N , therefore there are at most N N skeletons for node labels having an instance of F as their body.

Since the number of subformulae of F 0 is bounded by N , the number of skeletons for blockable nodes of B is bounded by N × N N . Lemma 8. Let B be a branch and N the size of its top formula. The maximal number of equivalence classes w.r.t. ≈ B of blockable node labels is bounded by an exponential function E d (N ).

Therefore the size of any set S of blockable formulae which may occur in a tableau branch B, and such that for any pair of its elements F, G ∈ S, F is not blocked by G in B, is bounded by E d (N ).

Proof. Let F s (w 1 , . . . , w k ) be the skeleton of a node label in B, and ν the cardinality of Cmp(B) (see Definition 7). Clearly, k ≤ N and ν ≤ N . By Lemma 4, for any nominal a occuring in B, Φ B (a) = {F | a: F ∈ B} ∩ Cmp(B). Therefore, for each of the (at most) k nominals a 1 , . . . , a k replacing the variables w 1 , . . . , w k in F s (w 1 , . . . , w k ), there are at most 2 ν possible sets Φ B (a i ), so that there are at most 2 k×ν ≤ 2 N 2 node labels in B sharing the same skeleton F s (w 1 , . . . , w k ) but pairwise not equivalent w.r.t. ≈ B . By Lemma 7, the number of different skeletons for blockable node labels in B is N N +1 . Therefore, the number of equivalences classes w.r.t. ≈ B of blockable node labels, and consequently the cardinality of the set S, is bounded by

E d (N ) = N N +1 × 2 N 2 .
Definition 12. A chain in a branch B is a sequence of nodes n 1 , n 2 . . . such that for all i: n i ≺ B n i+1 . If a chain n 1 , . . . , n k is finite and n 1 is a root node, we say that it is the maximal chain leading to n k .

We recall that, by Lemma 1.1, for any given node n there is exactly one maximal chain leading to n. Lemma 9. Let B be a tableau branch and N the size of its top formula. Then for any chain

n 1 ≺ B n 2 ≺ B . . . ≺ B n k k ≤ E d (N ) + 1
, where E d (N ) is the bound given by Lemma 8.

Proof. We note beforehand that if n ≺ B m, then:

• n < m in the branch;

• n is a blockable node. Therefore in any chain

n 1 ≺ B n 2 ≺ B . . . ≺ B n k , for all i = 1, . . . , k -1, n i is a blockable node (Lemma 1.2).
Let us assume that a branch B contains a chain

n 1 ≺ B n 2 ≺ B . . . ≺ B n K ≺ B n E d (N )+1 .
We show that such a chain cannot be extended.

If n E d (N )+1 is not a blockable node, the chain cannot be extended, by definition of ≺ B .

Otherwise, for all i = 1, . . . , E d (N )+1, the label of n i is a blockable formula, so, by Lemma 8, there are at least two indexes 1

≤ i < j ≤ E d (N ) + 1 such that n i blocks n j in B. If j = E d (N ) + 1, then n E d (N )+1
is directly blocked and cannot be expanded, by restriction R4. Otherwise, if j ≤ E d (N ), then n j is directly blocked by n i ; so, n E d (N )+1 is a phantom in B and it cannot be expanded either, by restriction R3. Hence, in any case, no node

n E d (N )+2 such that n E d (N )+1 ≺ n E d (N )+2 can be generated.
Theorem 1 (Termination). Every tableau branch has a bounded depth and tableau construction always terminates.

Proof. By Lemmas 1.1, 6 and 9, the nodes of a branch B are arranged by ≺ B in a bounded sized set of trees, each of which has bounded width and bounded depth. Hence any tableau branch B has a number of nodes that is bounded by the size of the initial formula.

Since every rule (except for the equality rule) adds some node to the current branch, the only reason why tableau construction might not terminate is that the equality rule is applied an infinite number of times. But this is absurd, since every application of such a rule reduces the number of nominals occurring in the branch.

The considerations underlying the termination argument establish a bound on the number of nodes in a tableau branch in function of the size N of its top formula. The nodes are arranged by ≺ B in at most E w (N ) trees, each of which has a width bounded by E w (N ) (Lemma 6) and a depth bounded by E d (N ) (Lemma 9). The functions E w and E d are exponential in the size of the input formula, therefore the number of nodes in a single branch is bounded by a doubly exponential function. As a consequence, according to the bounds given above, the decision procedure defined in this paper is not worst-case optimal, since the satisfiability problem for FHL \ ↓✷ is in 2ExpTime [START_REF] Cate | On the complexity of hybrid logics with binders[END_REF].

As a matter of fact, the worst-case complexity of the calculus has the same order of magnitude as that which can be inferred from the termination proofs of other calculi for binder-free Hybrid Logic with the converse and global modalities, based on ancestor nominal blocking with indirect blocking (such as the systems defined in [START_REF] Bolander | Termination for hybrid tableaus[END_REF][START_REF] Cerrito | Nominal substitution at work with the global and converse modalities[END_REF][START_REF] Kaminski | Terminating tableau systems for hybrid logic with difference and converse[END_REF]). Whenever (i) the argument showing finiteness of tableau branches relies on a tree-like ordering of elements (either nodes or nominals), (ii) blocking requires comparison of some sets of formulae associated to elements of the same chain, and (iii) the elements of such sets are taken from the set S of the subformulae of the initial formula, tree depth may reach, in general, the number of subsets of S. Therefore the trees can be exponential in depth and doubly exponential in total. This is the case also for the calculus presented in this paper, so that restriction to binder-free formulae does not decrease the order of magnitude of its worst-case complexity. Although the width of the trees induced by ≺ B becomes polynomial in the size of the initial formula, their depth stays exponential. The smaller bound for tree width is due to the fact that, without variables, the only instance of a formula F is F itself, therefore the cardinality of the set S n defined in Lemma 5 is polynomial. However, there still may be an exponential number of nominals pairwise incompatible, thus an exponential number of unblocked nodes in a ≺ B chain.

We conclude the above considerations on complexity with a brief comparison with the tableau calculus for the clique guarded fragment proposed in [START_REF] Hirsch | A tableau algorithm for the clique guarded fragment[END_REF] (some features shared by that calculus and ours will be pointed out in Section 6). Contrarily to the resolution method for guarded clauses defined in [START_REF] Ganzinger | A superposition decision procedure for the guarded fragment with equality[END_REF], the tableau system given in [START_REF] Hirsch | A tableau algorithm for the clique guarded fragment[END_REF] is not worst-case optimal either. The system nondeterministically builds a tree (called completion tree), whose nodes are labelled by sets of formulae. In order to block a node, its whole content must be compared with the content of the blocking node. The bound given in the paper to the branching factor of a completion tree (and the cardinality of each node) is exponential in the size of the initial formula -like the width of our ≺ B treeswhile tree depth is bounded by a doubly exponential function. Therefore, the bound on the number of nodes in a completion tree established by the termination proof given in [START_REF] Hirsch | A tableau algorithm for the clique guarded fragment[END_REF] is exponentially higher than the maximum number of nodes in a branch of our tableaux.

Completeness

Completeness will be proved in the standard way, by showing how to define a model of the initial formula from a complete and open tableau branch. However, for the calculus introduced in this work, the fact that the labels of blocked and blocking nodes are not identical must be taken into account. This means that the "witness" (see Definition 13 below) of the blocking node cannot be taken as a witness of the blocked one, and, in general, the branch may contain no nominal that could be used as a witness of the blocked node. Nor can a model be simply built from a set of states consisting of equivalence classes of nominals, where two nominals are in the same class whenever some blocking mapping maps one to the other. Consider, for instance, Example 1 in Section 3, where node 17, labelled by a formula of the form c: ✸ -F (c) is blocked by [START_REF] Ganzinger | A superposition decision procedure for the guarded fragment with equality[END_REF] b: ✸ -F (b). The branch is open and complete, but a model cannot directly be extracted from it, making b and c denote the same state: although c and b are in some sense identified by the mapping used to block node 17, they cannot denote the same state in the model, because the presence of node (13) c: ¬b forces them to denote distinct states.

Thus, we follow a different approach, showing that a (possibly infinite) model can be built out of a complete and open branch B by means of a preliminary infinitary extension N ∞ B of a subset of B. Let C be the set containing all the nodes of B whose label have the form a: F , for a occurring in some non-phantom node in B and F ∈ Cmp(B) (see Definition 7), and N 0 be the union of C and the set of the non-phantom nodes of B. We inductively construct an infinite sequence of finite extensions of N 0 : N 0 ⊆ N 1 ⊆ N 2 , . . . . Each N i is associated an order < i and a set of triples B i , that will be called the blocking relation for N i . At each stage in the construction, new nodes can be added to obtain N i+1 from N i . Each of them "corresponds" to some node n ∈ N 0 (its label is a renaming of label(n)). If some node added at stage i corresponds to the node n ∈ N 0 , it will be denoted by n i . For the sake of generality, a node n ∈ N 0 is identified with n 0 . Moreover, each stage i > 0 introduces at most one new nominal, for which the meta-notation b i will be used. For any i, each triple in the blocking relation B i for N i has the form (n q , m, π), where n q and m are distinct nodes in N i and π is an injective function from non-top nominals occurring in m to non-top nominals occurring in n q .

The following definition introduces the notion of witness of a blockable node occurring in a set N i .

Definition 13 (Witness). A nominal b is a witness in N i of a blockable node n ∈ N i if one of the following cases holds: The next subsection details the construction of the sets N i and the corresponding relations < i and B i , while Subsection 5.2.2 establishes some important properties of these sets and uses them in order to build the required model.

Unravelling the blockings

Let B be a complete and open tableau branch. Below, we show how to construct the sequence of sets of nodes S B : N 0 ⊆ N 1 ⊆ N 2 . . . and the associated order < i and relation B i , where N 0 includes the top node of B. The construction also shows that the following invariants are satisfied, for any i:

1. if (n q , m, π) ∈ B i (q ≥ 0), then: (c) the formulae labelling n q and m are blockable formulae and π(label(m)) = label(n q ); 2. for any node n q ∈ N i , if n q has no witness in N i , then (n q , m, π) ∈ B i , for some m and π.

The elements N i of S B , and the associated relations < i and B i , are defined inductively as follows. The proof that the above stated invariants hold goes along with the inductive construction of the sets.

Base: i = 0. N 0 is the union of the set of non-phantom nodes in B and the set C = {n ∈ B | label(n) = a: F, a occurs in some non-phantom node in B and F ∈ Cmp(B)}

The relation < 0 is <, i.e. the total order on nodes in the sequence B, and

B 0 = {(n, m, π) | n is directly blocked by m in B via the mapping π}
It is worth recalling that, according to definition 6, a node n cannot be both directly blocked and a phantom; therefore, if n is directly blocked in B, then it belongs to N 0 . Obviously, all the invariants hold here.

Inductive

Step (i > 0). We assume that the invariants hold for i -1.

(Case 1.) If B i-1 = Ø then N i = N i-1 , B i = Ø = B i-1 and < i =< i-1 .
(Case 2.) Otherwise, let n p be the first node in N i-1 , according to the order < i-1 , such that (n p , m, π) ∈ B i-1 for some m ∈ N 0 and mapping π. Let label(n p ) = a 0 : ∇F (a 1 , . . . , a k )

where ∇ ∈ {✸, ✸ -, E} and a 1 , . . . , a k are all the non-top nominals occurring in F .

By the invariant 1a, m ∈ N 0 and it is not blocked in B, and by the invariants 1b and 1c, label(m) has the form c 0 : ∇F (c 1 , . . . , c k ) where for j = 0, . . . , k, π(c j ) = a j . I.e. , π is a subset of {a 0 /c 0 , . . . , a k /c k }. By an abuse of notation, we shall however denote π by {a 0 /c 0 , . . . , a k /c k } itself, although, possibly, for some a i , a i = c i .

Since m is not blocked in B and B is complete, B contains a non-phantom node k 2 such that label(k 2 ) = b: F (c 1 , . . . , c k ) and, if ∇ ∈ {✸, ✸ -}, also a nonphantom node k 1 labelled by either c 0 : ✸b or b: ✸c 0 , according to the case. Since k 2 is non-phantom, it belongs to N 0 , thus to N i-1 ⊇ N 0 ; similarly for k 1 .

Let b i be a fresh nominal. A mapping θ i , that will guide the construction of the new nodes of N i , is then defined as follows:

• θ i (c j ) = π(c j ); • If b ∈ {c 0 , . . . , c k }, then θ i (b) = b i . • θ i (d) = d if d ∈ {b, c 0 , . . . , c k }
In other words:

θ i = {a 0 /c 0 , . . . , a k /c k } if b ∈ {c 0 , . . . , c k } {a 0 /c 0 , . . . , a k /c k , b i /b} otherwise
Clearly, the mapping θ i is injective, and the nominal b is a witness of m. If b was created by a blockable rule, at the time of its first appearance it was obviously fresh w.r.t. to the current branch, but it may subsequently have been replaced by some c i by the equality rule.

N i is defined as the union of N i-1 with

{(k i ) θ i (G) | (k) G ∈ N 0 and no node in N i-1 labels θ i (G)}
N i is thus obtained from N i-1 by addition of a finite number of nodes k i , where each k i corresponds to a node k in N 0 (its label is a "copy" of label(k) modulo the renaming θ i ).

In particular, N i contains, for some nominal d and some j ≥ 0 (possibly, j = i): (k j 2 ) d: F (a 1 , . . . , a k ) (where either d = b i is a fresh nominal or d = a q for some q), and, if ∇ = E, it contains also either (k j 1 ) a 0 : ✸d or (k j 1 ) d: ✸a 0 , according to the form of label(n p ). Hence, N i has a witness for (n p ) a 0 : ∇F (a 1 , . . . , a k ).

The order < i on nodes in N i is the extension of < i-1 where n j < i m i if j < i, and n i < i m i if n < 0 m.

Next, the set B i is defined, representing the blocking relation in N i . In the sequel, if F is a formula and γ is a mapping from nominals to nominals, the restriction of γ to the nominals occurring in F , γ | F , is:

γ | F (a) = γ(a) if a occurs in F a otherwise
The notation G(d 1 , . . . , d n ) will sometimes be used to denote a formula G where some of the non-top nominals d 1 , . . . , d n may occur (beyond other nominals). If π is a mapping that is the identity for nominals not in {d 1 , . . . , d n }, the application of π to G will be denoted by G(π(d 1 ), . . . , π(d n )). Now, let S be the set of all the new nodes

(q i ) θ i (G(c 0 , c 1 , . . . , c k , b)) = (q i ) G(a 0 , a 1 , . . . , a k , θ i (b))
added at stage i and such that G is a blockable formula with no witness in N i . For any node q i ∈ S, a blocking node β q i and blocking mapping µ q i are defined. Let us consider any q i ∈ S, with label θ i (G(c 0 , c 1 , . . . , c k , b)). Since q i is added at stage i, there is a node k ∈ N 0 labelled by G(c 0 , c 1 , . . . , c k , b), such that q i corresponds to k. The node k has no witness in N 0 : let us assume that label(k) = G(c 0 , c 1 , . . . , c k , b) has the form d: ∇F , where ∇ ∈ {✸, ✸ -, E}. If k had a witness d ′ in N 0 , then N 0 would contain a node labelled by d ′ : F and, if ∇ = E, a node labelled by d: ✸d ′ (or d ′ : ✸d). As a consequence, N i would contain nodes labelled by θ

i (d ′ ): θ i (F ) and, if ∇ = E, θ i (d): ✸θ i (d ′ ) (or θ i (d ′ ): ✸θ i (d)). Since label(q i ) = θ i (G(c 0 , c 1 , . . . , c k , b)) = θ i (d): ∇θ i (F ), then θ i (d ′
) would be a witness for q i in N i , contradicting the initial hypothesis that q i has no witness in N i .

Since k has no witness in N 0 , k is blocked in B, thus B 0 contains a triple of the form (k, k ′ , σ). Consequently, σ(label(k ′ )) = label(k) and θ i (label(k)) = label(q i ).

Then we set:

• β q i = k ′ ; • µ q i = (θ i • σ) | label(k ′ ) (see Figure 11). k ′ k q i σ θ i µ q i Figure 11:
The construction of the substitution µ q i mapping k ′ = β q i to q i . Since the invariants 1a, 1b and 1c hold for N i-1 , it follows that:

1a) k ′ = β q i is not blocked in B.
1b) Since both θ i and σ are injective, µ q i is injective too. Moreover, µ q i modifies only nominals occurring in label(β q i ) by construction. 1c) label(q i ) is a blockable formula, and (µ q i )(label(β

q i )) = (µ q i )(label(k ′ )) = (θ i • σ)(label(k ′ )) = θ i (σ(label(k ′ ))) = θ i (label(k)) = label(q i ).
We then define:

B i = (B i-1 \ {(n p , m, π)}) ∪ {(q i , β q i , µ q i ) | q i ∈ S}
In other words, B i is obtained from B i-1 by eliminating the triple (n p , m, π) (since n p has a witness in N i ), and adding the triple (q i , β q i , µ q i ) for any new node q i without witness in N i . The three invariants 1a, 1b and 1c still hold for N i , by the previous observations, and invariant 2 holds by construction.

Finally, if B is a complete and open branch, the possibly infinite set of nodes N ∞ B is defined by:

N ∞ B = i∈IN N i
Clearly, i∈IN B i = Ø, because of the fairness of the choice of the "blocked" nodes leading the construction of the sets N i , for which a witness is added at the i-th stage. Therefore, by invariant 2, every blockable node has a witness in N ∞ B .

• In order to show that item 13 holds for N 0 , let us assume that (n) a: AF ∈ N 0 and d occurs in N 0 . By Lemma 10, d occurs in some non-phantom node in B. As a consequence, by item 2 of Lemma 3, there exists a nonphantom node (m) d: F in B, and m ∈ N 0 .

Let us now assume that N i-1 is pseudo-saturated. The pseudo-saturation property in N i still holds for all nodes already belonging to N i-1 . We show that the newly added nodes do not spoil pseudo-saturation.

1. If some node n i in N i is labelled by a formula of the form a: ¬a, then for some node n ∈ N 0 , a: ¬a = θ i (label(n)). Therefore label(n) = θ - i (a: ¬a) = c: ¬c, for some nominal c, contradicting the fact that N 0 is pseudo-saturated.

2. Let us assume that, for some p ∈ PROP, (n j ) a: p ∈ N i and (m k ) a: ¬p ∈ N i . By the induction hypothesis, n j and m k cannot be both in N i-1 .

So let us consider three cases:

n i ) = a: F ∧ G = θ i (label(n)) = θ i (c): θ i (F ′ ) ∧ θ i (G ′ ). Since N 0 is pseudo-saturated, it con- tains nodes (n 1 ) c: F ′ and (n 2 ) c: G ′ . Therefore N i contains nodes labelled by θ i (label(n 1 )) = θ i (c: F ′ ) = a: F and θ i (label(n 2 )) = θ i (c: G ′ ) = a: G.
5. Let a node n i ∈ N i be labelled by a: F ∨ G, and let c: F ′ ∨ G ′ be the label of the node n ∈ N 0 . Then label(n

i ) = θ i (label(n)) = θ i (c): θ i (F ′ ) ∨ θ i (G ′ ).
Since N 0 is pseudo-saturated, N 0 contains either a node (n 1 ) c: F ′ or a node (n 2 ) c: G ′ . As a consequence, either θ i (c: F ′ ) = a: F or θ i (c: G ′ ) = a: G occurs as a node label in N i .

6. Let a node n i ∈ N i be labelled by a: d: F , and let c: e: F ′ be the label of the node n ∈ N 0 . Then label(n i ) = θ i (label(n)) = θ i (c: e: F ′ ). Since N 0 is pseudo saturated, it contains a node labelled by e: F ′ , therefore N i contains a node labelled by θ i (e: F ′ ) = d: F .

7. Let us assume that (n i ) a: ↓x.F ∈ N i . Then θ - i (a: ↓x.F ) = c: ↓x.G is the label of the node n ∈ N 0 , where θ i (c) = a and θ i (G) = F . Since N 0 is pseudo-saturated, it also contains a node labelled by c: G[c/x]. Therefore N i contains a node labelled by θ does not contain any non-top nominal, hence θ i (F ) = F for any i (for the sake of generality, θ 0 is taken to be the identity).

i (c: G[c/x]) = θ i (c): θ i (G)[θ i (c)/x] = a: F [a/x]. 8. Let (n) a: ✸F ∈ N i ,
We distinguish two cases:

(a) (n) a: ✷F ∈ N i-1 . By item 1 of Lemma 11, then, a = b i is the new nominal introduced at stage i. Therefore, N 0 contains nodes labelled by θ

- i (b i : ✷F ) = θ - i (b i ): ✷F and θ - i (b i : ✸d) = θ - i (b i ): ✸θ - i (d). Since N 0 is pseudo-saturated, θ - i (d): F ∈ N 0 , so that θ i (θ - i (d)): F = d: F ∈ N i . (b) (n) a: ✷F ∈ N i-1 . If also (m) a: ✸d ∈ N i-1 , then d: F ∈ N i-1 ⊆ N i by the induction hypothesis. Otherwise, θ - i (a): ✸θ - i (d) ∈ N 0 . Let a ′ = θ - i (a) and d ′ = θ - i (d)
. By item 2 of Lemma 11, a and a ′ are compatible in N i , therefore a ′ : ✷F ∈ N i . Moreover, since a ′ occurs in N 0 , by item 1 of Lemma 11, a ′ : ✷F ∈ N 0 . Since also a ′ : ✸d ′ ∈ N 0 and N 0 is pseudo-saturated, d ′ : F ∈ N 0 , so that also θ i (d ′ ): F = d: F ∈ N i . 10-11. Items 10 and 11 are proved similarly to cases 8 and 9, respectively. 12. Let (n) a: EF ∈ N i . If n has no witness in N i (there is no node labelled by d: F in N i ), then B i contains a triple of the form (n, n ′ , π), by the invariant 2 of the construction of S B defined in Section 5.2.1.

13. Let us assume that (n) a: AF ∈ N i and let d be any nominal occurring in N i . By Lemma 4, F does not contain any non-top nominal, hence θ i -(F ) = F for any i. As a consequence there is a node m ∈ N 0 whose label is θ - j (a): AF for some j (if j = 0, θ j is the identity). If d occurs in N i-1 , since m ∈ N i-1 ⊇ N 0 , some node labelled by d: F belongs to N i-1 ⊆ N i , by the induction hypothesis. Otherwise, d is the new nominal b i introduced at stage i and, since N 0 is pseudo-saturated, θ - i (d): F ∈ N 0 , so that θ i (θ - i (d)): F = d: F ∈ N i .

Now we have all that is needed to build a model of any complete and open branch B, i.e. an interpretation M such that for any node label a : F ∈ B, F holds in the state denoted by a. Theorem 2 (Completeness). If a formula F is unsatisfiable, then any complete tableau for F is closed.

Proof. We show, as usual, that if a tableau for F has a complete and open branch, then F is satisfiable. So, let B be a complete and open branch in a tableau for the formula F , and let a: F 0 be its top formula. Since the equality rule may be used during the construction of B, F 0 = F [c 1 /a 1 , . . . , c n /a n ], where a 1 , . . . , a n do not occur in B. By Lemma 13, there exists a model of F 0 . Such a model can easily be extended to a model of F , establishing that I(a i ) = I(c i ) for i = 1, . . . , n.

The model built in the proof is potentially infinite, even though the considered hybrid fragment enjoys the finite model property (since the same holds for guarded logic [START_REF] Grädel | On the restraining power of guards[END_REF]). As already remarked at the beginning of this section, it is not possible to construct a finite model just reusing existing nominals as witnesses, instead of creating a fresh one for each blocked node. Moreover, in general, if a given stage of the construction uses the blocking mapping π i = {a 0 /c 0 , . . . , a k /c k }, it might be the case that the branch constructed so far contains some inequality a j : ¬c j , so that a j and c j cannot be interpreted by the same state in the model. Whether different nominals can be semantically identified at some stage, so that the existing construction can sooner or later terminate, is still an open question.

Concluding Remarks

In this work a tableau calculus for full hybrid logic (FHL, which includes the binder and the global and converse modalities) is defined, which is provably terminating (independently of the rule application strategy) and complete for formulae belonging to the fragment FHL \↓✷. A preprocessing step transforming formulae into equisatisfiable ones turns the calculus into a satisfiability decision procedure for FHL \ ✷↓✷.

The main features of the calculus can be summarized as follows. A tableau branch is a sequence of nodes, each of which is labelled by a satisfaction statement. Nominal equalities are dealt with by means of substitution, and, in the context of the considered fragment, this ensures a key property of the calculus, used to prove both termination and completeness: any universal formula occurring in a tableau branch is a subformula of the top formula, therefore a branch cannot contain an unbounded number of universal formulae. As an effect of nominal substitution, different occurrences of the same formula may occur as labels of different nodes in a branch, because, when two formulae become equal by an application of the equality rule, the corresponding nodes do not collapse. Alhough this fact is responsible for a significant amount of technicalities in the proofs, it is essential for the definition of a binary relation ≺ B on nodes which organizes them into a family of trees (i.e. each node has at most one "parent").

Each tree of the family has a bounded depth, and this is guaranteed by a blocking mechanism which forbids the application of the blockable rules (✸, ✸ - and E) to a node n whenever there exists a previous node whose label is equal to the label of n, modulo non-top nominal renaming (accompanied by suitable restrictions). Renaming is essential, because, in the presence of the binder, nontop nominals may occur in the body of any node label. The blocking mechanism is anywhere blocking, paired with indirect blocking, relying on the relation ≺ B .

Moreover, each tree has a bounded width, and this is essentially due to the following peculiarities of the relation ≺ B : (i) when applying a two-premiss rule (either ✷ or ✷ -), it is the minor premiss, labelled by a relational formula, which is taken to be the "main responsible" of the expansion, i.e. the node producing the conclusion; and (ii) the main responsible of an application of the A rule adding a node labelled by b: F is not its premiss, but the first node containing the focused nominal b, provided that such a node is not indirectly blocked.

We remark that indirect blocking is necessary to ensure termination, even in the absence of the converse modalities, since the binder allows a state to convey information to other states from which it is accessible (its "past").

A blocking mechanism similar to ours is used in the tableau calculus testing satisfiability of formulae in the constant-free clique guarded fragment, proposed in [START_REF] Hirsch | A tableau algorithm for the clique guarded fragment[END_REF]. A restriction of the algorithm to the guarded fragment has been defined and implemented [START_REF] Hladik | Implementation and evaluation of a tableau algorithm for the guarded fragment[END_REF]. In these calculi, a tableau branch (called completion tree) is a tree where each node is labelled by a set of formulae. Termination in the considered tableau systems is also due to anywhere blocking with indirect blocking, which relies on the ancestor relation in the tree. A node is directly blocked by a previously created node if, essentially, their labels are the same modulo constant renaming. Our comparison modulo renaming method was originally inspired by [START_REF] Hirsch | A tableau algorithm for the clique guarded fragment[END_REF][START_REF] Hladik | Implementation and evaluation of a tableau algorithm for the guarded fragment[END_REF], although it is not exactly the same (and is embedded in a different context). As already observed in Section 5.1, the cardinality of node labels in a completion tree has an exponential upper bound w.r.t. the size of the initial formula. As a consequence, considering all the formulae in the node label for blocking instead of a single formula (paired, in the setting of our calculus for hybrid logic, with a polynomial amount of information on nominal compatibility) leads to an exponentially higher number of "blockable node types" and, consequently, to an exponentially higher bound on the number of nodes in a tableau branch.

In order to compare the calculus defined in the present paper with other terminating tableau systems for binder-free hybrid logic, it may be useful to see what it looks like in the absence of the binder. In the binder-free sub-calculus, for any node label a: F , F contains only top nominals. Therefore, a blockable node (n) a: F is directly blocked by a previous non-blocked node m in a branch B if and only if label(m) = b: F and a and b label, in B, the same set of propositions in PROP and the same formulae of the form ∇G, for ∇ ∈ {✷, ✷ -}. As remarked in Section 4, the blocking condition for E in our calculus can actually ignore the compatibility restriction on the outermost nominal. In the absence of the binder, this amounts to saying that (n) a: EF is blocked whenever the branch contains a previous non-blocked node labelled by b: EF for some nominal b.

between practice and theory is the question of turning the construction given in the completeness proof (which builds a potentially infinite model although the logic itself enjoys the finite model property) into one ensuring the output of a finite model. On the theoretical side, investigating the possibility of enriching the language with transitive relations and number restrictions might open the way to exporting our results to description logics.

2 .

 2 M w , σ |= a if N (a) = w, for a ∈ NOM.

3 .

 3 M w , σ |= x if σ(x) = w, for x ∈ VAR.

4 .

 4 M w , σ |= ¬F if M w , σ |= F . 5. M w , σ |= F ∧ G if M w , σ |= F and M w , σ |= G. 6. M w , σ |= F ∨ G if either M w , σ |= F or M w , σ |= G.

7 .

 7 M w , σ |= a: F if M N (a) , σ |= F , for a ∈ NOM. 8. M w , σ |= x: F if M σ(x) , σ |= F , for x ∈ VAR. 9. M w , σ |= ↓x.F if M w , σ w x |= F . 10. M w , σ |= ✷F if for every w

Definition 1 (

 1 Nominal compatibility). If B is a tableau branch and a is a nominal occurring in B, then Φ B (a) = {p | p ∈ PROP and a: p ∈ B} ∪ {✷F | a: ✷F ∈ B} ∪{✷ -F | a: ✷ -F ∈ B} If a and b are nominals occurring in a tableau branch B, then a and b are compatible in B if Φ B (a) = Φ B (b), i.e. if they label the same propositions in PROP and the same formulae of the form ∇F , for ∇ ∈ {✷, ✷ -}. Definition 2 (Mappings). A mapping π for a branch B is an injective function from non-top nominals to non-top nominals such that for all a, a and π(a) are compatible in B.

Definition 3 .

 3 Let B be a tableau branch. The relation n ≺ B m between nodes of B is inductively defined as follows: Base case. If R is a blockable rule and n ❀ R (m, k), then n ≺ B m and n ≺ B k;

F

  = a: (✸p ∧ ✷↓x.✸ -(p ∧ ¬x ∧ ↓y.a: ✸y)) represented in Figure 1. Node numbering reflects the order in which nodes are added to the branch. The right column reports the ❀ R relation justifying the addition of the corresponding node to the branch. W.r.t. the relation ≺ B , 0, 1 and 3 are root nodes with no children; 2 is also a root node, with children 4, 5, 6 and 7; nodes 8-17 are all children of 7 (see Figure 2).

( 0 )Figure 1 :

 01 Figure 1: A tableau branch for a: (✸p ∧ ✷↓x.✸ -(p ∧ ¬x ∧ ↓y.a: ✸y))

Figure 2 :

 2 Figure 2: One of the trees induced by the ≺ B relation on the nodes of the branch in Figure 1

B ( 0

 0 ) a: ↓x.✸(p ∧ ↓y.x: (p ∧ y)) (1) a: ✸(p ∧ ↓y.a: (p ∧ y)) 0 ❀ ↓ 1 (2) a: ✸b 1 ❀ ✸ 2 (3) b: (p ∧ ↓y.a: (p ∧ y)) 1 ❀ ✸ 3 (4) b: p 3 ❀ ∧ 4 (5) b: ↓y.a: (p ∧ y) 3 ❀ ∧ 5 (6) b: a: (p ∧ b) 5 ❀ ↓ 6 (7) a: (p ∧ b) b: ↓x.✸(p ∧ ↓y.x: (p ∧ y)) (1) b: ✸(p ∧ ↓y.b:

Figure 4 :

 4 Figure 4: Example 3

  represents a closed one-branch tableau for F = (✸↓x.✸(x: p)) ∧ (✸↓y.✸(y: ¬p)) ∧ (✸↓z.(✸(z: p) ∧ ✸(z: ¬p)))

Figure 5 :

 5 Figure 5: Example 4

Figure 6 : 5

 65 Figure 6: The relation ≺ B on the nodes of the branch in Figure 5 The branch is closed because of nodes 23 and 26. In B 20 , node 19 is not blocked by 6, since a: ✸a: p cannot be mapped to c: ✸c: p because c and a are not compatible in B 20 (Φ 20 (c) = Ø = {p} = Φ 20 (a)); therefore, node 19 can be expanded. In the same branch segment, on the contrary, node 20 is blocked by 12, because Φ 20 (c) = Ø = Φ 20 (b).When the construction proceeds, expanding the non-blocked node 19, and nodes 21-23 are added to the branch, c and b are no more compatible (Φ 23 (c) = {p} while Φ 23 (b) is still empty), so node 20 is unblocked and it is expanded, producing 24-26 and the branch closes.After the addition of node 23, a and c become compatible, so that in B 23 node 19 is blocked by 6, and 21-23 are phantom nodes. Since 20 is not a descendant of 19 w.r.t. ≺ B , it is not a phantom, thus it can be expanded.

Figure 7 : 5 .

 75 Figure 7: Example 5. The relation ≺ B in this branch can be described as follows: the root nodes are 1-4, 4 ≺ B {5, . . . , 8}, 8 ≺ B {9, . . . , 17}, 17 ≺ B {18, . . . , 26} and 26 ≺ B {27, . . . , 33}. 3 In B 17 , node 17 is not blocked by 8 because Φ 17 (b) = {q, p} = Ø = Φ 17 (b 1 ). And it is not blocked by 8 in B n for any n ≥ 23 either, where Φ n (b) = {q, p} = {p} = Φ n (b 1 ). Moreover, in B 26 , node 26 is blocked neither by 8 nor by 17, because Φ 26 (b) = {q, p}, Φ 26 (b 1 ) = {p}, and Φ 26 (b 2 ) = Ø. But in B 33 , node 26 is blocked by 17, because Φ 33 (b 1 ) = {p} = Φ 33 (b 2). Therefore its children w.r.t. ≺ B33 , i.e. 27-33, are all phantom nodes, and, in particular, node 33 cannot participate, with node 3, to an expansion via the ✷ rule.Without restriction R3, the construction of the branch would go on forever, since the following nodes could be added:

(34) b 3 :

 3 ↓x.✸↓y.(x: p ∧ a: ✸y) (3, 33) ❀ ✷ 34 (35) b 3 : ✸↓y.(b 3 : p ∧ a: ✸y) 34 ❀ ↓ 35 In B 35 , node 35 would not be blocked, because Φ 35 (b 3 ) = Ø, while Φ 35 (b 1 ) = Φ 35 (b 2 ) = {p}. So a sequence of new nodes could be added, with labels obtained from the labels of 27-34, by renaming b 2 with b 3 and b 3 with a new nominal b 4 . A neverending story . . .

Figure 8 :

 8 Figure 8: Construction of a tableau branch for a: (A↓x.a: x ∧ Ap ∧ A✸q).

  11 is not blocked by 8 in B 11 because b 1 and b 2 are not compatible in B 11 : Φ 11 (b 1 ) = {p, q} = {q} = Φ 11 (b 2 ). So, 11 can be expanded, generating 12 and 13, and 11 ≺ B {12, 13}.In B 13 , the first non-phantom node where b 3 occurs is 12, that is therefore the minor premiss of the A inference producing 14. Consequently, 11 ≺ B 14. In B 14 , node 14 is blocked by11 because Φ 14 (b 2 ) = Φ 14 (b 3 ) = {q}.Since B 14 has no phantoms, the A rule can expand node 1, focusing on b 3 , and producing node 15 with minor premiss 12. Therefore 11 ≺ B 15. Since 11 is not blocked, 15 can be expanded, and its siblings 16 and then 17 are added to the branch: 11 ≺ B {16, 17}. Now, the application of the (=) rule to node 17 replaces b 3 for a in the node labels, so that the branch becomes B ′ 17 . The relation ≺ B ′ is the same as ≺ B : 0-4 are root nodes, 4 ≺ B ′ {5, 6, 7, 8}, 8 ≺ B ′ {9, 10, 11} and 11 ≺ B ′ {12, 13, 14, 15, 16, 17}. However the status of nodes w.r.t. blocks changes: since b 3 is a top nominal in B ′ , 11 does not block 14 any longer. The next inference adds node 18 by an application of the A rule with 9 as the minor premiss (so 8 ≺ B ′ 18). Now b 1 and b 2 are compatible in B ′ 18 because Φ 18 (b 1 ) = Φ 18 (b 2 ) = {p, q}. As a consequence, 8 blocks 11 and its descendants, 12-17, are phantoms in B ′ 18 . Since, in B ′

a 2 :@ 12 Figure 9 :

 2129 Figure 9: A complete tableau for A↓x.Ex: p.

Figure 10 :

 10 Figure 10: Outside the fragment

2 . 1 .

 21 if B is a complete and open branch containing a non-phantom node (n) a: AF and if b occurs in some non-phantom node in B, then there exists a nonphantom node (m) b: F in B. Proof. Let us assume that n ≺ B m and n ≺ B m ′ . If either n is directly blocked or is a phantom in B, then both m and m ′ are phantom in B. Otherwise none of them is a phantom. 2. Let B be a complete and open branch containing a non-pantom node (n) a: AF , and let b occur in some non-phantom node k in B. Then an application of the A rule on n focusing on b in B would violate neither restriction R3 nor restriction R6. Therefore, the only reason why B can be complete is that an application of the A rule on n focusing on b would violate restriction R1, i.e. B already contains a non phantom node labelled by b: F .

8 .

 8 Finally, let us consider the case where the equality rule is applied to B ′ , replacing the nominal c with b, and let a 0 : F 0 be the top formula of B ′ . The top formula of B is therefore a 0 [b/c]: F 0 [b/c]. Let us consider the label a: F of any node n in B ′ , which is not a relational formula. The label of n in B is a[b/c]: F [b/c]. Any subformula of F [b/c] is obtained from a subformula F ′ of F by replacing c with b, i.e. it has the form F ′ [b/c]. By the inductive hypothesis

  . a n ), then the label of n 0 in B has the form b 0 : F 0 (b 1 , . . . b n ), where b i is either a i or a nominal replacing it. Lemma 4 establishes that any universal formula H occurring in B is a subformula of b 0 : F 0 (b 1 , . . . b n ), and its nominals are top nominals in B, i.e. they occur in b 0 : F 0 (b 1 , . . . b n ). As a consequence, the number of universal formulae occurring in B is bounded by the number of subformulae of F 0 (a 1 , . . . a n ).

3 .

 3 The set ∆ M is the set containing all the M -instances of every element of ∆. For instance, if ∆ = {x: ✸y, z: p} and M = {a, b}, then: ∆ M = {a: ✸a, a: ✸b, b: ✸b, b: ✸a, a: p, b: p} Clo(∆ M ) = (Clo(∆)) M = ∆ M ∪ {✸a, ✸b, a, b, p} Lemma 5. Let n be a node in a branch B of a tableau for a formula F , and let N = |F |. Then the cardinality of Σ(n) = {m | n ✄ * m} is bounded by an exponential function E w (N ).

  with label Bi-1 (k) = label Bi (k) = a: b: F ′ and label Bi (m) = b: F ′ . By the induction hypothesis, a: b: F ′ = σ i-1 (c: d: F ) = σ i (c: d: F ) for some c: d: F ∈ F n . Since d: F ∈ S n , d ∈ M n and F ∈ S n . Therefore also d: F ∈ F n . So, since label Bi (m) = b: F′ = σ i (d: F ), d: F is a matrix of m in B i . (↓) Let n ✄ * k ❀ ↓ m, with label Bi (k) = a: ↓x.F ′ and label Bi (m) = a: F ′ [a/x].By the induction hypothesis, a: ↓x.F ′ = σ i-1 (c: ↓x.F ) = σ i (c: ↓x.F ) for some c: ↓x.F ∈ F n . Since ↓x.F ∈ S n , any instance of F replacing x with a nominal in M n is in S n . In particular F [c/x] ∈ S n . Moreover c ∈ M n and a

  ✸b and label Bi (m) = b: G. By Lemma 4, ✷G ∈ S n . Therefore also G ∈ S n . By the induction hypothesis, a: ✸b = σ i (c: ✸d) for some c: ✸d ∈ F n , i.e. b = σ i (d) for d ∈ M n . Therefore d: G ∈ F n and, since b: G = σ i (d: G), d: G is a matrix of m in B i . (✷ -) The reasoning is the same as in the previous case, with the obvious replacement of node labels. (A) Let n ✄ * k and let (m) b: G be added to B i by an application of the A rule whose minor premiss is k, so that k ✄ m. By Lemma 4, G ∈ S n . By the induction hypothesis, since b occurs in label Bi-1 (k), b = σ i (d) for some d ∈ M n . Therefore d: G ∈ F n and, since b: G = σ i (d: G), d: G is a matrix of m in B i .Next we observe that:(β)for any pair of nodes m, k and any branch B, if m ✄ k then m is a phantom node in B if and only if k is a phantom in B. Consequently, also if m ✄ * k then m is a phantom in B if and only if k is a phantom in B. And, for any branch B, either all elements of Σ(n) are phantom nodes in B or none of them is a phantom in B.

1 .

 1 label(n) = a: ✸F and N i contains nodes labelled, respectively, by a: ✸b and b: F ; 2. label(n) = a: ✸ -F and N i contains nodes labelled, respectively, by b: ✸a and b: F ; 3. label(n) = a: EF and N i contains a node labelled by b: F .

  (a) m ∈ N 0 and m is not blocked in B (neither directly nor indirectly); (b) π is an injective mapping from non-top nominals to non-top nominals modifying only nominals occurring in the label of m;

  (a) (n j ) a: p ∈ N i-1 and (m k ) a: ¬p ∈ N i-1 , thus k = i and label(m i ) = θ i (label(m)) = θ i (c: ¬p) for some (m) c: ¬p ∈ N 0 and nominal c such that θ i (c) = a. By item 2 of Lemma 11, a and c are compatible in N i , therefore c: p ∈ N i . Since c occurs in N 0 , by item 1 of Lemma 11, c: p ∈ N 0 , contradicting the fact that N 0 is pseudo-saturated.(b) (n j ) a: p ∈ N i-1 and (m k ) a: ¬p ∈ N i-1 , thus j = i.By item 1 of Lemma 11, a = b i is the fresh nominal introduced at stage i, which does not occur in N i-1 . So, it cannot be the case that m k ∈ N i-1 , i.e. this case is actually impossible.(c) Neither n j nor m k are in N i-1 , and j = k = i. Since label(n i ) = a: p, by item 1 of Lemma 11, a = b i is the fresh nominal introduced at stage i. Therefore, for some nodes n, m ∈ N 0 , label(n i ) = θ i (label(n)) and label(m i ) = θ i (label(m)). Therefore, label(n) = θ - i (a: p) = θ - i (a): p and label(m) = θ - i (a: ¬p) = θ - i (a): ¬p, contradicting the fact that N 0 is pseudo-saturated. 3. Let n i be a new node added at stage i and labelled by a formula of the form a: d, where where a and d are nominals. Therefore a: d = θ i (c): θ i (d) for some c: d ∈ N 0 . Since N 0 is pseudo-saturated, c = d, therefore also a = d. 4. Let (n i ) a: F ∧ G be a node newly added to N i , and let c: F ′ ∧ G ′ be the label of the node n ∈ N 0 . By construction, label(

Lemma 13 .

 13 If B is a complete and open branch, then the possibly infinite set N ∞ B has a model. Proof. Let M = W, R, N, I be defined as follows: W is the set of all the nominals occurring in N ∞ B and, for a, b ∈ W : aRb if and only if a: ✸b is the label of some node in N ∞ B , N (a) = a and, for any p ∈ PROP, p ∈ I(a) if and only if a: p is the label of some node in N ∞ B . Such an interpretation is well defined because of Lemma 12. Since i∈IN B i = Ø, every blockable node in N ∞ B has a witness. Exploiting this fact and Lemma 12, an easy induction on F shows that for any label a: F of a node in N ∞ B , M a |= F .

Table 1 :

 1

Expansion rules labels, therefore it does not change the relation ❀ R between nodes. In general, the relation ❀ R is static: if a branch B ′ is obtained by application of an expansion rule to B, then, for every pair of nodes n, m ∈ B, n ❀ R m in B ′ if and only if n ❀ R m in B. This justifies the fact that the current branch is left implicit in the notation.

  ′ on the right is obtained from the branch B, shown on the left, by application of the equality rule to node 9. The two nodes labelled by the same formula, 4 and 8, are siblings w.r.t. the relation ≺ B .

	Figure 3: Example 2
	Example 2. Figure 3 represents a one-branch tableau for the formula ↓x.✸(p ∧
	↓y.x: (p ∧ y)). The example shows that, notwithstanding Restriction R1, a
	tableau branch may contain different nodes with the same label, because of the
	presence of the equality rule.
	The branch B

  [START_REF] Marx | Narcissists, stepmothers and spies[END_REF] a 3 : ↓x.Ex: p 0 ❀ A 13 (14) a 3 : Ea 3 : p 13 ❀ ↓ 14 (15) a 4 : a 3 : p 14 ❀ E 15 (16) a 3 : p 15 ❀ @ 16 (17) a 4 : ↓x.Ex: p 0 ❀ A 17 (18) a 4 : Ea 4 : p 17 ❀ ↓ 18 (19) a 4 : a 4 : p 18 ❀ E 19 (20) a 4 : p 19 ❀ @ 20

	.
	.
	.

  where F is not a nominal. If n has no witness in N i (there is no nominal b and nodes (m) a: ✸b ∈ N i and (k) b: F ∈ N i ), then B i contains a triple of the form (n, n ′ , π), by the invariant 2 of the construction of S B defined in Section 5.2.1.

9. Let us assume that (n) a: ✷F ∈ N i and (m) a: ✸d ∈ N i . By Lemma 4, F

The cited works prove a stronger result: even in the absence of nominals and @, HL(↓) is undecidable.

After applying the standard translation, universally guarded formulae must be rewritten into equisatisfiable guarded ones. Furthermore, constants deriving from nominals must be eliminated, since the cited decision procedures apply to constant-free formulae.

The notation n ≺ B {m 1 , . . . , m k } abbreviates n ≺ B m 1 and . . . n ≺ B m k . 13

An application of the A rule with no minor premiss generates a top node. If such expansions were allowed, the forest of nodes induced by ≺ B would possibly be made of an unbounded number of trees. However, this is actually not going to be a problem, as it will be taken care of by restriction R6, stated later on.

Let us recall that a : ✸ -b is blockable, since it is not a relational formula.

The nominal generating relation in the considered paper is somewhat more complicated than in[START_REF] Bolander | Termination for hybrid tableaus[END_REF][START_REF] Cerrito | Nominal substitution at work with the global and converse modalities[END_REF], because of an implicit treatment of nominal equalities.

Acknowledgments. The authors wish to thank the anonymous reviewers of this paper for their comments and suggestions, and Rajeev Goré for helpful remarks on the content of this work.

Model construction

The proof that if B is a complete and open tableau branch for F then F is satisfiable, exploits the construction of a model of N ∞ B . In order to build such a model, some properties of the sets N i and their associated relations are first proved.

In what follows, we shall sometimes write a: F ∈ N i to mean that N i (i.e. an element of the sequence S B ) contains some node labelled by a: F . We recall moreover that any mapping θ i (guiding the construction of N i as defined above) is injective, hence its inverse θ - i is defined.

If it were d ′ = c j for some j = 0, . . . , k, then the label of n i would be a j : H; consequently, since no node labelled by a formula already occurring in N i-1 is added to N i , a j : H wouldn't be the label of any node in N i-1 ; but this is impossible, because, by the induction hypothesis (item 2) a j and c j are compatible in N i-1 . Therefore, we are left with the only possibility that d = b i .

2. Let θ i be either

. By the inductive hypothesis (item 3), a j and c j are compatible in N i-1 , and, by item 1 (which has already been proved for N i ), they stay compatible in N i . Thus, let us assume that b = c j , so that θ i (b) = b i where b i is the fresh nominal added at stage i, and let H be any propositional letter in PROP or formula of the form ∇G for ∇ ∈ {✷, ✷ -}. We have: Proof. The proof is by induction on i. N 0 is pseudo-saturated with respect to B 0 because B is a complete and open branch. In particular:

• items 1 and 2 hold for N 0 because B is open.

• Item 3 holds because B is complete, hence during its construction each non-phantom node labelled by a non-trivial equality has been expanded by the equality rule, and the only phantom nodes of B possibly occurring in N 0 have the form a: F where F ∈ Cmp(B).

• Items 4-7 hold because if n is not a phantom and non-phantom nodes labelled by its expansion(s) were not present in B, n would have to be expanded before completing the branch, generatings siblings having the same non-phantom status as n.

• Items 8, 10 and 12 hold for N 0 because, if a blockable node n is in N 0 , then it is not a phantom in B, and if B 0 contains no triple of the form (n, n ′ , π), then n is not blocked in B. Since B is complete, it contains a non-phantom node (m) d: F , for some nominal d, and, in cases 8 and 10, a non-phantom node k labelled by a: ✸d or d: ✸a, respectively. N 0 contains m (and k) because it contains all non-phantom nodes.

• Item 9 holds because, if (m) a: ✸d ∈ N 0 , then m is not a phantom in B.

If also (n) a: ✷G ∈ N 0 ⊆ B and N 0 did not contain any node (k) d: G, then any node labelled by d: G in B (if present) would be a phantom. Therefore, in order for B to be complete, the ✷ rule should be applied to n and m, generating a node (k) d: G ∈ B. Since m and k would be siblings w.r.t. ≺ B , k would not be a phantom in B, therefore k ∈ N 0 . A similar argument shows that item 11 holds for N 0 .

The blocking mechanism used in the calculus defined in the present paper differs from [START_REF] Bolander | Termination for hybrid tableaus[END_REF][START_REF] Cerrito | Nominal substitution at work with the global and converse modalities[END_REF], where calculi for hybrid logic with the global and converse modalities (and no binders) are defined. Such calculi adopt ancestor blocking, where nominals (and not nodes) are blocked, and indirect blocking relies on a partial order on nominals (instead of nodes), depending on the "nominal generating" relation (holding between a and b when the expansion of a: F produces the new nominal b by application of a rule that generates fresh nominals, i.e. one of our blockable rules). In the considered works, moreover, in order for a formula a: F to be directly blocked by an ancestor b: F , a and b are required to label exactly the same set of formulae (equality blocking) -except for the E rule in [START_REF] Cerrito | Nominal substitution at work with the global and converse modalities[END_REF], where the outermost nominal is ignored. Differently from [START_REF] Cerrito | Nominal substitution at work with the global and converse modalities[END_REF], finally, the calculus defined in this work, though still treating nominal equalities by means of substitution, does not require nominal deletion to ensure termination. This is due, again, to the fact that a branch is not a set of formulae, but a sequence of nodes.

In [START_REF] Kaminski | Terminating tableau systems for hybrid logic with difference and converse[END_REF] a terminating system for binder-free hybrid logic with the global, converse and difference modalities, as well as reflexive and transitive relations, is defined. In the sub-calculus without the converse modalities, a formula a: ✸F is blocked if the branch already contains a formula b: F , such that b: G is in the branch for every a: ✷G in the branch; a formula a: EF is blocked if the branch already contains b: F for some nominal b. The blocking condition for E is therefore quite similar to that used in the present paper. It is actually the same as restriction R5, but for the fact that our restriction requires the witness to be non-phantom (however, indirect blocking could be dispensed with, when neither the binder nor the converse modalities are present). Also the blocking rule for ✸ (pattern based blocking) is similar to our restrictions on the applicability of the corresponding expansion rule. However, the sub-calculus does not terminate under every rule application strategy, but only if applications of the ✷ rule are prioritized. Pattern based blocking is not extended to the converse modalities. In the full calculus, in fact, ancestor blocking with indirect blocking is adopted: a formula of the form a: ∇F for ∇ ∈ {✸, ✸ -} is directly blocked by b: ∇F if b is an ancestor of a (w.r.t. the "nominal generating" relation), 6 and the outermost nominals a and b are modally equivalent, i.e. they label the same set of formulae taken from a given finite set.

Since the presence of the converse modalities (or the binder) necessarily requires indirect blocking to ensure termination, a partial order on the elements of a tableau branch (either nodes or formulae) has to be considered. The main novelty of the present work w.r.t. [START_REF] Bolander | Termination for hybrid tableaus[END_REF][START_REF] Cerrito | Nominal substitution at work with the global and converse modalities[END_REF][START_REF] Kaminski | Terminating tableau systems for hybrid logic with difference and converse[END_REF] is that indirect blocking relies on a partial order that is not the usual ordering on nominals induced by the nominal generating rules. Paired with a suitable notion of nominal compatibility which is sufficient for completeness, this partial order arranges tableau nodes in a bounded-sized forest of bounded-sized trees, independently of the rule application strategy.

Directions for future work include both practical and theoretical issues. An implementation of the tableau calculus defined in this paper (which requires a careful analysis of some non-trivial mechanisms) would allow for an experimental comparison of the direct method w.r.t. translation based systems. Midway