Constraint Tableaux for Hybrid Logics Draft

Jan van Eijck

CWI and ILLC, Amsterdam, Uil-OTS, Utrecht

February 8, 2002

Abstract

Hybrid logics are modal logics with names for worlds. Tableau systems for various hybrid logics were proposed in [?, ?, ?]. We present an improved tableau system for hybrid logic that handles equality for nominals by substitution and generation of inequality constraints. This compiles out the equalities while storing the inequalities, thus allowing for efficient equality reasoning. The proof procedure based on the tableau calculus —the constraint proof engine — uses two other kinds of constraints: box constraints and inverse box constraints. Completeness of the system follows in the usual way from fairness of the proof procedure, together with a model generation argument.

Next, calculus and proof engine are extended to incorporate the universal modality. Among other things, universal modalities allow us to tune the proof engine to specific frame classes. This leads to a general completeness result for the calculus, for all frame classes that can be described by a Aφ formula. We also propose rules for minimal model generation, and a compression algorithm for generating minimal models from complete open tableau nodes. Finally, we focus on some fragments of hybrid logic that are decided by the constraint proof engine.

A theorem prover for hybrid logic based on the constraint proof engine, HyLoTab, has been implemented. A companion paper [?] contains the full code of of this implementation in Haskell [?], in ‘literate programming’ style [?]. This documented code can be found at

http://www.cwi.nl/~jve/hylotab.

Keywords: Hybrid logic, tableau reasoning, equality reasoning, model generation, decision methods.

MSC codes: 03B10, 03F03, 68N17, 68T15

1 Hybrid Logic: Syntax and Semantics

Our starting point is HL(@,˘ , ↓), a hybrid logic language [?, ?] with the following syntax. Assume p ranges over a set of propositions {p_{0}, p_{1}, …}, c over a set of constant nominals {c_{0}, c_{1}, …}, x over a set of variable nominals {x_{0}, x_{1}, …}, n over the sets of constant nominals {c_{0}, c_{1}, …} and variable nominals {x_{0}, x_{1}, …}, and i over a set of relation indices {i_{0}, i_{1}, …}. Then HL(@,˘ , ↓) is given by:

φ ::= ⊤ | ⊥ | p | c | x | ¬φ | φ ∧ φ′ | φ ∨ φ′ | φ → φ′ | [ i]φ | [ i]^{}φ̆ | ⟨ i ⟩φ | ⟨ i ⟩^{}φ̆ | @nφ |↓x.φ.

HL(@,˘ ) is the hybrid language that results from leaving out the binders ↓x.φ from HL(@,˘ , ↓), and HL(@) is the hybrid language that results from leaving out the converse modalities [ i]^{}φ̆ and ⟨ i ⟩^{}φ̆ from HL(@,˘ ).

Models for HL(@,˘ , ↓) consist of a set of woirld W, a set R = {R_{i} | i ∈ I} of binary relations on W, a valuation function V that maps proposition letters to subsets of W, and constant nominals to singleton subsets of W. Let M = (M, R, V) be such a model, and let w be a world from M. Let g be a valuation that maps variable nominals to members of W. Then the crucial clauses of the semantics for HL(@,˘ , ↓) are given by:

M, g, w ⊢⊢ p iff w ∈ V (p)
M, g, w ⊢⊢ c iff {w} = V (c)
M, g, w ⊢⊢ x iff w = g(x)
M, g, w ⊢⊢ [ i]φ iff for all w′ with wR_{i}w′ it holds that M, g, w′ ⊢⊢ φ
M, g, w ⊢⊢ ⟨ i ⟩φ iff for some w′ with wR_{i}w′ it holds that M, g, w′ ⊢⊢ φ
M, g, w ⊢⊢ [ i]^{}φ̆ iff for all w′ with w′R_{i}w it holds that M, g, w′ ⊢⊢ φ
M, g, w ⊢⊢ ⟨ i ⟩^{}φ̆ iff for some w′ with w′R_{i}w it holds that M, g, w′ ⊢⊢ φ
M, g, w ⊢⊢ @nφ iff M, g, w′ ⊢⊢ φ where {w′} = V (n)
M, g, w ⊢⊢ ↓x.φ iff M, g_{w}^{x}, w ⊢⊢ φ.

Here g_{w}^{x} is like g, except possibly for the fact that it maps x to w.

2 A Tableau Calculus for HL(@,˘ , ↓)

The tableau rules for HL(@,˘ , ↓) work on the labelled version of this language, with inequalities and access statements added. The tableau rules use the following language (φ ∈ HL(@,˘ , ↓)):

ψ ::= m ≉ n | mRn | @nφ.

We assume a linear ordering < on the set of nominals. An inequality m ≉ n generated by the tableau rules will always satisfy m ≤ n. Inequalities m ≉ m are written as ⊥.

As in [?, ?], the tableau rules are rules for labelled formulas. In fact, the tableau system of this paper is a variation on these calculi, with a different approach to equality reasoning for nominals.

The [ i] and [ i]^{}˘ rules are the only rules that cannot be treated once and for all in the proof procedure. They have the ‘standing order’ nature of the γ tableau rules in first order logic [?]. In the proof procedure based on the calculus they are translated into constraints (see Section ??).

Conjunctive rules (α rules)

\frac{@m(φ ∧ ψ)}{\begin{matrix}@mφ \\ @mψ \end{matrix}}  \frac{@m¬(φ ∨ ψ)}{\begin{matrix}@m¬φ \\ @m¬ψ \end{matrix}}  \frac{@m¬(φ → ψ)}{\begin{matrix}@mφ \\ @m¬ψ \end{matrix}}

Disjunctive rules (β rules)

\frac{@m(φ ∨ ψ)}{@mφ | @mψ}  \frac{@m¬(φ ∧ ψ)}{@m¬φ | @m¬ψ}  \frac{@m(φ → ψ)}{@m¬φ | @mψ}

Negation rule As this is a single-sided calculus, the only negation rule we need is the rule for double negation.

\frac{@m¬¬φ}{@mφ}

[ i] rules Like the γ rules in FOL tableaux, these are ‘standing orders’.

\frac{@m[ i]φ, mR_{i}n}{@nφ}  \frac{@m¬⟨ i ⟩φ, mR_{i}n}{@n¬φ}

⟨ i ⟩ rules

\frac{@n⟨ i ⟩φ}{\begin{matrix}nR_{i}m \\ @mφ \end{matrix}} φ not a nominal, m fresh  \frac{@n¬[ i]φ}{\begin{matrix}nR_{i}m \\ @m¬φ \end{matrix}} φ not a negated nominal, m fresh

[ i]^{}˘ rules Like the γ rules in FOL tableaux, these are ‘standing orders’.

\frac{@m[ i]^{}φ̆, nR_{i}m}{@nφ}  \frac{@m¬⟨ i ⟩^{}φ̆, nR_{i}m}{@n¬φ}

⟨ i ⟩^{}˘ rules

\frac{@n⟨ i ⟩^{}φ̆}{\begin{matrix}mR_{i}n \\ @mφ \end{matrix}} φ not a nominal, m fresh  \frac{@n¬[ i]^{}φ̆}{\begin{matrix}mR_{i}n \\ @m¬φ \end{matrix}} φ not a negated nominal, m fresh

Access rules Formulas of the forms ⟨ i ⟩n, ¬[ i]¬n, ⟨ i ⟩^{}n̆, ¬[ i]^{}˘ ¬n, are called access formulas. They are treated by a separate rule.

\frac{@n⟨ i ⟩m}{nR_{i}m}  \frac{@n¬[ i]¬m}{nR_{i}m}  \frac{@n⟨ i ⟩^{}m̆}{mR_{i}n}  \frac{@n¬[ i]^{}˘ ¬m}{mR_{i}n}

Label rules

\frac{@m@nφ}{@nφ}  \frac{@m¬@nφ}{@n¬φ}

Nominal substitution Here comes the new element, a substitution rule that makes use of the fact that nominals are unique names. B_{s}^{t} is the result of substituting s for t everywhere in tableau branch B. The rules make use of the linear order < on nominals.

\frac{B + @mm}{B} \frac{B + @mn}{B_{s}^{t}}s = min(m, n), t = max(m, n)

Inequality generation Write ⊥ for m ≉ m.

\frac{@m¬m}{⊥} \frac{@m¬n}{s ≉ t} s = min(m, n), t = max(m, n)

\frac{@mφ, @m¬φ}{⊥} \frac{@mφ, @n¬φ}{s ≉ t} s = min(m, n), t = max(m, n)

The rule that derives an inequality constraint from @mφ, @n¬φ is a so-called admissible rule. It does not change the set of formulas that can be refuted or proved satisfiable, but admitting it to the calculus may shorten some tableau proofs.

Binding rules

\frac{@m ↓x.φ}{@mφ_{m}^{x}}  \frac{@m¬ ↓x.φ}{@m¬φ_{m}^{x}}

Here φ_{m}^{x} denotes the result of substituting m for all free occurrences of x in φ.

Tableau Closure A tableau branch is closed if it contains ⊥. A tableau is closed if all its branches are closed. Note that nominal substitution can lead to branch closure.

3 Examples of Refutation Proofs, for HL(@)

Figure ?? gives a tableau refutation of (??), with the active formulas of the branch repeated at each node. Figure ?? gives another version of this, without repetition of formulas, but with the substitution instructions indicated along the branch.

@m(◇(i ∧ p) ∧ ◇(i ∧ q) ∧ □(¬p ∨ ¬q)) ; @m◇(i ∧ p), @m◇(i ∧ q), @m□(¬p ∨ ¬q) ; mRn, @n(i ∧ p), @m◇(i ∧ q), @m□(¬p ∨ ¬q) ; mRn, @ni, @np, @m◇(i ∧ q), @m□(¬p ∨ ¬q) ; mRi, @ip, @m◇(i ∧ q), @m□(¬p ∨ ¬q) ; mRi, @ip, mRk, @k(i ∧ q), @m□(¬p ∨ ¬q) ; mRi, @ip, mRk, @ki, @kq, @m□(¬p ∨ ¬q) ; mRi, @ip, @iq, @m□(¬p ∨ ¬q) ; \begin{matrix}mRi, @ip, @iq, @m□(¬p ∨ ¬q), @i(¬p ∨ ¬q) \\ \begin{matrix}mRi, @ip, @iq, \\ @m□(¬p ∨ ¬q), @i¬p \end{matrix} ; ⊥ & \begin{matrix}mRi, @ip, @iq, \\ @m□(¬p ∨ ¬q), @i¬q \end{matrix} ; ⊥ \end{matrix}

Figure 1: Tableau refutation for (??).

@m(◇(i ∧ p) ∧ ◇(i ∧ q) ∧ □(¬p ∨ ¬q)) ; @m◇(i ∧ p), @m◇(i ∧ q), @m□(¬p ∨ ¬q) ; mRn, @n(i ∧ p) ; @ni, @np ; n ↦ i ; mRk, @k(i ∧ q) ; @ki, @kq ; k ↦ i ; \begin{aligned}& @i(¬p ∨ ¬q) \\ \begin{matrix}@i¬p \\ ⊥ \end{matrix} & & \begin{matrix}@i¬q \\ ⊥ \end{matrix} \end{aligned}

Figure 2: Tableau refutation for (??), without formula repetition.

@m(◇(i ∧ p) ∧ ◇(i ∧ q) ∧ □(¬p ∨ ¬q)).  (1)

The tableau refutation of (??) proves the validity of ◇(i ∧ p) ∧ ◇(i ∧ q) → ◇(p ∧ q), which expresses that if from the current world i is accessible, and at i both p and q hold, then from the current world a p ∧ q world is accessible.

@m¬((◇p ∧ ◇¬p) → (□(q → i) → ◇¬q)) ; @m(◇p ∧ ◇¬p), @m¬(□(q → i) → ◇¬q) ; @m◇p, @m◇¬p, ; @m□(q → i), @m¬◇¬q ; mRn, @np ; mRk, @k¬p ; @n(q → i), @nq ; \begin{aligned}& @k(q → i), @kq \\ \begin{matrix}@n¬q \\ ⊥ \end{matrix} & @ni ; \begin{aligned}& n ↦ i \\ \begin{matrix}@k¬q \\ ⊥ \end{matrix} & & @ki ; \begin{matrix}k ↦ i \\ ⊥ \end{matrix} \end{aligned} \end{aligned}

Figure 3: Tableau refutation for @m¬((◇p ∧ ◇¬p) → (□(q → i) → ◇¬q)) .

Figure ?? gives a tableau refutation of @m¬((◇p ∧ ◇¬p) → (□(q → i) → ◇¬q)). The nominal substitutions n ↦ i and k ↦ i act on the formulas @np and @k¬p to give @ip, @i¬p on the branch, and therefore branch closure. The tableau refutation proves the validity of ((◇p ∧ ◇¬p) → (□(q → i) → ◇¬q)), a principle which expresses that if from the current world there are at least two worlds accessible, and if i is the only accessible q world, then there has to be an accessible ¬q world.

4 Examples of Model Generation, for HL(@)

@m(◇◇m ∧ ¬◇m) ; @m◇◇m, @m¬◇m ; mRn, @n◇m ; @n¬m ; n ≉ m ; \begin{matrix}nRk, @km \\ m ↦ k \end{matrix}

Figure 4: Open tableau for @m(◇◇m ∧ ¬◇m).

Figure ?? gives an open tableau for @m(◇◇m∧¬◇m). Since the formula contains no proposition letters, it defines a frame property. The smallest frame with the property is • ↔ •.

Figure ?? gives an open tableau for @m(◇i ∧ ◇j ∧ ◇k ∧ @i¬j ∧ @j¬k ∧ @i¬k).

Figure ?? shows that the formula ◇(c ∧ ◇c ∧ □◇c) is satisfiable. Note that this formula causes the first of the two tableau proof procedures in [?] to loop.

5 Examples of the treatment of ↓

Figure ?? gives a closed tableau for @m ↓ x.□◇x∧¬(◇□p → p). The formula ↓ x.□◇x holds at the point m if mRn implies nRm. The formula ◇□p → p is true at points where R is symmetric. Therefore, ↓ x.□◇x → (◇□p → p) is valid.

In HL(↓, @) it is easy to describe situations that only have infinite models. Figure ?? gives an infinite tableau for (??).

@s(◇⊤ ∧ □□ ↓ x.@s◇x ∧ □(◇⊤ ∧ φ)),  (2)

@m(◇i ∧ ◇j ∧ ◇k ∧ @i¬j ∧ @j¬k ∧ @i¬k) ; @m◇i, @m◇j, @m◇k, @m@i¬j, @m@j¬k, @m@i¬k ; mRi, mRj, mRk ; \begin{matrix}@i¬j, @j¬k, @i¬k \\ i ≉ j, j ≉ k, i ≉ k \end{matrix}

Figure 5: Open tableau for @m(◇i ∧ ◇j ∧ ◇k ∧ @i¬j ∧ @j¬k ∧ @i¬k).

@m◇(c ∧ ◇c ∧ □◇c) ; mRn, @n(c ∧ ◇c ∧ □◇c) ; @nc, @n◇c, @n□◇c ; n ↦ c ; cRc, @c□◇c ; \begin{matrix}@c◇c \\ cRc \end{matrix}

Figure 6: Open tableau for ◇(c ∧ ◇c ∧ □◇c).

@m(↓ x.□◇x ∧ ¬(◇□p → p)) ; @m ↓ x.□◇x, @m¬(◇□p → p) ; @m□◇m ; @m◇□p, @m¬p ; mRn, @n□p ; @n◇m ; nRm ; \begin{matrix}@mp \\ ⊥ \end{matrix}

Figure 7: Closed tableau for @m ↓ x.□◇x ∧ ¬(◇□p → p).

@s(◇⊤ ∧ □□ ↓ x.@s◇x ∧ □(◇⊤ ∧ φ)) ; @s◇⊤, @s□□ ↓ x.@s◇x, @s□(◇⊤ ∧ φ) ; sRt ; @t◇⊤, @tφ ; tRt′ ; @t□ ↓ x.@s◇x ; @t′ ↓ x.@s◇x ; @t′@s◇t′ ; @s◇t′ ; sRt′ ; @t′◇⊤, @t′φ ; t′Rt′′ ; ⋮

Figure 8: Infinite tableau for (??). where φ is the formula

↓ x.□¬x∧ ↓ x.□□¬x∧ ↓ x.□□ ↓ y.@x◇y.

The formula ↓ x.□¬x expresses irreflexivity, the formula ↓ x.□□¬x asymmetry, the formula ↓ x.□□ ↓ y.@x◇y transitivity. Formula (??) expresses that from the spypoint s a serial, irreflexive, asymmetric and transitive, hence infinite, relation is visible.

6 From Tableau Calculus to Proof Engine

A proof procedure (or proof engine) for φ is a systematic search for a Kripke model satisfying φ, by means of a search tree starting out from a node start φ. Our proof engine for hybrid logic based on the calculus given above is presented in Figure ??. The proof rules work on tuples (U, A, I, P, N, C, F) consisting of a node universe (or node domain) U, a list of accessibilities A, a list of inequality constraints I, a list of positive propositional attributions P, a list of negative propositional attributions N, a list of box constraints and converse box constraints C, and a list of pending formulas F. Write φ : F for the list with head φ and tail F, and F_{1} ++F_{2} for the result of concatenating lists F_{1}, F_{2}. Write [] for the empty list, [φ] for the unit list with φ as its element, and [φ_{1}, … φ_{n}] for the list consisting of φ_{1} through φ_{n}. We will assume throughout that the lists do not contain duplicates, i.e., that the lists behave as ordered sets. In particular, U_{t}^{s} means that s gets replaced by t in U, and the duplicate of t that this may generate is removed.

The table uses abbreviations φ ∈ α, φ ∈ β, φ ∈ [ i], φ ∈ ⟨ i ⟩, φ ∈ [ i]^{}˘ , φ ∈ ⟨ i ⟩^{}˘ for “φ is an α formula”, and so on. We do not count ⟨ i ⟩n or ⟨ i ⟩^{}n̆ or ¬[ i]¬n or ¬[ i]^{}˘ ¬n as ⟨ i ⟩ or ⟨ i ⟩^{}˘ formulas, as these ‘access formulas’ are treated by a separate rule. If φ ∈ α ∪ β, the components of φ are referred to as φ_{1}, …, φ_{n}. If φ ∈ [ i] ∪ ⟨ i ⟩ ∪ [ i]^{}˘ ∪ ⟨ i ⟩^{}˘ , its component is referred to as φ′.

The key to understanding the table is the following invariant of the rule applications: the constraint store of the node contains only constraints that have been combined with all access relations of the node. This invariant may get destroyed when a new access relation gets added, when a new constraint gets added, or when a substitution is applied to a node. In all such cases, the invariant is restored by applying the appropriate constraints, thus generating extra material on the pending formula list.

Here is what has to happen in the case of applying a substitution to a node:

• If the substitution results in new access relations, these get combined with all box and converse box constraints of the node.

• If the substitution results in new box constraints, these get combined with all access relations of the node.

• If the substitution results in new converse box constraints, these get combindew ith all access relations of the node.

In the substitution rule in the table, this procedure is abbreviated as ‘add stuff to restore the invariant’.

\frac{start φ}{[m], [], [], [], [], [], [@mφ]} m fresh

\frac{U, A, I, P, N, C, F}{closure} ⊥ ∈ I ∨ P ∩ N ≠ ∅ \frac{U, A, I, P, N, C, []}{success} ⊥ ∉ I, P ∩ N = ∅

\frac{U, A, I, P, N, C, (@mφ : F)}{U, A, I, P, N, C, [@mφ_{1}, …, @mφ_{n}] ++F} φ ∈ α

\frac{U, A, I, P, N, C, (@mφ : F)}{U, A, I, P, N, C, (@mφ_{1} : F) | ⋯ | U, A, I, P, N, C, (@mφ_{n} : F)} φ ∈ β

\frac{U, A, I, P, N, C, (@m¬¬φ : F)}{U, A, I, P, N, C, (@mφ : F)}

\frac{U, A, I, P, N, C, (@mp : F)}{U, A, I, (@mp : P), N, C, F}  \frac{U, A, I, P, N, C, (@m¬p : F)}{U, A, I, P, (@np : N), C, F}

\frac{U, A, I, P, N, C, (@mn : F)}{U_{s}^{t}, A_{s}^{t}, I_{s}^{t}, P_{s}^{t}, N_{s}^{t}, C_{s}^{t}, F_{s}^{t} ++F′} s = min(m, n), t = max(m, n), F′ = stuff to restore invariant

\frac{U, A, I, P, N, C, (@m¬n : F)}{U, A, (s ≉ t : I), P, N, C, F} s = min(m, n), t = max(m, n)

\frac{U, A, I, P, N, C, (@m@nφ : F)}{U, A, I, P, N, C, (@nφ : F)}  \frac{U, A, I, P, N, C, (@m¬@nφ : F)}{U, A, I, P, N, C, (@n¬φ : F)}

\frac{U, A, I, P, N, C, (@mφ : F)}{U, A, I, P, N, (@mφ : C), F ++ [@nφ′ | mR_{i}n ∈ A]} φ ∈ [ i]

\frac{U, A, I, P, N, C, (@m⟨ i ⟩n : F)}{U, (mR_{i}n : A), I, P, N, C, F + ++ [@nψ | @m[ i]ψ ∈ C] ++ [@mψ | @n[ i]^{}ψ̆ ∈ C]}

\frac{U, A, I, P, N, C, (@mφ : F)}{(n : U), (mR_{i}n : A), I, P, N, C, (@nφ′ : F) ++ [@nψ | @m[ i]ψ ∈ C]} φ ∈ ⟨ i ⟩, n fresh

\frac{U, A, I, P, N, C, (@mφ : F)}{U, A, I, P, N, (@mφ : C), F ++ [@nφ′ | nR_{i}m ∈ A]} φ ∈ [ i]^{}˘

\frac{U, A, I, P, N, C, (@m⟨ i ⟩^{}n̆ : F)}{U, (nR_{i}m : A), I, P, N, C, F ++ [@mψ | @n[ i]ψ ∈ C]F ++ [@nψ | @m[ i]^{}ψ̆ ∈ C]}

\frac{U, A, I, P, N, C, (@mφ : F)}{(n : U), (nR_{i}m : A), I, P, N, C, (@nφ′ : F) ++ [@nψ | @m[ i]^{}ψ̆ ∈ C]} φ ∈ ⟨ i ⟩^{}˘ , n fresh

\frac{U, A, I, P, N, C, (@m ↓ x.φ : F)}{U, A, I, P, N, C, (@mφ_{m}^{x} : F)}  \frac{U, A, I, P, N, C, (@m¬ ↓ x.φ : F)}{U, A, I, P, N, C, (@m¬φ_{m}^{x} : F)}

Figure 9: Constraint Proof Engine for HL(@,˘ , ↓).

Closure, Success A node (U, A, I, P, N, C, F) is closed if either ⊥ ∈ I or P ∩N ≠ ∅, otherwise it is open. An open node (U, A, I, P, N, C, F) is a success node if it has F = []. A node is incomplete if it is neither closed nor a success node.

Selection Rule To develop an incomplete node, use the table from Figure ??. Since an incomplete node contains a non-empty list of pending formulas, and the table has exactly one rule that applies to the head φ of the pending formula list, this specifies the selection rule of the proof engine.

Search Rule To select an incomplete leaf node to develop, use any breadth first search method for tree traversal. This specifies a search rule for the proof engine.

Termination Condition The proof procedure ends when there are no more nodes to develop. The proof procedure can be used both for satisfiablity checking and for refutation. For satisfiability checking, the satisfiability procedure outputs true when a success node is encountered, and outputs false if the proof procedure ends with closed nodes at all leaves. For refutation, the refutation procedure outputs false when a success node is encountered, and outputs true if the proof procedure ends with closed nodes at all leaves.

7 Soundness, Fairness of Proof Engine, Completeness

Theorem 1 The tableau calculus for HL(@,˘ , ↓) is sound.

Proof. By an easy inspection, all tableau rules are sound. Soundness of the calculus follows from this by induction on tableau structure. □

For completeness, we need a fair proof procedure P. Consider the (possibly infinite) set of tableaux for formula φ, according to procedure P. Since P determines which rule (selection) to apply to which node (search), this tableau set is ordered. The successor of a tableau T is tableau T′ computed from T according to P. Let T_{0} be the initial tableau for φ. Then there is a possibly infinite ascending chain T_{0}, … of tableaux for φ. By Zorn’s lemma, this chain has a supremum T_{∞}.

A proof procedure for hybrid logic is fair if the following hold for all open branches B in T_{∞}:

1. All formulas of type α ∪ β ∪ (¬¬) ∪ @ ∪ ↓ ∪ ⟨ i ⟩ ∪ ⟨ i ⟩^{}˘ on B were used to expand B.

2. All formulas of type [ i] or [ i]^{}˘ on B were combined with all mR_{i}n accessibilities on B to expand B.

Theorem 2 The Constraint Proof Engine of Section ?? is fair.

Proof. Inspection of the table in Figure ?? makes clear that (1) is satisfied. That (2) is also satisfied follows from an induction argument: it can be proved by induction on path length that the constraint sets B and C at each node N consist of exactly the [ i] ∪ [ i]^{}˘ formulas at the node that were used to expand all appropriate mR_{i}n accessibilities introduced on the path along B from the root up to N. Finally, note that formulas resulting from combining an accessibility relation mR_{i}n and a constraint @m[ i]φ or @n[ i]^{}φ̆ are appended to the list of pending formulas, thus ensuring that every formula on the pending formula list will eventually get treated. □

Call a tableau finished if it does not contain incomplete end nodes. It is easy to see that each limit tableau T_{∞} is finished. Every open branch of a finished tableau for φ yields a Kripke model for φ: take the nominals as worlds, put m ⟶^{i} n if a mR_{i}n relation occurs along the branch, make all proposition letters p with @mp along the branch true at m, and all other proposition letters false at m. From the facts that the tableau is finished and that the branch is open it follows that this model is well-defined, and from the fact that the tableau rules are truth preserving in both directions it follows that it is indeed a model for φ.

Theorem 3 The tableau calculus for HL(@,˘ , ↓) is complete.

Proof. Immediate from Theorem ??, plus the fact that every open branch of a finished tableau for φ yields a Kripke model for φ. □

8 Adding the Universal Modality

Let us now extend the language with the universal modality A and its dual E, with the following intended meanings:

M, g, w ⊢⊢ Aφ iff for all w′ ∈ M it holds that M, g, w′ ⊢⊢ φ
M, g, w ⊢⊢ Eφ iff for some w′ ∈ M it holds that M, g, w′ ⊢⊢ φ

It is well known that binding together with universal modality makes it possible to express full quantification. Indeed, ∀xφ can be taken as shorthand for A ↓ xφ, and ∃xφ as shorthand for E ↓ xφ.

Tableau rules for A and E can look like this:

\frac{@mAφ}{@nφ} n on the branch \frac{@m¬Eφ}{@n¬φ} n on the branch

\frac{@mEφ}{@nφ} n fresh \frac{@m¬Aφ}{@n¬φ} n fresh

Since the tableau rules for A and E are obviously sound, we get by induction on tableau structure:

Theorem 4 The tableau calculus for HL(@,˘ , ↓, A) is sound.

Figure ?? lists the modifications in the constraint proof engine that are necessary to accommodate the universal modality. The conditions φ ∈ A, φ ∈ E have the obvious meanings. A-type formulas are of the forms Aψ, with component ψ, and ¬Eψ, with component ¬ψ. E-type formulas are of the forms Eψ, with component ψ, and ¬Aψ, with component ¬ψ. The constraint

\frac{U, A, I, P, N, C, (@mφ : F)}{(n : U), A, I, P, N, C, (@nφ′ : F) ++ [@nψ | Aψ ∈ C]} φ ∈ E, n fresh

\frac{U, A, I, P, N, C, (@mφ : F)}{U, A, I, P, N, (φ : C), F ++ [@nφ′ | n ∈ U]} φ ∈ A

\frac{U, A, I, P, N, C, (@m⟨ i ⟩n : F)}{U, (mR_{i}n : A), I, P, N, C, F ++ [@nψ | @m[ i]ψ ∈ C] ++ [@mψ | @n[ i]^{}ψ̆ ∈ C] ++ [@mψ | Aψ ∈ C]}

\frac{U, A, I, P, N, C, (@mφ : F)}{(n : U), (mR_{i}n : A), I, P, N, C, (@nφ′ : F) ++ [@nψ | @m[ i]ψ ∈ C] ++ [@nψ | Aψ ∈ C]} φ ∈ ⟨ i ⟩, n fresh

\frac{U, A, I, P, N, C, (@m⟨ i ⟩^{}n̆ : F)}{U, (nR_{i}m : A), I, P, N, C, F ++ [@nψ | @m[ i]^{}ψ̆ ∈ C] ++ [@nψ | Aψ ∈ C]}

\frac{U, A, I, P, N, C, (@mφ : F)}{(n : U), (nR_{i}m : A), I, P, N, C, (@nφ′ : F) ++ [@nψ | @m[ i]^{}ψ̆ ∈ C] ++ [@nψ | Aψ ∈ C]} φ ∈ ⟨ i ⟩^{}˘ , n fresh

Figure 10: Modified Constraint Proof Engine for HL(@,˘ , ↓, A).

store C now also contains universal formulas Aψ, and the corresponding constraints have to be imposed on all nominals that turn up at the branch.

The results about fairness and completeness extend to the new calculus and proof engine:

Theorem 5 The modified Constraint Proof Engine of Figure ?? is fair.

Theorem 6 The tableau calculus for HL(@,˘ , ↓, A) is complete.

9 Tuning the Engine: Proof Procedures for Frame Classes

The calculus and proof engine give a systematic search for Kripke models, without imposing any constraint on the kind of Kripke model. In other words, it interprets ‘validity’ as ‘validity in models based on the class of all Kripke frames’. It is straightforward to adapt our reasoning engine for hybrid logic to other frame classes than the universal frame class. Since we have a way of dealing with the universal modality, the only thing we have to do is modify the start rule, by storing the appropriate constraint for the frame class we want. Here are some examples:

Irreflexive Frames for R_{i} Modify the start rule to:

\frac{start φ}{[m], [], [], [], [], [A ↓ x.[ i]¬x], [@mφ]} m fresh

Reflexive Frames for R_{i} Modify the start rule to:

\frac{start φ}{[m], [], [], [], [], [A ↓ x.⟨ i ⟩x], [@mφ]} m fresh

Transitive Frames for R_{i} Modify the start rule to:

\frac{start φ}{[m], [], [], [], [], [A ↓ x.[ i][ i]⟨ i ⟩^{}x̆], [@mφ]} m fresh

S4 Frames for R_{i} Modify the start rule to:

\frac{start φ}{[m], [], [], [], [], [A ↓ x.(⟨ i ⟩x ∧ [ i][ i]⟨ i ⟩^{}x̆)], [@mφ]} m fresh

It is obvious that this can be done for any frame class that can be described (hence characterized) by a universal formula. This gives the following:

Theorem 7 (General Completeness) The tableau calculus for HL(@,˘ , ↓, A) is complete for any frame class that can be described by a hybrid formula of the form Aφ.

10 Modifying the Calculus for Minimal Model Generation

A model M is minimal for φ if there are g, w with M, g, w ⊢⊢ φ, and for all N , h, w′ with N , h, w′ ⊢⊢ φ it holds that |N| ≥ |M|. E.g., the formula ¬c ∧ □◇⊤ has minimal models of size 2.

To generate minimal models, replace the ⟨ i ⟩ and ⟨ i ⟩^{}˘ rules by the following trial-and-error versions:

⟨ i ⟩ rules, trial-and-error version

\frac{@n⟨ i ⟩φ}{\begin{matrix}nRk_{1} \\ @k_{1}φ \end{matrix} | ⋯ | \begin{matrix}nRk_{s} \\ @k_{s}φ \end{matrix} | \begin{matrix}nRm \\ @mφ \end{matrix}} k_{1}, … k_{s} all nominals on the branch, m fresh

\frac{@n¬[ i]φ}{\begin{matrix}nRk_{1} \\ @k_{1}¬φ \end{matrix} | ⋯ | \begin{matrix}nRk_{s} \\ @k_{s}¬φ \end{matrix} | \begin{matrix}nRm \\ @m¬φ \end{matrix}} k_{1}, … k_{s} all nominals on the branch, m fresh

\frac{@n¬[ i]φ}{\begin{matrix}nRk_{1} \\ @k_{1}¬φ \end{matrix} | ⋯ | \begin{matrix}nRk_{s} \\ @k_{s}¬φ \end{matrix} | \begin{matrix}nRm \\ @m¬φ \end{matrix}} k_{1}, … k_{s} all nominals on the branch, m fresh

⟨ i ⟩^{}˘ rules, trial-and-error version

\frac{@n⟨ i ⟩^{}φ̆}{\begin{matrix}k_{1}Rn \\ @k_{1}φ \end{matrix} | ⋯ | \begin{matrix}Rk_{s}Rn \\ @k_{s}φ \end{matrix} | \begin{matrix}mRn \\ @mφ \end{matrix}} k_{1}, … k_{s} all nominals on the branch, m fresh

\frac{@n¬[ i]^{}φ̆}{\begin{matrix}k_{1}Rn \\ @k_{1}¬φ \end{matrix} | ⋯ | \begin{matrix}k_{s}Rn \\ @k_{s}¬φ \end{matrix} | \begin{matrix}mRn \\ @m¬φ \end{matrix}} k_{1}, … k_{s} all nominals on the branch, m fresh

Figure ?? gives an infinite tableau expansion for Formula (??).

@s◇¬s ∧ @s□ ↓ x.◇(¬s ∧ ¬x) ∧ @s□□ ↓ x.@s◇x  (3)

Still, the formula has finite models, and we can find finite models of minimal size by means of (the proof engine based on) the trial-and-error version of the tableau system. See Figure ??.

Again, the new rules are obviously sound, so we get:

Theorem 8 The minimal model calculus for HL(@,˘ , ↓, A) is sound.

The rules lead to an obvious modification of the proof engine, which gives us a fair proof procedure for minimal model generation. From this, by the same reasoning as above:

Theorem 9 The minimal model calculus for HL(@,˘ , ↓, A) is complete.

11 Generation of Minimal Models Through Node Compression

Open branches in finished tableaux in general correspond to partial models rather than full models. E.g., in the propositional case, it does not matter what truth value one assigns to proposition letters not mentioned along open branches [?]. The same phenomenon presents itself in the case of hybrid logic. In general, an open tableau node of the form (U, A, I, P, N, C, []) for φ can be used to generate a whole range of Kripke models for φ, including minimal models. The following node compression algorithm accomplishes this.

Node Compression Algorithm

Let a finished open constraint tableau node (U, A, I, P, N, C, []) be given.

• If there are no pairs of nominals m, n with m preceding n and m ≉ n ∉ I then return the unit list [(U, A, I, P, N, C, [])].

• Otherwise, nondeterministically pick a pair of nominals m, n with m preceding n and m ≉ n ∉ I.

Compression Step Develop the tableau [(U_{m}^{n}, A_{m}^{n}, I_{m}^{n}, P_{m}^{n}, N_{m}^{n}, [], C_{m}^{n})].

– If this remains open, then compress the finished open nodes and collect the results.

– If it closes, then compress (U, A, (m ≉ n : I), P, N, C, []).

@s◇¬s, @s□ ↓ x.◇(¬s ∧ ¬x), @s□□ ↓ x.@s◇x ; sRt, @t¬s ; t ≉ s ; @t ↓ x.◇(¬s ∧ ¬x) ; @t◇(¬s ∧ ¬t) ; tRt′, t′ ≉ s, t′ ≉ t ; @t□ ↓ x.@s◇x ; @t′ ↓ x.@s◇x ; @t′@s◇t′ ; @s◇t′ ; sRt′ ; @t′ ↓ x.◇(¬s ∧ ¬x) ; @t′◇(¬s ∧ ¬t′) ; t′Rt′′, t′′ ≉ s, t′′ ≉ t′ ; ⋮

Figure 11: Tableau for (??).

@s◇¬s, @s□ ↓ x.◇(¬s ∧ ¬x), @s□□ ↓ x.@s◇x ; \begin{matrix}sRs, @s¬s \\ ⊥ \end{matrix} ; sRt, @t¬s ; t ≉ s ; @t ↓ x.◇(¬s ∧ ¬x) ; \begin{aligned}& @t◇(¬s ∧ ¬t) \\ tRs, @s(¬s ∧ ¬t) ; ⋮ ; ⊥ & tRt, @s(¬s ∧ ¬t) ; ⋮ ; ⊥ & tRt′, t′ ≉ s, t′ ≉ t ; @t□ ↓ x.@s◇x ; @t′ ↓ x.@s◇x ; @t′@s◇t′ ; @s◇t′ ; sRt′ ; @t′ ↓ x.◇(¬s ∧ ¬x) ; @t′◇(¬s ∧ ¬t′) ; t′Rs ; ⋮ ; ⊥  t′Rt′ ; ⋮ ; ⊥  t′Rt ; ⋮ ; open  t′Rt′′ ; ⋮ \end{aligned}

Figure 12: Trial-and-error tableau for (??).

Theorem 10 (Soundness of Node Compression Algorithm) If the node compression algorithm is applied to a finished open tableau node for φ, then all finished open tableau nodes that result from the algorithm satisfy φ.

Proof. Induction on the number of nominal pairs m, n with m preceding n and m ≉ n ∉ I on a finished open tableau node for φ. □

Theorem 11 (Completeness of Node Compression Algorithm) If the node compression algorithm is applied to a finished open tableau node for φ it yields at least one open node

(U, A, I, P, N, C, [])

that corresponds to a minimal model for φ.

Proof. If the algorithm is called with a finite node, termination is ensured, for every step either removes a pair m, n from the list of candidates for merging, or merges the pair. Also, upon termination, there are open nodes, for if (U, A, I, P, N, C, []) is open then

(U, A, (m ≉ n : I), P, N, C, [])

is open. Since the resulting open nodes cannot be compressed any further, at least one of them is minimal. □

To define the notion of a minimal model for a fragment of hybrid logic per se, we can use the notion of a hybrid bisimulation [?, ?], with the obvious extension to take care of the converse modalities. A Kripke model M is minimal for a hybrid language if for all models N, all sequences m̄ ∈ ^{k}M and n̄ ∈ ^{k}N, any hybrid bisimulation (for that language) ∼^{ω} with (M, m̄) ∼^{ω} (N , n̄) and m̄(i) = m̄(j) satisfies n̄(i) = n̄(j). Intuitively, M is minimal for some hybrid logic language if no distinct worlds in M are ever identified by a hybrid bisimulation for that language. We leave the investigation of this notion for a future occasion.

12 Deciding Some Fragments of HL(↓,˘ , @)

It is well known that HL(@) and HL(@,˘ ) are decidable. Theorem ?? states that the constraint proof engine from Section ?? decides hybrid logic formulas without binders.

Theorem 12 The constraint proof engine for HL(@,˘ , ↓) decides satisfiability of HL(@,˘ ) formulas.

Proof. The result follows from a modal depth argument. HL(@,˘ ) has a notion of finite degree ([?], Ch. 7); in particular, modal depth for its formulas can be defined as follows:

d(p) = d(c) = d(x) = 0
d(φ ∗ ψ) = max(d(φ), d(ψ)), ∗ ∈ {∧, ∨, →}
d(¬φ) = d(φ)
d(Mφ) = d(φ) + 1, M ∈ {[ i], ⟨ i ⟩, [ i]^{}˘ , ⟨ i ⟩^{}˘ }
d(@mφ) = d(φ)

Every non-literal formula φ ∉ {[ i], [ i]^{}˘ } gets decomposed by the rule that applies to it. Every formula φ ∈ {[ i], [ i]^{}˘ } generates a constraint. When a constraint @m□φ is combined with an mRn relation, it generates a new formula @nφ on the list of pending formulas, but d(φ) = d(□φ) − 1. Thus, the box formula @m□φ gets replaced by a finite number of @nφ formulas, and each of these is appended to the list of pending formulas, so fairness of the procedure is preserved. □

At first sight, there is something puzzling about the undecidability of HL(@,˘ , ↓), especially since the so-called standard translation given in [?, ?] seems to suggest that hybrid sentences (hybrid formulas without unbound world variables) are in the two-variable bounded fragment of first order logic. In fact, the translation instruction has a flaw, as can be seen when we use it to translate the transitivity sentence ↓ u.□□ ↓ w.@u◇w. Carrying out the instruction starting out from ST_{x}(↓ u.□□ ↓ w.@u◇w), we end up with an injunction to substitute x for u in ∀y(Rxy → ∀x(Ryx → ∃y(Ruy ∧ y = x))), with capture of x by ∀x as a result. The standard translation can be repaired by replacing the instructions for the modalities and the binders as follows:

ST_{x}(⟨ i ⟩φ) := ∃y(R_{i}xy ∧ ST_{y}φ) with y a fresh variable,
ST_{x}(↓ w.φ) := (ST_{y}φ)_{y}^{w} with y a fresh variable.

A fresh variable, of course, is a variable that has not been used before in the translation. This makes clear that the translation does not ensure a bound on the number of variables that are needed. E.g., the translation of the transitivity sentence needs as least three different variables.

We will now demonstrate that it is the presence of ↓ in the scope of box modalities that causes undecidability of HL(@,˘ , ↓). Consider the version of HL(@,˘ , ↓) without [ i], [ i]^{}˘ , → that can be got by paraphrasing d with the help of [ i]φ ↔ ¬⟨ i ⟩¬φ, [ i]^{}φ̆ ↔ ¬⟨ i ⟩^{}˘ ¬φ, and (φ → ψ) ↔ ¬φ∨ψ. A subformula ψ of φ is existential in φ if every ◇ that outscopes ψ in φ is in the scope of an even number of negation operators. Thus, ψ is existential in ◇¬ψ and @m¬(◇m ∧ ¬◇ψ), but not in ¬◇ψ. Call a formula φ innocent if every binder subformula ↓ x.ψ of φ is existential in φ.

Theorem 13 The innocent fragment of HL(@˘, ↓) is decidable.

Proof. Consider the following translation from (located formulas of) HL(@,˘ , ↓) to HL(@,˘ ).

(@mp)^{T} := @mp
(@mn)^{T} := @mn
(@m¬φ)^{T} := ¬(@mφ)^{T}
(@mφ ∧ ψ)^{T} := (@mφ)^{T} ∧ (@mψ)^{T}
(@mφ ∨ ψ)^{T} := (@mφ)^{T} ∨ (@mψ)^{T}
(@m@nφ)^{T} := (@nφ)^{T}
(@m⟨ i ⟩φ)^{T} := @m⟨ i ⟩(n ∧ (@nφ)^{T}), n a fresh nominal
(@m⟨ i ⟩^{}φ̆)^{T} := @m⟨ i ⟩^{}˘ (n ∧ (@nφ)^{T}), n a fresh nominal
(@m ↓ x.φ)^{T} := (@mφ[x := m])^{T}

Check by induction on formula structure that this translation is truth-preserving for all formulas in the innocent fragment. □

Another way of seeing this is by observing that the tableaux for φ and φ^{T} are essentially the same, which leads immediately to:

Theorem 14 The constraint proof engine for HL(@,˘ , ↓) decides the innocent fragment.

Consider the following fragment of existential formulas of HL(@,˘ ):

ψ ::= n | ¬n | ¬⟨ i ⟩n | ¬⟨ i ⟩^{}n̆ | ψ ∧ ψ′ | ψ ∨ ψ′ | ⟨ i ⟩ψ | ⟨ i ⟩^{}ψ̆

Use this to define HL(@,˘ , ↓^{∃}), by changing the definition of binder formulas from ↓ x.φ to ↓ x.ψ. In other words, binding is only allowed over existential formulas. If, moreover, we only allow one binding variable w, we get [?]:

Theorem 15 (M. Marx) The language HL(@,˘ , (↓ w)^{∃}) is decidable in EXPTIME.

Proof. Using a standard translation we can map this language to the universal guarded fragment (where universal quantifiers are guarded, but existential quantifiers need not be) in three variables x, y, w. By a remark in [?], existential guards can be dispensed with, for the sentence (∀x.α)∃yφ(xy), with ∃y unguarded, is satisfiable if and only if the properly guarded sentence (∀x.α)∃yRxy ∧(∀x.Rxy)φ(xy), with R a new relation symbol of the appropriate arity, is satisfiable. Satisfiability of the universal guarded fragment in a bounded number of variables is shown to be decidable in EXPTIME in [?]. □

If we allow an unrestricted number of binding variables x_{1}, … the fragment is still decidable, but since there is no bound now on the number of variables employed in the translation, the complexity is in 2EXPTIME [?].

Theorem 16 The constraint proof engine for HL(@,˘ , ↓) decides satisfiability of HL(@,˘ , ↓^{∃}) formulas.

Proof. Suppose the proof engine is invoked to check satisfiability of φ. We only need to be concerned about formulas of the forms [ i] ↓ x.ψ, ⟨ i ⟩¬ ↓ x.ψ, [ i]^{}˘ ↓ x.ψ ⟨ i ⟩^{}˘ ¬ ↓ x.ψ that turn up along a tableau branch during the processing of φ, for these are the formulas that cause binders to appear in the [ i] and [ i]^{}˘ constraints. Suppose @m□ ↓ x.ψ is in the box constraint store, and gets combined with an mRn accessibility along the branch. Then @n ↓ x.ψ will get appended to the pending formula list. When @n ↓ x.ψ gets decomposed, it gets replaced by ψ_{n}^{x}, and further decomposition will not affect the constraint stores because ψ is existential. □

13 Related Work

Comparison with other tableau systems Tableau calculi for hybrid logic are still in their infancy. A prefixed tableau calculus along the lines of the prefixed tableau style theorem proving of [?] is given in [?]. This does not yet make full use of the possibility to let the role of prefixes be played by nominals. In [?] it is pointed out that nominals can play the role of labels in labelled deduction style theorem proving, and a tableau calculus is proposed that handles equality reasoning on nominals by means of rewrite rules that express reflexivity, symmetry and transitivity of equality, and that allows substitution of equal nominals. However, since this rewrite system is not normalizing, equality reasoning in the resulting calculus is awkward, and proof engines based on it will spend too much effort on pointless rewrite steps for equality [?].

Comparison with resolution for hybrid logic The resolution approach to modal logic dates back to at least [?, ?]. A prefixed resolution calculus for description and hybrid logic was proposed in [?], and implemented in [?]. Detailed efficiency comparison with this is future work.

Acknowledgement Many thanks to the Dynamo team (Wim Berkelmans, Balder ten Cate, Juan Heguiabehere, Breanndán Ó Nualláin) and to Carlos Areces, Patrick Blackburn and Maarten Marx, for useful comments and fruitful discussion.