Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus TH(@,E,D) for hybrid logics with satisfaction operators, universal modality and difference modality. TH(@,E,D) not only uniformly covers relatively wide range of various hybrid logics but it is also conceptually simple and enables effective search for a minimal model for a satisfiable formula. TH(@,E,D) exploits the unrestricted blocking mechanism introduced as an explicit, sound tableau rule.
Hybrid logics are powerful extensions of modal logics which allow referring to particular states of a model without using meta-language. In order to achieve it, the language of standard modal logics is enriched with the countably infinite set of propositional expressions called nominals (we fix the notation nom = {i, j, k, . . . } to stand for the set of nominals), disjoint from the set of propositional variables prop. Each nominal is true at exactly one world and therefore can serve both as a label and as a formula. Supplying a language with nominals significantly strengthens its expressive power. In the presented paper we also consider further modifications of hybrid logic obtained by adding the so-called satisfaction operators, the universal modality and the difference modality. The satisfaction operators of the form @i allow stating that a particular formula holds at a world labelled by i. The universal modality E expresses the fact that there exists a world in a domain, at which a particular formula holds. The difference modality D stands for the fact that a particular formula holds at a world different from the current one.
Some hybrid logics additionally contain a different sort of expressions, the state
variables, which allow quantifying over worlds, and additional operators like the
downarrow operator or the state quantifiers. However, these logics are proven to be
undecidable (cf. [
In the present paper we introduce a sound, complete and terminating tableau
calculus TH(@,E,D) for hybrid logics with @, E and D operators. Our approach, unlike that
in [
In Section 2 a characterisation of the logic H(@, E, D) is provided. In Section 3 we introduce the tableau calculus TH(@,E,D) and we describe the decision procedure for H(@, E, D). In Section 4 we prove soundness and completeness of TH(@,E,D) and Section 5 provides a closer look at the termination problem for TH(@,E,D). We conclude the paper in Section 6. 2
Let O ∈ {@, E, D}. By H(O) we will denote the hybrid logic with operator(s) O.
We recursively define the set form of well-formed formulas of the logic H(@, E, D) in the following manner: where p ∈ prop, i ∈ nom and ψ, χ ∈ form.
Other connectives and operators are defined in a standard way. Both E and D have dual operators. @ is self-dual. We abbreviate ¬E¬ as A.
W 6= ∅ is called a domain, R ⊆ W 2 is called an accessibility relation, V : prop ∪ nom −→ P(W ) such that for each i ∈ nom V (i) is a singleton set; V is called a valuation function.
Relation |= (forcing) is defined inductively:
M, w |= p M, w |= i M, w |= ¬ϕ M, w |= ϕ ∧ ψ M, w |= ✸ϕ M, w |= Eϕ M, w |= Dϕ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ w ∈ V (p), p ∈ prop; {w} = V (i), i ∈ nom; M, w 6|= ϕ; M, w |= ϕ ∧˙ M, w |= ψ; ∃z ∈ W (wRz ∧˙ M, z |= ϕ); {z} = v(i) ∧˙ M, z |= ϕ; ∃z ∈ W (M, z |= ϕ); ∃z ∈ W (z 6 =˙ w ∧˙ M, z |= ϕ), where ⇔, ∃, ∧˙, |=, =˙ are meta-language symbols. Henceforth, we will call the expressions containing these meta-language symbols the domain expressions. 3
Synthesising tableau calculus for the logic H(@ E D)
, ,
Two main types of tableau calculi for hybrid logics are present in the literature, namely
the prefixed and the internalised calculi. The prefixed calculi consist in introducing
another sort of expressions, namely prefixes. They serve as labels for worlds, which,
unlike nominals, are of meta-linguistic provenience. Another type of meta-language
expressions occurring in prefixed tableaux are the accessibility expressions. The equality
between two prefixes is expressed implicitly by imposing on them the satisfaction of
the same nominal. Apparently, prefixed calculi are less complex than internalised
calculi. Besides, basic hybrid logic H is not supplied with sufficient expressive power to
internalise its own semantics. It therefore requires the domain expressions occurring in
the calculus. The most widely known prefixed tableau calculi for hybrid logics come
from Tzakova [
Internalised calculi for hybrid logics take advantage of the high expressive power
of these logics which allows encoding the domain expressions within the language.
Although internalisation of the logic allows dispensing with certain rules present in
prefixed tableau calculi, it also jeopardises termination of the calculus by, e.g., using
pure axioms (not including other formulas but nominals) to characterise frame
conditions (cf. [
In this section we present an internalised tableau calculus covering hybrid logics
with the satisfaction operators, the universal modality and the difference modality. It
resembles Blackburn’s calculus from [
In [
(¬) i : ¬j j : j (¬¬) i : ¬¬ϕ i : ϕ (∧) i : ϕ ∧ ψ i : ϕ, i : ψ (¬∧) i : ¬(ϕ ∧ ψ) i : ¬ϕ | i : ¬ψ (✸)∗ (E)∗ i : Eϕ j : ϕ
i : ✸ϕ i : ✸j, j : ϕ i : ¬✸ϕ, i : ✸j (¬✸) j : ¬ϕ (¬E) i : ¬Eϕ, j : j j : ¬ϕ (D)∗ i : Dϕ i : ¬j, j : ϕ (¬@) i : ¬@jϕ j : ¬ϕ (¬D) i : ¬Dϕ, j : j i : j | j : ¬ϕ
Closure rule and unrestricted blocking rule: ∗ Nominals in the conclusions are fresh on the branch.
(ref) i : ϕ i : i (sub) i : j, i : ϕ
j : ϕ (⊥) i : ϕ, i : ¬ϕ ⊥ (ub) i : i, j : j i : j | i : ¬j from B reflected in M(B). Then the refined rule X0X,¬ijX+i11|·,·.·.|.X,¬iXnij is admissible (i.e. the resulting calculus TR is still complete) satisfies the following condition is satisfied: If X0(ϕi1 , . . . , ϕik ) ∈ B then M(B) |= Xm(ϕi1 , . . . , ϕik ), for some m ∈ {1, . . . , n}. (†) (†) holds for (¬✸) in most modal and description logics but, as it turns out, it fails for (¬D).
Before we provide a proper method of constructing a tableau, we need to introduce several preliminary definitions.
Definition 1. We call a branch of a TH(@,E,D) tableau closed if the closure rule was applied on it. If a branch is not closed, it is open. An open branch is fully expanded if no other rules are applicable on it.
Definition 2. Let nom(B) be a set of nominals occurring as labels on a fully expanded branch B of a TH(@,E,D) tableau for a given input formula. We introduce the !B relation over nom(B) which we define in the following way:
i !B j iff i : j ∈ B.
!B is the equivalence relation.
Proof. Reflexivity is ensured by the (ref) rule. For symmetry assume that i : j is on B. By (ref) we obtain i : i and after applying (sub) to these two premises we obtain j : i. For transitivity suppose that i : j and j : k are on B. By symmetry we have that j : i is also on B. We therefore take j : i and j : k as premises of (sub) and obtain i : k. Definition 3. A rule of the TH(@,E,D) is applied eagerly in a tableau iff whenever it is applicable, it is applied.
Definition 4. Let ≺B be an ordering on nom(B) defined as follows: i ≺B j iff i : i occurred on B earlier than j : j.
Note that ≺B is well-founded and linear since no rule introduces more than 1 labelling nominal as a conclusion.
Definition 5. To each TH(@,E,D) rule we affix the priority number. It indicates what the order of application of particular rules should be. The lower the number is, the sooner the rule should be applied. We have: (ref), (¬): 1, (ub): 2, (sub):3, (¬¬), (∧), (¬∧): 4, (¬✸), (¬E), (¬D): 5, (✸), (E), (D): 6.
Now we are ready to provide the tableau construction algorithm. As usual, we do it inductively.
formula ϕ put i : ¬ϕ at the initial node. i is a nominal not occurring in ϕ. Inductive step: Suppose that you performed n steps of a derivation. In the n + 1th step apply the rules of TH(@,E,D) eagerly respecting the priority ordering given in Definition 5 and fulfilling the following conditions: (c1) if the application of a rule results in a formula that is already present on a branch, do not perform this application; (c2) rules of priority 5 and 6 can only by applied to labels that are the least elements (with respect to ≺B) of the equivalence class (with respect to !B); (c3) the (✸) must not be applied to formulas of the form i : ✸j. We call them the accessibility formulas; (c4) apply the (⊥) rule whenever it is possible.
If after the n + 1th step of derivation: (a) all tableau branches are closed, stop and return: theorem, (b) there are open branches in a tableau and no further rules are applicable (respecting conditions (c1)-(c4)), stop and return: non-theorem; (c) there are open branches in a tableau and further rules are applicable (respecting conditions (c1)-(c4)), proceed to the n + 2th step.
We will explain the way the (ub) rule works more carefully in Section 5. 4
Soundness and Completeness of TH(@,E,D) In the current section we state and prove soundness and completeness of the forgoing calculus. First, we formulate the following Definition 7. We call a tableau calculus T sound if and only if for each satisfiable input formula ϕ each tableau T(ϕ) is open, i.e., there exists a fully expanded branch on which no closure rule was applied. A tableau calculus is called complete if and only if for each unsatisfiable input formula ϕ there exists a closed tableau, i.e. a tableau where a closure rule was applied on each branch.
For soundness it amounts to proving that particular rules preserve satisfiability. For completeness we take the contrapositive of the condition given in Definition 7 and demonstrate that if there exists an open, fully expanded branch B in a tableau for ϕ then there exists a model for ϕ.
Proof. By easy verification of all the rules.
Suppose that B is an open, fully expanded branch in a TH(@,E,D) tableau for ϕ. We define a model M(B) = hW, R, V i derived from B in the following way: W = {[i]!B | i : i ∈ B}; R = {([i]!B , [j]!B ) | i : ✸j :∈ B}; V = {(i, [i]!B ) | i : i ∈ B} ∪ {(p, U ) | p ∈ prop, p occurred in B and U = {[i]!B | i : p ∈ B}}.
Lemma 1. Suppose that B is an open, fully expanded branch in a TH(@,E,D) tableau for ϕ. Then if i : ψ ∈ B then M(B), [i]!B |= ψ.
Proof. By induction on the complexity of ψ. Since all cases save ψ = Dχ and ψ = ¬Dχ
are covered by proofs given in [
{A(✸ϕ), ✸ϕ, ϕ} w0 (b)
Case: ψ = ¬Dχ. We have i : ¬Dχ ∈ B. If no labels different than i occurred on B, it means that W = {[i]!B } and therefore M(B), [i]!B |= ¬Dχ trivially holds. Suppose that L is a set of labels different than i, which occurred in B. Pick an arbitrary label j from L. After applying (¬D) to ¬Dχ we obtain that either i : j ∈ B or j : ¬χ ∈ B. If the former is the case, by the inductive hypothesis we obtain that [i]!B = [j]!B . If the latter holds, then by the inductive hypothesis, M(B), [j]!B |= ¬χ. Both cases are subsumed by M(B), [i]!B |= ¬Dχ. Since j was picked arbitrarily, we obtain the conclusion.
Proof. By Definition 7 and Lemma 1. 5 Exploiting the (ub) rule and the conditions (c1)-(c4) we show that TH(@,E,D) is terminating for the logic H(@, E, D), provided that it has the finite model property for a certain class of frames.
First, we make a remark that will be useful afterwards (cf. [
Remark 1. For each [i]!B the number of applications of the rules introducing a new label, namely (✸), (E), (D), to members of [i]!B is finite.
Proof. Indeed, if the (ub) is eagerly applied and the conditions (c2) and (c3) are fulfilled, it ensures that no superfluous application of (✸), (E), (D) is performed, since they are only applied to one member of [i]!B and are not applied to accessibility formulas (otherwise it would lead to an infinite derivation that could not be subjected to blocking). Since the input formula ϕ is assumed to be finite, therefore for each i that occurred in B [i]!B the number of (✸), (E), (D) applications is finite. Corollary 1. For each TH(@,E,D) tableau branch B is finite iff W of M(B) is finite.
Now we are ready to state the lemma that is essential for termination of TH(@,E,D). However, before we do this, we explain informally how the (ub) rule works. Our tableau calculus by default handles all distinct nominals that were introduced to a branch as labelling distinct worlds. It leads to a situation where a satisfiable formula having a simple model generates an infinite tableau (see Fig. 2 ). The (ub) rule compares all labels that occurred in a branch and its left conclusion merges each pair unless it leads to the inconsistency. As a consequence, if a formula has a model M of a certain cardinality, it will be reflected by a finite, fully expanded open branch of a TH(@,E,D) tableau. The reason is that the left conclusion of the (ub) rule decreases the cardinality of a model whenever possible, so a model of the cardinality not-greater than the cardinality of M will eventually be obtainable from one of the branches of a tableau. The formal argument is presented in the following lemma.
Lemma 2. Suppose that a finite model N = hW ′, R′, V ′i satisfies a formula ϕ. Then there exists an open branch B in a TH(@,E,D) tableau and M(B) = hW, R, V i such that Card(W ) ≤ Card(W ′).
Proof. We proceed by induction on the number of steps in the derivation. During the
derivation we construct a branch B in such a way that M(B) is partially isomorphic
to N (cf. [
Basic step: ϕ is satisfiable on N, so there must exist w ∈ W ′ such that N, w |= ϕ. If also N, w |= i such that i does not occur in ϕ, we put at the initial node of the derivation i : ϕ. If no such nominal holds in w, we conservatively extend N by adding fresh nominal i to w and put at the initial node of the derivation i : ϕ. Inductive step: Application of each tableau rule should be considered as a separate case. Nevertheless, only four rules seem to be essential for this proof, namely (✸), (E), (D) and (ub), i.e. rules that either introduce a new label to a branch or identify labels already present on a branch. We consider each of them.
Case: (✸). Suppose that a formula ✸ψ occurred at the nth node of the derivation. It means that we associated the label i of this node with a world in W ′ that satisfies ✸ψ and i. What follows, there must exist a world v such that wRv and N, v |= ψ. If v does not satisfy any nominal l that has not yet occurred on the branch either as a label or as a subformula, we conservatively extend N by ascribing l to v. Applying (✸) to ✸ψ we obtain i : ✸j and j : ψ. We put l in place of j.
Case: (E). Suppose that a formula Eψ occurred at the nth node of the derivation. It means that we associated the label i of this node with a world in W ′ that satisfies Eψ and i. Therefore, there exists a world v such that N, v |= ψ. If v does not satisfy any nominal l that has not yet occurred on a branch either as a label or as a subformula, we conservatively extend N by ascribing l to v. Applying (E) to Eψ we obtain j : ψ. We put l in place of j.
Case: (D). Suppose that a formula Dψ occurred at the nth node of the derivation. It means that we affixed the label i of this node to a world in W ′ that satisfies Dψ and i. Therefore, there exists a world v such that N, v |= ψ ∧ ¬i. If v does not satisfy any nominal l that has not yet occurred on a branch either as a label or as a subformula, we conservatively extend N by ascribing l to v. Applying (D). to Dψ we obtain j : ¬i and j : ψ. We put l in place of j.
Case: (ub). Suppose that during the derivation two labels i and j have been introduced to B. By the inductive hypothesis we mapped these labels to worlds w and v of (the conservative extension of) W ′. Either the world w satisfies i ∧ j (which would mean that w and v are the same world) or it satisfies i ∧ ¬j (which indicates that w and v are distinct). If the former is the case, we pick the left conclusion of (ub) and add it to B, if the latter is the case, we choose the right conclusion of (ub) and add it to B.
Since B is open, we can construct a model M(B) = hW, R, V i out of it. Now we show that Card(W ) ≤ Card(W ′) (we consider N as already conservatively extended in progress of constructing B). We set a function f : W ′ −→ W as follows if there is i : i ∈ B such that i was affixed to w during the derivation arbitrary element of W, otherwise f is injective and if we cut it to these elements of W ′ to which we assigned a nominal during the derivation, it is also an isomorphism. That concludes the proof.
To conclude our considerations it is sufficient to prove that the logic H(@, E, D) has the finite model property. The following proposition deals with it.
Proposition 2. The logic H(@, E, D) has the effective finite model property with the bounding function μ = 2Card(Sub(ϕ))+1, where Sub(ϕ) is a set of all subformulas of a formula φ.
Proof. We use the standard, filtration-based argument. Suppose that a formula ϕ is satisfied on a (possibly infinite) model M = hW, R, V i. It means that there exists w ∈ W such that M, w |= ϕ.We show that there exists a finite model M′ that satisfies ϕ and whose cardinality does not exceed 2Card(Sub(ϕ))+1.
First, we set the relation !ϕ on W in the following way: w !ϕ v iff
for all ψ ∈ Sub(ϕ) M, w |= ψ iff M, v |= ψ.
It is straightforward that !ϕ is the equivalence relation
Now we are ready to construct our finite model that will satisfy φ. Let M′ = hW ′, R′, V ′i such that:
W ′ = W/!ϕ ⊎ W/!ϕ ; R′ = {(|v|!ϕ , |u|!ϕ ) : R(v, u)}; V ′(p) = {|v|!ϕ : v ∈ V (p)} for all proposition letters in ϕ;
V ′(i) = {|v|!ϕ : v ∈ V (i)} for all nominals in ϕ.
We prove that M′ satisfies ϕ by induction on the complexity of subformulas of ϕ. Since
the proof for the modal part of H(@, E, D) is well known (cf. [
Case: ψ = @iχ. Suppose that M, v |= @iχ. It means that χ holds at a world u at which also i holds. This world is transformed to a singleton equivalence class {u} in W ′. By the inductive hypothesis it follows that M′, {u} |= i and M′, {u} |= χ. Hence M′, |v| |= @iχ.
Case: ψ = Eχ. Suppose that M, v |= Eχ. It means that there exists a world u at which χ holds. By the inductive hypothesis M′, |u| |= χ. Hence M′, |v| |= Eχ. Case: ψ = Dχ. Suppose that M, v |= Dχ. It means that there exists a world u different than v, at which χ holds. By the inductive hypothesis M′, |u| |= χ. Two complementary cases might occur. If |v| 6= |u|, then we obtain M′, |v| |= χ. If, however, |v| = |u|, it means that χ is also satisfied by a copy of |v| that we pasted to W ′ at the stage of the construction of M′. Since |v| and its copy are distinct, we obtain M′, |v| |= χ.
Observe that pasting a distinct copy of W/!ϕ to W ′ is only necessary if D is involved. Therefore, in other cases the bounding function μ = 2Card(Sub(ϕ)).
Consequently, we obtain the following result:
Proof. Follows from Corollary 1, Lemma 2 and Proposition 2.
Obviously, the bounding function μ from Proposition 2 can be reduced (cf. [
It turns our tableau calculus into a deterministic decision procedure. 6
In this paper we presented an internalised tableau-based decision procedure for the
logic H(@, E, D). Tableau calculus TH(@,E,D) was proven to be sound, complete and
terminating. In the existing literature of the subject several approaches to systematic
treatment of decision procedures for hybrid logics can be found. We recall two of them.
In [
The decision procedure introduced in this paper presents the approach which is
different from the aforementioned. It introduces (ub) as an explicit tableau rule which
is sound and, together with the conditions (c1)-(c4), ensures termination of the whole
calculus. (ub) allows a direct comparison of every pair of labels that occurred on a
branch and, therefore, subsumes any other blocking mechanisms. (ub) is a generic rule
which means that it generates every possible configuration of labels occurring on a
branch. In comparison to [
The research reported in this paper is a part of the project financed from the funds supplied by the National Science Centre, Poland (decision no. DEC-2011/01/N/HS1/01979).