
## 4 Termination Of The Tableau Cal Ulus

```
The 
    al
      ulus presented above 
                       an lead to non-terminating 
                                             omputations due to
                                                            

```

the interplay between the rules whi h generate new labels (the dynami rules

(F2 ⇔), (F) and (Fx)) and the stati rule (T ⇔) whi
h generates formula ¬xA to whi
h (Fx) may again be applied. Our 
al
ulus 
an be made

```
terminating by dening a systemati
                                    pro
                                        edure for applying the rules and by
                                                                          

```

introdu ing appropriate blo king onditions. The systemati pro edure simply

```
pres
    ribes to apply stati
                    rules as far as possible before applying dynami
                                                          rules.
                                                              

```

To prevent the generation of an innite tableau set, we put some restri tions on the rule's appli ations. The restri tions on all rules ex ept (F2 ⇔) and (F2x)

```
are easy and prevent redundant appli
                                    ations of the rules. We 
                                                           all the restri
                                                                        tions
                                                                             

```

on (F2 ⇔) and (F2x) blo
king 
onditions in analogy with standard 
onditions

```
for getting termination in modal and des
                                              ription logi
                                                           s tableaux; they prevent the generation of innitely many labels by performing a kind of loop-
                                                                  he
                                                                     king.
                                                                          

```

To this aim, we rst dene a total ordering ⊏ on the labels of a tableau set su h that x ⊏ y for all labels x that are already in the tableau when y is introdu ed. If x ⊏ y, we will say that x is older than y.

We dene Box+
Γ,x,y as the set of positive boxed formulas indexed by x labelled by y whi
h are in Γ : Box+
Γ,x,y = {x¬A | y : x¬A ∈ Γ} and ΠΓ (x) as the set of non boxed formulas labelled by x: ΠΓ (x) = {A | A ∈ LCSL and x : A ∈ Γ}.

Denition 25. (Stati and dynami rules) We al l dynami the fol lowing rules:

(F2 ⇔), (F2x) and (F). We 
al l stati al l the other rules.

(Rules restri tions)

1. Do not apply a stati rule to Γ if at least one of the 
onsequen
es is already

in it.

2. Do not apply the rule (F2 ⇔) to a x : ¬(A ⇔ B), x : ¬**A, x** : ¬B
(a) if there exists some label y in Γ su
h that y : B and y : x¬A are in Γ .

(b) if there exists some label u su
h that u ⊏ x and ΠΓ (x) ⊆ ΠΓ (u).

3. Do not apply the rule (F2x) to a z : ¬x¬**A, x** : ¬A
(a) if there exists some label y in Γ su
h that y <x z , y : A and y : x¬A
are in Γ .

(b) if there exists some label u in Γ su
h that u ⊏ x and ΠΓ (x) ⊆ ΠΓ (u).

(
) if there exists some label v in Γ su
h that v ⊏ z and v : ¬x¬A ∈ Γ and Box+
Γ,x,z ⊆ Box+
Γ,x,v .

4. Do not apply the rule (F) to a x : ¬¬A in Γ if there exists some label y su h that y : A is in Γ .
(Systemati pro edure) (1) Apply stati rules as far as possible. (2) Apply a

(non blo ked) dynami rule to some formula label led x only if no dynami rule is appli able to a formula label led y, su
h that y ⊏ x.

We prove that a tableau initialized with a CSL-formula always terminates provided it is expanded a ording to Denition 25.