=Paper=
{{Paper
|id=None
|storemode=property
|title=Tableau-based Decision Procedure for Hybrid Logic with Satisfaction
Operators, Universal Modality and Difference Modality
|pdfUrl=https://ceur-ws.org/Vol-954/paper20.pdf
|volume=Vol-954
}}
==Tableau-based Decision Procedure for Hybrid Logic with Satisfaction
Operators, Universal Modality and Difference Modality==
https://ceur-ws.org/Vol-954/paper20.pdf
Tableau-based Decision Procedure for Hybrid
Logic with Satisfaction Operators, Universal
Modality and Difference Modality
Michal Zawidzki12
1
Department of Logic, University of Lodz
16/18 Kopcinskiego St., 90-232 Lodz, Poland
2
School of Computer Science, The University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
michal.zawidzki@gmail.com
Abstract. 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 in-
troduce a sound, complete and terminating tableau calculus TH(@,E,D) for
hybrid logics with satisfaction operators, universal modality and differ-
ence 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.
Keywords: hybrid logics, modal logics, tableau algorithms, decision
procedures, automated reasoning
1 Introduction
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.
R.K. Rendsvig and S. Katrenko (Eds.): ESSLLI 2012 Student Session Proceedings, CEUR Work-
shop Proceedings vol.: see http://ceur-ws.org/, 2012, pp. 191–201.
192 Michal Zawidzki
Some hybrid logics additionally contain a different sort of expressions, the state
variables, which allow quantifying over worlds, and additional operators like the down-
arrow operator or the state quantifiers. However, these logics are proven to be undecid-
able (cf. [1]) so, in principle, they cannot be subjected to a terminating tableau-based
decision procedure. We therefore confine ourselves only to the forgoing decidable hybrid
logic.
In the present paper we introduce a sound, complete and terminating tableau cal-
culus TH(@,E,D) for hybrid logics with @, E and D operators. Our approach, unlike that
in [7] and [3], is focused on the uniform treatment of all aforementioned logics, con-
ceptual simplicity and minimality of models generated by TH(@,E,D) . Basing on [10], we
introduce the unrestricted blocking mechanism that satisfies these conditions.
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 Hybrid logic
Syntax
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:
form ∋ ϕ := p | i | ¬ψ | ψ ∧ χ | ✸ψ | @i ψ | Eψ | Dψ,
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.
Semantics
A model M for hybrid logic H(@, E, D) is a triple hW, R, V i where:
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 ⇔ w ∈ V (p), p ∈ prop;
M, w |= i ⇔ {w} = V (i), i ∈ nom;
M, w |= ¬ϕ ⇔ M, w 6|= ϕ;
M, w |= ϕ ∧ ψ ⇔ M, w |= ϕ ∧˙ M, w |= ψ;
M, w |= ✸ϕ ⇔ ∃z ∈ W (wRz ∧˙ M, z |= ϕ);
M, w |= @i ϕ ⇔ {z} = v(i) ∧˙ M, z |= ϕ;
M, w |= Eϕ ⇔ ∃z ∈ W (M, z |= ϕ);
M, w |= Dϕ ⇔ ˙ w ∧˙ M, z |= ϕ),
∃z ∈ W (z 6=
Tableau-based Decision Procedure for Hybrid Logics 193
˙ |=, =
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)
Tableau calculi
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 ex-
pressions 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 cal-
culi. 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 [12], Bolander and Braüner (who improved Tzakova’s calculus to the
terminating version) [5], Kaminski and Smolka [8]. The tableau calculus for hybrid
logics obtained than the synthesised framework from [10] is also subsumed under the
prefixed calculi class.
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 condi-
tions (cf. [3]).
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 [2] modified by Bolander and Braüner in [5] and
by Blackburn and Bolander in [3]. However, certain rules have been added (e.g. the
rules for D).
Encoding the domain expressions
In [2] Blackburn made an observation that the language of hybrid logic with @ operators
is sufficiently rich to express semantics within itself. As we mentioned in Section 2,
there are three types of the domain expressions: satisfaction statements (M, w |= ϕ),
accessibility statements (wRv) and equality statements (w=v).
˙ Hybrid equivalents of
the forgoing expressions are shown below.
H(M, w |= ϕ) = @iw ϕ H(M, w 6|= ϕ) = @iw ¬ϕ
H(R(w, v)) = @iw ✸jv H(¬R(w, v)) = @iw ¬✸jv
˙ = @ i w jv
H(w=v) ˙ v) = @ix ¬jy
H(w6=
Both E and D operators allow mimicking @ operators: @i ϕ := E(i ∧ ϕ) and @i ϕ :=
(i ∧ ϕ) ∨ D(i ∧ ϕ). Therefore, in the calculus we use the notation i : ϕ, rather than @i ϕ,
to keep its universal character. This colon notation will stand for one of the forgoing
expressions, depending on a considered logic, except for the fact that whenever a logic
includes @ operators, i : ϕ means @i ϕ.
194 Michal Zawidzki
Rules for the connectives:
i : ¬j i : ¬¬ϕ i:ϕ∧ψ i : ¬(ϕ ∧ ψ)
(¬) (¬¬) (∧) (¬∧)
j:j i:ϕ i : ϕ, i : ψ i : ¬ϕ | i : ¬ψ
i : ✸ϕ i : ¬✸ϕ, i : ✸j i : @j ϕ i : ¬@j ϕ
(✸)∗ (¬✸) (@) (¬@)
i : ✸j, j : ϕ j : ¬ϕ j:ϕ j : ¬ϕ
i : Eϕ i : ¬Eϕ, j : j i : Dϕ i : ¬Dϕ, j : j
(E)∗ (¬E) (D) ∗
(¬D)
j:ϕ j : ¬ϕ i : ¬j, j : ϕ i : j | j : ¬ϕ
Equality rules:
i:ϕ i : j, i : ϕ
(ref) (sub)
i:i j:ϕ
Closure rule and unrestricted blocking rule:
i : ϕ, i : ¬ϕ i : i, j : j
(⊥) (ub)
⊥ i : j | i : ¬j
∗
Nominals in the conclusions are fresh on the branch.
Fig. 1. Rules for the calculus TH(@,E,D)
Tableau calculus
Figure 1 presents the rules of the tableau calculus TH(@,E,D) for the logic H(@, E, D).
Boolean rules are straightforward and require no additional comments. (✸), (E)
and (D) are rules introducing new labels, which was marked as the side-condition for
them. In the case of (¬E) and (¬D) the standard side-condition of former occurrence
of a label on a branch was replaced by introducing an explicit premiss stating that a
particular nominal has appeared as a label on a branch. The rule (ref) is a reflexivity
rule that introduces to a branch the explicit information that a nominal occurred as
a label within a branch. (sub) expresses the substitutability of two nominals as labels,
provided that one of them is labelled by the other. The (⊥) rule is self-evident. The
(ub) rule is a variant of the analytical cut rule applied to nominals. Intuitively, if two
labels appear on a branch, they either label two distinct worlds or the same world.
Thus, (ub) allows comparing any pair of labels that appeared on a branch. As it will
turn out before long, this possibility is essential for termination of the whole calculus.
The rule (¬D) deserves a wider comment. In [3] Blackburn and Bolander notice that
the (¬D) rule of the form
i : ¬Dϕ, i : ¬j
j : ¬ϕ
breaks the completeness of the whole calculus. In [8] Kaminski and Smolka formulate
(¬D) correctly but they do not explain why no such modification like from [3] can be
applied to (¬D). In [10] Schmidt and Tishkovsky introduce the (†) condition which
decides whether the refinement can be applied to a rule:
X0
Theorem 1 ([10]). Let T be a tableau calculus. Let β be the rule of the form X1 |···|X n
and let T R be a refined version of T. Suppose that B is an arbitrary open and fully-
expanded branch in a T R -tableau.Let F = {ϕ1 , . . . , ϕl } be a set of all K(En )-formulas
X0 ,¬Xi1 ,...,¬Xij
from B reflected in M(B). Then the refined rule Xij+1 |···|Xin
is admissible (i.e. the
Tableau-based Decision Procedure for Hybrid Logics 195
resulting calculus T R 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.
Proposition 1. !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.
Definition 6 (Tableau construction algorithm). Basic step: For a given input
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;
196 Michal Zawidzki
(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 ϕ.
Theorem 2. TH(@,E,D) is sound.
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 [3] and [5], we only consider missing cases.
Case: ψ = Dχ. We have i : Dχ ∈ B. After applying (D) we obtain i : ¬j ∈ B and j : χ ∈
B. By the inductive hypothesis we have that M(B), [j]!B |= χ. It suffices to show
that [i]!B and [j]!B are distinct. Suppose that they are the same equivalence
class. But then, by Def. 2, i : j ∈ B, which contradicts the fact that B is open.
Tableau-based Decision Procedure for Hybrid Logics 197
w0 w1 w2 w3 w0
...
{A(✸ϕ), ✸ϕ} {A(✸ϕ), ✸ϕ, ϕ} {A(✸ϕ), ✸ϕ, ϕ} {A(✸ϕ), ✸ϕ, ϕ} {A(✸ϕ), ✸ϕ, ϕ}
(a) (b)
Fig. 2. (a) and (b) present, respectively, an infinite and a finite (minimal) model for the
formula A(✸ϕ). Both of them can be obtained from a tableau if the (ub) rule is involved,
since it allows merging worlds in an arbitrary way, provided that the consistency is
preserved.
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.
Theorem 3. TH(@,E,D) is complete.
Proof. By Definition 7 and Lemma 1.
5 Termination of TH(@,E,D)
Exploiting the (ub) rule and the conditions (c1)-(c4) we show that TH(@,E,D) is ter-
minating 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. [11]).
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 ful-
filled, 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
198 Michal Zawidzki
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. [11]).
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
Tableau-based Decision Procedure for Hybrid Logics 199
progress of constructing B). We set a function f : W ′ −→ W as follows
[i]!B ,
if there is i : i ∈ B such that i was affixed
f (w) = 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. [4]) and the case of ψ = i
follows immediately from the definition of V ′ , we confine ourselves to proving the cases
of @i χ, Eχ and Dχ.
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 comple-
mentary 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(ϕ)) .
200 Michal Zawidzki
Consequently, we obtain the following result:
Theorem 4. TH(@,E,D) is terminating.
Proof. Follows from Corollary 1, Lemma 2 and Proposition 2.
Obviously, the bounding function µ from Proposition 2 can be reduced (cf. [1, 9]),
however, the main aim of this paper is not optimising the complexity of TH(@,E,D) . Be-
sides, the filtration-based argument can be easily adapted for different types of frames.
Thus, we formulate the following strategy-condition for performing the derivation in
TH(@,E,D) :
(tm) Expand a branch of TH(@,E,D) -tableau until the number of equivalence classes of
individuals in B exceeds the bound given by µ function. Then stop.
It turns our tableau calculus into a deterministic decision procedure.
6 Concluding remarks
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 [3] and [5] Blackburn, Bolander and Braüner provide a terminating internalised
tableau-based decision procedure for the logic H(@, E). However, their main concern is
different from ours. Their attempts are focused on tailoring a suitable tableau calculus
for each logic separately. Therefore, they introduce two different blocking mechanisms,
namely subset blocking and equality blocking for the logics H(@) and H(@, E) and
modify the notion of urfather subject to a particular logic. The resulting calculus is
conceptually complex but seems to avoid any superfluous performances of the rules.
In [7] Götzmann, Kaminski and Smolka describe Spartacus, which is a tableau prover
for hybrid logics with @ operators and universal modality. Thanks to the application
of advanced blocking and optimisation techniques, namely pattern-based blocking and
lazy branching the system is very efficient in terms of complexity.
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 [3] and [7] many of these configurations are superfluous.
However, the huge advantage of this approach is conceptual simplicity which allows
to avoid introducing complicated strategies of searching for a pair of labels that are
liable to blocking mechanism. Additionally, for each satisfiable formula ϕ (ub) ensures
that a minimal model for ϕ (in terms of a domain size) will be generated, which
cannot be guaranteed by the systems of [3] and [7]. Moreover, TH(@,E,D) provides a
uniform approach to all hybrid logics mentioned in the paper and covers the case of
difference modality which is omitted in [3]. A possible direction of future work may be
investigating whether the applications of the (ub) rule can be optimised.
Tableau-based Decision Procedure for Hybrid Logics 201
Acknowledgements
The research reported in this paper is a part of the project financed from the funds sup-
plied by the National Science Centre, Poland (decision no. DEC-2011/01/N/HS1/01979).
References
1. Areces C., Blackburn P., Marx M.: A road-map on complexity for hybrid logics.
Proc. of the 8th Annual Conference of the European Association for Computer
Science Logic (CSL 1999), Madrid, Spain, 307–321
2. Blackburn P.: Internalizing labelled deduction. J. Log. Comput. 10(1), 137—168
(2000)
3. Blackburn P., Bolander T.: Termination for Hybrid Tableaus. J. Log. Comput.
17(3), 517–554 (2007)
4. Blackburn P., Venema Y., de Rijke M.: Modal Logics. Cambridge University Press
(2002)
5. Bolander T., Braüner T.: Tableau-based Decision Procedures for Hybrid Logic. J.
Log. Comput. 16, 737–763 (2006)
6. Braüner T.: Hybrid Logic and its Proof-Theory Springer (2011)
7. Götzmann D., Kaminski M., Smolka G.: Spartacus: A Tableau Prover for Hybrid
Logic. Electron. Notes Ther. Comput. Sci. 262, 127-139 (2010)
8. Kaminski M., Smolka G.: Terminating Tableau Systems for Hybrid Logic with
Difference and Converse. J. Log. Lang. Inf. 18, 437–464 (2009)
9. Mundhenk M., Schneider T.: Undecidability of Multi-modal Hybrid Logics. Elec-
tron. Notes Ther. Comput. Sci. 174, 29–43 (2007)
10. Schmidt, R. A., Tishkovsky, D.: Automated Synthesis of Tableau Calculi. Log.
Meth. Comput. Sci. 7(2), 1–32 (2011)
11. Schmidt R.A., Tishkovsky D.: Using Tableau to Decide Description Logics with Full
Role Negation and Identity. http://www.mettel-prover.org/papers/ALBOid.pdf
(2012)
12. Tzakova M.: Tableau Calculi for Hybrid Logics. LNCS 1617, 278–292 (1999)