hylotab-1.2.0: cthl.tex
\documentclass[oribibl]{llncs}
\usepackage{url}
\usepackage{latexsym,amssymb,amsmath,theorem,proof,calc,alltt}
%\usepackage{parsetree}
%\usepackage{tree-dvips}
\usepackage{pst-tree}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% VERSION FEB 2002 %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\input{mymacros}
\newcommand{\commentout}[1]{}
\newcommand{\close}[1]{\begin{array}{c}{#1} \\ {\times} \end{array}}
\newcommand{\clsubs}[2]{\begin{array}{c}{#1} \\ {#2} \end{array}}
\newcommand{\stack}[1]{\begin{array}{c}{#1} \end{array}}
\newcommand{\barr}{\begin{array}{c}}
\newcommand{\earr}{\end{array}}
\newcommand{\EQ}{\approx}
\newcommand{\NEQ}{\not\approx}
\newcommand{\var}{{\rm var\:}}
%\newcommand{\dom}{{\rm dom\:}}
%\newcommand{\rng}{{\rm rng\:}}
\newcommand{\bB}{\mbox{\boldmath $B$}}
\newcommand{\ttop}{\mbox{\boldmath $\top\!\!\!\!\top$}}
\newcommand{\bbot}{\mbox{\boldmath $\bot\!\!\!\!\bot$}}
\newcommand{\bT}{\mbox{\boldmath $T$}}
\newcommand{\cB}{\mbox{$\cal B$}}
\newcommand{\cE}{{\cal E}}
\newcommand{\href}[1]{}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Exists}{\boldsymbol{\exists\!\!\!\exists}}
\newcommand{\Forall}{\boldsymbol{\forall\!\!\!\forall}}
\newcommand{\Neg}{\boldsymbol{\neg\!\!\!\neg}}
\newcommand{\SC}{\ \boldsymbol{;}\ }
\newsavebox{\fminibox}
\newlength{\fminilength}
\newenvironment{fminipage}[1][\linewidth]
{\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}%
\bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip}
{\smallskip\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}\bigskip}
\newcommand{\bc}{\begin{fminipage}}
\newcommand{\ec}{\end{fminipage}}
\newenvironment{code}{\begin{fminipage}\begin{alltt}}%
{\end{alltt}\end{fminipage}}
\newenvironment{pcode}{\begin{fminipage}\begin{alltt}}%
{\end{alltt}\end{fminipage}
}
\newcommand{\impl}{\Rightarrow}
\newcommand{\M}{{\cal M}}
\newcommand{\N}{{\cal N}}
\newcommand{\forces}{\mbox{\ $\vdash\!\!\!\vdash$\ }}
\newcommand{\sref}[1]{(\ref{#1})}
\newcommand{\bfx}{\mbox{\bf x}}
\newcommand{\bfy}{\mbox{\bf y}}
\newcommand{\bfz}{\mbox{\bf z}}
\newcommand{\produces}{\longrightarrow}
\newcommand{\yields}{\Rightarrow}
\setlength{\textheight}{22cm}
\setlength{\textwidth}{16cm}
\setlength{\topmargin}{0cm}
\setlength{\oddsidemargin}{0cm}
\setlength{\evensidemargin}{0cm}
\setlength{\parindent}{0 ex}
\setlength{\parskip}{1.5 ex}
\newcommand{\Ibox}[1]{[{\scriptstyle\:#1\: }]}
\newcommand{\Idia}[1]{\langle{\scriptstyle\: #1\: }\rangle}
\newcommand{\Icbox}[1]{[{\scriptstyle\: #1\:}]^{\:\breve{}}}
\newcommand{\Icdia}[1]{\langle{\scriptstyle\: #1\: }\rangle^{\breve{}}}
\newcommand{\Cbox}{\Box^{\:\breve{}}}
\newcommand{\Cdia}{\Diamond^{\breve{}}}
\title{Constraint Tableaux for Hybrid Logics}
\author{Jan van Eijck}
\institute{CWI and ILLC, Amsterdam, Uil-OTS, Utrecht;
\email{jve@cwi.nl}}
\begin{document}
\maketitle
\begin{abstract} \noindent
Hybrid logics are modal logics with names for worlds. 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 formula in the first order
correspondence language of hybrid logic. We propose a sound and
complete calculus for minimal model generation; this is useful
for processing formulas without fixed depth.
% , 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, {\em HyLoTab}, has been implemented. A companion paper
\cite{Eijck02:hylotab} contains the full code of of this
implementation in Haskell \cite{Haskell98:rep}, in `literate
programming' style \cite{Knuth:lp}. This documented code can be
found at \url{http://www.cwi.nl/~jve/hylotab}.
\end{abstract}
\paragraph{Keywords:} Hybrid logic, tableau reasoning,
equality reasoning, model generation, decision methods.
\paragraph{MSC codes:} 03B10, 03F03, 68N17, 68T15
\section{Hybrid Logic: Syntax and Semantics}
Our starting point is ${\cal HL}(@,\breve{},\downarrow)$, a hybrid
logic language
\cite{Areces:le,AreBlaMar:hlcic} with the following syntax. Assume
$p$ ranges over a set of propositions $\{ p_0, p_1, \ldots \}$,
$c$ over a set of constant nominals $\{ c_0, c_1,\ldots \}$,
$x$ over a set of variable nominals $\{ x_0, x_1, \ldots \}$,
$n$ over the sets of constant nominals and variable nominals,
and $i$ over a set of relation indices $\{ i_0, i_1 , \ldots \}$.
Then ${\cal HL}(@,\breve{},\downarrow)$ is given by:
\begin{eqnarray*}
\phi & ::= & \top \mid \bot \mid p
\mid c \mid x \mid \neg \phi
\mid \phi \land \phi'
\mid \phi \lor \phi'
\mid \phi \rightarrow \phi'
\mid \Ibox{i} \phi
\mid \Icbox{i} \phi
\mid \Idia{i} \phi
\mid \Icdia{i} \phi
\mid @ n \phi
\mid \downarrow\! x. \phi.
\end{eqnarray*}
${\cal HL}(@,\breve{})$ is the hybrid language that results from
leaving out the binders $\downarrow\! x. \phi$ from ${\cal
HL}(@,\breve{},\downarrow)$, and ${\cal HL}(@)$ is the hybrid language
that results from leaving out the converse modalities $\Icbox{i}\phi$
and $\Icdia{i} \phi$ from ${\cal HL}(@,\breve{})$.
Models for ${\cal HL}(@,\breve{},\downarrow)$ consist of a set of
woirld $W$, a set $R = \{ R_i \mid i \in 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 ${\cal HL}(@,\breve{},\downarrow)$
are given by:
\begin{eqnarray*}
\M, g, w \forces p & \text{ iff } & w \in V(p) \\
\M, g, w \forces c & \text{ iff } & \{ w \} = V(c) \\
\M, g, w \forces x & \text{ iff } & w = g(x) \\
\M, g, w \forces \Ibox{i} \phi & \text{ iff } & \text{ for all }w'
\text{ with } wR_iw' \text{ it holds that } \M, g, w' \forces \phi \\
\M, g, w \forces \Idia{i} \phi & \text{ iff } &
\text{ for some }w' \text{ with } wR_iw' \text{ it holds that }
\M, g, w' \forces \phi \\
\M, g, w \forces \Icbox{i} \phi & \text{ iff } & \text{ for all }w'
\text{ with } w'R_iw \text{ it holds that } \M, g, w' \forces \phi \\
\M, g, w \forces \Icdia{i} \phi & \text{ iff } &
\text{ for some }w' \text{ with } w'R_iw \text{ it holds that }
\M, g, w' \forces \phi \\
\M, g, w \forces @ n \phi & \text{ iff } & \M, g, w' \forces \phi
\text{ where } \{ w' \} = V(n) \\
\M, g, w \forces \downarrow\! x. \phi & \text{ iff } &
\M, g^x_w, w \forces \phi.
\end{eqnarray*}
Here $g^x_w$ is like $g$, except possibly for the
fact that it maps $x$ to $w$.
\section{A Tableau Calculus for ${\cal HL}(@,\breve{},\downarrow)$}
The tableau rules for ${\cal HL}(@, \breve{},\downarrow)$ work on
the labelled version of this language, with inequalities and access
statements added. The tableau rules use the following language ($\phi
\in {\cal HL}(@,\breve{},\downarrow)$):
\begin{eqnarray*}
\psi & ::= & m \NEQ n \mid mRn \mid @ n \phi.
\end{eqnarray*}
We assume a linear ordering $<$ on the set of nominals. An
inequality $m \NEQ n$ generated by the tableau rules will
always satisfy $m \leq n$. Inequalities $m \NEQ m$ are written
as $\bot$. As in \cite{Blackburn:ild,Blackburn:rrars},
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 $\Ibox{i}$ and $\Icbox{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 $\gamma$ tableau rules in first order
logic \cite{Smullyan:fl}. In the proof procedure based on the calculus they
are translated into constraints (see Section \ref{PP}).
\paragraph{Conjunctive rules ($\alpha$ rules)}
\[
\text{}\cfrac{@m (\phi \land \psi)}{
\begin{array}{c}@m \phi \\
@m \psi
\end{array}}
\hspace*{3em}
\text{}\cfrac{@m \neg (\phi \lor \psi)}{
\begin{array}{c}@m \neg \phi \\
@m \neg \psi
\end{array}}
\hspace*{3em}
\text{}\cfrac{@m \neg (\phi \rightarrow \psi)}{
\begin{array}{c}@m \phi \\
@m \neg \psi
\end{array}}
\]
\paragraph{Disjunctive rules ($\beta$ rules)}
\[
\text{}\cfrac{@m (\phi \lor \psi)}{
@m \phi \ \mid \ @m \psi}
\hspace*{3em}
\text{}\cfrac{@m \neg (\phi \land \psi)}{
@m \neg \phi \ \mid \ @m \neg \psi}
\hspace*{3em}
\text{}\cfrac{@m (\phi \rightarrow \psi)}{
@m \neg \phi \ \mid \ @m \psi}
\]
\paragraph{Negation rule} As this is a single-sided calculus, the only
negation rule we need is the rule for double negation.
\[
\cfrac{@m \neg \neg \phi}{
@m \phi}
\]
\paragraph{$\Ibox{i}$ rules} Like the $\gamma$ rules in FOL tableaux, these
are `standing orders'.
\[
\cfrac{@m \Ibox{i} \phi, mR_in}{
@n \phi}
\hspace*{3em}
\cfrac{@m \neg \Idia{i}\phi, mR_in}{
@n \neg \phi}
\]
\paragraph{$\Idia{i}$ rules}
\[
\cfrac{@n \Idia{i} \phi}{
\begin{array}{c} nR_im \\
@m \phi
\end{array}}\text{ $\phi$ not a nominal, $m$ fresh}
\hspace*{3em}
\cfrac{@n \neg \Ibox{i} \phi}{
\begin{array}{c} nR_im \\
@ m \neg \phi
\end{array}}\text{ $\phi$ not a negated nominal, $m$ fresh}
\]
\paragraph{$\Icbox{i}$ rules}
Like the $\gamma$ rules in FOL tableaux, these are `standing orders'.
\[
\cfrac{@m \Icbox{i} \phi, nR_im}{
@n \phi}
\hspace*{3em}
\cfrac{@m \neg \Icdia{i} \phi, nR_im}{
@n \neg \phi}
\]
\paragraph{$\Icdia{i}$ rules}
\[
\cfrac{@n \Icdia{i} \phi}{
\begin{array}{c} mR_in \\
@m \phi
\end{array}}\text{ $\phi$ not a nominal, $m$ fresh}
\hspace*{3em}
\cfrac{@n \neg \Icbox{i} \phi}{
\begin{array}{c} mR_in \\
@ m \neg \phi
\end{array}}\text{ $\phi$ not a negated nominal, $m$ fresh}
\]
\paragraph{Access rules} Formulas of the forms $\Idia{i} n$,
$\neg \Ibox{i} \neg n$, $\Icdia{i} n$, $\neg \Icbox{i} \neg n$,
are called access formulas. They are treated by a separate rule.
\[
\cfrac{@n \Idia{i} m}{nR_im}
\hspace*{3em}
\cfrac{@n \neg \Ibox{i} \neg m}{nR_im}
\hspace*{3em}
\cfrac{@n \Icdia{i} m}{mR_in}
\hspace*{3em}
\cfrac{@n \neg \Icbox{i} \neg m}{mR_in}
\]
\paragraph{Label rules}
\[
\text{}\cfrac{@m @n \phi}{
@n \phi}
\hspace*{3em}
\text{}\cfrac{@m \neg @ n \phi}{
@ n \neg \phi}
\]
\paragraph{Nominal substitution}
Here comes the new element, a substitution rule that makes use of the
fact that nominals are unique names. $\bB^t_s$ is the result of
substituting $s$ for $t$ everywhere in tableau branch $\bB$. The rules
make use of the linear order $<$ on nominals.
\[
\cfrac{\bB + @m m}{\bB}
\hspace*{3em}
\cfrac{\bB + @m n}{\bB^t_s} s = \min(m,n), t = \max(m,n)
\]
\paragraph{Inequality generation}
Write $\bot$ for $m \NEQ m$.
\[
\cfrac{@m \neg m}{\bot}
\hspace*{3em}
\cfrac{@m \neg n}{s \NEQ t} \ s = \min(m,n), t = \max(m,n)
\]
\[
\cfrac{@m \phi, @m \neg \phi}{\bot}
\hspace*{3em}
\cfrac{@m \phi, @n \neg \phi}{s \NEQ t} \ s = \min(m,n), t = \max(m,n)
\]
The rule that derives an inequality constraint from $@m \phi, @n \neg
\phi$ 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.
\paragraph{Binding rules}
\[
\cfrac{@m \downarrow\! x. \phi}{@m \phi^x_m}
\hspace*{3em}
\cfrac{@m \neg \downarrow\! x. \phi}{@m \neg \phi^x_m}
\]
Here $\phi^x_m$ denotes the result of substituting $m$ for all
{\em free}\/ occurrences of $x$ in $\phi$.
\paragraph{Tableau Closure}
A tableau branch is closed if it contains $\bot$. A tableau is closed
if all its branches are closed. Note that {\bf nominal substitution}\/ can
lead to branch closure.
\section{Examples of Refutation Proofs, for ${\cal HL} (@)$}
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{@m (\Diamond (i \land p) \land \Diamond (i \land q) \land
\Box (\neg p \lor \neg q))}}{
\pstree{\Tr{@m \Diamond (i \land p),
@m \Diamond (i \land q),
@m \Box(\neg p \lor \neg q)}}{
\pstree{\Tr{mRn, @n (i \land p),
@m \Diamond (i \land q),
@m \Box(\neg p \lor \neg q)
}}{
\pstree{\Tr{mRn, @n i, @n p,
@m \Diamond (i \land q),
@m \Box(\neg p \lor \neg q)
}}{
\pstree{\Tr{mRi, @i p,
@m \Diamond (i \land q),
@m \Box(\neg p \lor \neg q)
}}{
\pstree{\Tr{mRi, @i p,
mRk, @k(i \land q),
@m \Box(\neg p \lor \neg q)
}}{
\pstree{\Tr{mRi, @i p,
mRk, @ki, @ k q,
@m \Box(\neg p \lor \neg q)
}}{
\pstree{\Tr{mRi, @i p,
@i q,
@m \Box(\neg p \lor \neg q)
}}{
\pstree{\Tr{mRi, @i p,
@i q,
@m \Box(\neg p \lor \neg q),
@i (\neg p \lor \neg q)
}}{
\pstree{\Tr{
\begin{array}{l}
mRi, @i p, @i q, \\
@m \Box(\neg p \lor \neg q),
@i \neg p
\end{array}
}}{\Tr{\bot}}
\pstree{\Tr{\begin{array}{l}
mRi, @i p, @i q, \\
@m \Box(\neg p \lor \neg q),
@i \neg q
\end{array}
}}{\Tr{\bot}}
}
}
}
}
}
}
}
}
}
$
\end{center}
\caption{Tableau refutation for (\ref{Ex1}).}
\label{FigEx1}
\end{figure}
\commentout{
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{@m (\Diamond (i \land p) \land \Diamond (i \land q) \land
\Box (\neg p \lor \neg q))}}{
\pstree{\Tr{@m \Diamond (i \land p),
@m \Diamond (i \land q),
@m \Box(\neg p \lor \neg q)}}{
\pstree{\Tr{mRn, @n (i \land p)
}}{
\pstree{\Tr{@n i, @n p
}}{
\pstree{\Tr{n \mapsto i
}}{
\pstree{\Tr{mRk, @k(i \land q)
}}{
\pstree{\Tr{@ki, @ k q
}}{
\pstree{\Tr{k \mapsto i
}}{
\pstree{\Tr{@i (\neg p \lor \neg q)
}}{
\pstree{\Tr{
@i \neg p
}}{\Tr{\bot}}
\pstree{\Tr{
@i \neg q
}}{\Tr{\bot}}
}
}
}
}
}
}
}
}
}
$
\end{center}
\caption{Tableau refutation for (\ref{Ex1}), without formula repetition.}
\label{FigEx1a}
\end{figure}
}
Figure \ref{FigEx1} gives a tableau refutation of \sref{Ex1}, with the
active formulas of the branch repeated at each node.
\commentout{
Figure
\ref{FigEx1} gives another version of this, without repetition of
formulas, but with the substitution instructions indicated along the
branch.
}
\begin{equation} \label{Ex1}
@m (\Diamond (i \land p) \land \Diamond (i \land q) \land
\Box (\neg p \lor \neg q)).
\end{equation}
The tableau refutation of \sref{Ex1} proves the validity of
$\Diamond (i \land p) \land \Diamond (i \land q)
\rightarrow \Diamond (p \land 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\land q$
world is accessible.
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{@m \neg ((\Diamond p \land \Diamond \neg p)
\rightarrow (\Box (q \rightarrow i) \rightarrow \Diamond \neg q))}}{
\pstree{\Tr{
@m (\Diamond p \land \Diamond \neg p),
@m \neg (\Box (q \rightarrow i) \rightarrow \Diamond \neg q)}}{
\pstree{\Tr{
@m \Diamond p, @m \Diamond \neg p,
}}{
\pstree{\Tr{
@m \Box (q \rightarrow i), @m \neg \Diamond \neg q
}}{
\pstree{\Tr{
mRn, @n p
}}{
\pstree{\Tr{
mRk, @k \neg p
}}{
\pstree{\Tr{
@n (q \rightarrow i), @n q
}}{
\pstree{\Tr{
@k (q \rightarrow i), @k q
}}{
\pstree{\Tr{
@n \neg q
}}{\Tr{\bot}}
\pstree{\Tr{
@n i
}}{
\pstree{\Tr{n \mapsto i
}}{
\pstree{\Tr{@k \neg q}}{\Tr{\bot}}
\pstree{\Tr{@k i}}{
\pstree{\Tr{k \mapsto i }}{\Tr{\bot}}
}
}
}
}
}
}
}
}
}
}
}
$
\end{center}
\caption{Tableau refutation for
$@m \neg ((\Diamond p \land \Diamond \neg p)
\rightarrow (\Box (q \rightarrow i) \rightarrow \Diamond \neg q))$
.}
%(\ref{Ex2}).}
\label{FigEx2}
\end{figure}
Figure \ref{FigEx2} gives a tableau refutation of $@m \neg ((\Diamond
p \land \Diamond \neg p) \rightarrow (\Box (q \rightarrow i)
\rightarrow \Diamond \neg q))$, without repetition of
formulas, but with the substitution instructions indicated along the
branch. The nominal substitutions $n \mapsto
i$ and $k \mapsto i$ act on the formulas $@ n p$ and $@ k \neg p$ to
give $@ i p, @ i \neg p$ on the branch, and therefore branch
closure. The tableau refutation proves the validity of $((\Diamond p
\land \Diamond \neg p) \rightarrow (\Box (q \rightarrow i) \rightarrow
\Diamond \neg 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
$\neg q$ world.
\commentout{
\section{Examples of Model Generation, for ${\cal HL} (@)$}
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{
@m (\Diamond \Diamond m \land \neg \Diamond m)
}}{
\pstree{\Tr{
@m \Diamond \Diamond m, @m \neg \Diamond m
}}{
\pstree{\Tr{
mRn, @n \Diamond m
}}{
\pstree{\Tr{
@n \neg m
}}{
\pstree{\Tr{
n \NEQ m
}}{
\pstree{\Tr{
nRk, @k m
}}{
\pstree{\Tr{
m \mapsto k
}}{
}
}
}
}
}
}
}
$
\end{center}
\caption{Open tableau for
$@m (\Diamond \Diamond m \land \neg \Diamond m)$.}
\label{FigRef1}
\end{figure}
Figure \ref{FigRef1} gives an open tableau for
$@m (\Diamond \Diamond m \land \neg \Diamond m)$.
Since the formula contains no proposition letters, it defines a
frame property. The smallest frame with the property is $\bullet
\leftrightarrow \bullet$.
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{
@m (\Diamond i \land \Diamond j \land \Diamond k
\land @ i \neg j \land @ j \neg k \land @ i \neg k)
}}{
\pstree{\Tr{
@m \Diamond i,
@m \Diamond j,
@m \Diamond k,
@m @ i \neg j,
@m @ j \neg k,
@m @ i \neg k
}}{
\pstree{\Tr{
mRi, mRj, mRk
}}{
\pstree{\Tr{
@i \neg j, @j \neg k, @i \neg k
}}{
\pstree{\Tr{
i \NEQ j, j \NEQ k, i \NEQ k
}}{
}
}
}
}
}
$
\end{center}
\caption{Open tableau for
$ @m (\Diamond i \land \Diamond j \land \Diamond k
\land @ i \neg j \land @ j \neg k \land @ i \neg k)$.}
%(\ref{Ref2}).}
\label{FigRef2}
\end{figure}
Figure \ref{FigRef2} gives an open tableau for
$ @m (\Diamond i \land \Diamond j \land \Diamond k
\land @ i \neg j \land @ j \neg k \land @ i \neg k)$.
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{@m \Diamond (c \land \Diamond c \land \Box \Diamond c)}}{
\pstree{\Tr{mRn, @n (c \land \Diamond c \land \Box \Diamond c)}}{
\pstree{\Tr{@n c, @ n \Diamond c, @ n \Box \Diamond c
}}{
\pstree{\Tr{n \mapsto c
}}{
\pstree{\Tr{cRc, @c \Box \Diamond c
}}{
\pstree{\Tr{@ c \Diamond c
}}{
\Tr{cRc}}
}
}
}
}
}
$
\end{center}
\caption{Open tableau for $\Diamond (c \land
\Diamond c \land \Box \Diamond c)$.}
\label{FigNewEx}
\end{figure}
Figure \ref{FigNewEx} shows that the formula $\Diamond (c \land
\Diamond c \land \Box \Diamond c)$ is satisfiable. Note that this
formula causes the first of the two tableau proof procedures in
\cite{Tzakova:tcfhl} to loop.
\section{Examples of the treatment of $\downarrow$}
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{
@m(\downarrow x. \Box \Diamond x
\land \neg (\Diamond \Box p \rightarrow p))
}}{
\pstree{\Tr{
@m \downarrow x. \Box \Diamond x,
@m \neg (\Diamond \Box p \rightarrow p)
}}{
\pstree{\Tr{
@m \Box \Diamond m
}}{
\pstree{\Tr{
@m \Diamond \Box p, @m \neg p
}}{
\pstree{\Tr{
mRn, @n \Box p
}}{
\pstree{\Tr{
@n \Diamond m
}}{
\pstree{\Tr{
nRm
}}{
\pstree{\Tr{
@m p
}}{\Tr{\bot}}
}
}
}
}
}
}
}
$
\end{center}
\caption{Closed tableau for $@m \ \downarrow x . \Box \Diamond x \land
\neg (\Diamond \Box p \rightarrow p)$.}
\label{FigArrowEx1}
\end{figure}
Figure \ref{FigArrowEx1} gives a closed tableau for
$@m \ \downarrow x . \Box \Diamond x \land
\neg (\Diamond \Box p \rightarrow p)$.
The formula $\downarrow x . \Box \Diamond x$ holds at the point $m$ if
$mRn$ implies $nRm$. The formula $\Diamond \Box p \rightarrow p$ is
true at points where $R$ is symmetric. Therefore, $\downarrow x . \Box
\Diamond x \rightarrow (\Diamond \Box p \rightarrow p)$ is valid.
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{
@s (\Diamond \top \land \Box \Box \downarrow x. @ s \Diamond x
\land \Box (\Diamond \top \land \phi))
}}{
\pstree{\Tr{
@s \Diamond \top,
@s \Box \Box \downarrow x. @ s \Diamond x,
@s \Box (\Diamond \top \land \phi)
}}{
\pstree{\Tr{
sRt
}}{
\pstree{\Tr{
@t \Diamond \top, @ t \phi
}}{
\pstree{\Tr{
tRt'
}}{
\pstree{\Tr{
@t \Box \downarrow x. @ s \Diamond x
}}{
\pstree{\Tr{
@t' \downarrow x. @ s \Diamond x
}}{
\pstree{\Tr{
@t' @ s \Diamond t'
}}{
\pstree{\Tr{
@ s \Diamond t'
}}{
\pstree{\Tr{
sRt'
}}{
\pstree{\Tr{
@t' \Diamond \top, @ t' \phi
}}{
\pstree{\Tr{
t'Rt''
}}{\Tr{\vdots}}
}
}
}
}
}
}
}
}
}
}
}
$
\end{center}
\caption{Infinite tableau for (\ref{ArrowEx2}).}
\label{FigArrowEx2}
\end{figure}
}
In ${\cal HL}(\downarrow, @)$ it is easy to describe situations that
only have infinite models. See \sref{ArrowEx2}
%Figure \ref{FigArrowEx2} gives an infinite
%tableau for \sref{ArrowEx2}.
\begin{equation} \label{ArrowEx2}
@s (\Diamond \top \land \Box \Box \downarrow x. @ s \Diamond x
\land \Box (\Diamond \top \land \phi)),
\end{equation}
where $\phi$ is the formula
\[
\downarrow x . \Box \neg x \land \downarrow x. \Box \Box \neg x
\land
\downarrow x . \Box \Box \downarrow y . @ x \Diamond y.
\]
The formula $\downarrow x . \Box \neg x$ expresses irreflexivity, the
formula $\downarrow x . \Box \Box \neg x$ asymmetry, the formula
$\downarrow x . \Box \Box \downarrow y . @ x \Diamond y$
transitivity. Formula \sref{ArrowEx2} expresses that from the spypoint
$s$ a serial, irreflexive, asymmetric and transitive, hence infinite,
relation is visible.
\section{From Tableau Calculus to Proof Engine}
\label{PP}
\begin{figure}[htbp] \small
\bc
\[
\cfrac{\text{start } \phi}{[m],[],[],[],[],[],[@ m \phi]}\ m \text{ fresh
}
\]
\[
\cfrac{U,A,I,P,N,C,F}
{\text{closure}}
\ \bot \in I \lor P \cap N \neq
\emptyset \hspace{3em}
\cfrac{U,A,I,P,N,C,[]}
{\text{success}}
\ \bot \notin I, P \cap N = \emptyset
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{U,A,I,P,N,C,[@m \phi_1, \ldots, @m \phi_n] +\!\!+ F}\ \phi \in
\alpha
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{U,A,I,P,N,C,(@m \phi_1:F)\ \mid \ \ \cdots \ \ \mid \
U,A,I,P,N,C,(@m \phi_n:F)}\ \phi \in \beta
\]
\[
\cfrac{U,A,I,P,N,C,(@m \neg \neg \phi:F)}
{U,A,I,P,N,C,(@m \phi:F)}
\]
\[
\cfrac{U,A,I,P,N,C,(@m p:F)}
{U,A,I,(@m p:P),N,C,F} \hspace{3em}
\cfrac{U,A,I,P,N,C,(@m \neg p:F)}
{U,A,I,P,(@ n p:N),C,F}
\]
\[
\cfrac{U,A,I,P,N,C,(@m n:F)}
{U^t_s,A^t_s,I^t_s,P^t_s,N^t_s,C^t_s,F^t_s +\!\!+ F'}
\ s = \min(m,n), t = \max(m,n), F' = \text{ stuff to restore invariant }
\]
\[
\cfrac{U,A,I,P,N,C,(@m \neg n:F)}
{U,A,(s\NEQ t:I),P,N,C,F}
\ s = \min(m,n), t = \max(m,n)
\]
\[
\cfrac{U,A,I,P,N,C,(@m @n \phi:F)}
{U,A,I,P,N,C,(@n \phi:F)} \hspace{3em}
\cfrac{U,A,I,P,N,C,(@m \neg @n \phi:F)}
{U,A,I,P,N,C,(@n \neg \phi:F)}
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{U,A,I,P,N,(@m \phi:C),F +\!\!+\, [@ n
\phi' \mid mR_in \in A]} \ \phi \in \Ibox{i}
\]
\[
\cfrac{U,A,I,P,N,C,(@m \Idia{i} n:F)}
{U,(mR_in:A),I,P,N,C, F +
+\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C]
+\!\!+\, [@ m \psi \mid @ n \Icbox{i} \psi \in C]}
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{(n:U),(mR_in:A),I,P,N,C,(@ n \phi':F)
+\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C]}
\ \phi \in \Idia{i}, n \text{ fresh }
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{U,A,I,P,N,(@m \phi:C), F
+\!\!+\, [@ n \phi' \mid nR_im \in A]}
\ \phi \in \Icbox{i}
\]
\[
\cfrac{U,A,I,P,N,C,(@m \Icdia{i} n:F)}
{U, (nR_im:A),I,P,N,C, F +\!\!+\, [@
m \psi \mid @ n \Ibox{i} \psi \in C] F +\!\!+\, [@ n \psi \mid @ m
\Icbox{i} \psi \in C]}
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{(n:U),(nR_im:A),I,P,N,C,(@ n \phi':F)
+\!\!+\, [@ n \psi \mid @ m \Icbox{i} \psi \in C]}
\ \phi \in \Icdia{i}, n \text{ fresh }
\]
\[
\cfrac{U,A,I,P,N,C,(@m \downarrow x.\phi:F)} {U,A,I,P,N,C,(@m
\phi^x_m:F)} \hspace{3em} \cfrac{U,A,I,P,N,C,(@m \neg \downarrow
x.\phi:F)} {U,A,I,P,N,C,(@m \neg \phi^x_m:F)}
\]
\ec
\caption{Constraint Proof Engine for
${\cal HL}(@,\breve{},\downarrow)$.}
\label{PPfig}
\end{figure}
A proof procedure (or proof engine) for $\phi$ is a systematic search
for a Kripke model satisfying $\phi$, by means of a search tree
starting out from a node {\em start $\phi$}. Our proof engine for
hybrid logic based on the calculus given above is presented in Figure
\ref{PPfig}. 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 $\phi:F$ for the list with head $\phi$ and tail
$F$, and $F_1 +\!\!+ F_2$ for the result of concatenating lists $F_1,
F_2$. Write $[]$ for the empty list, $[\phi]$ for the unit list with
$\phi$ as its element, and $[\phi_1,
\ldots \phi_n]$ for the list consisting of $\phi_1$ through $\phi_n$.
We will assume throughout that the lists do not contain duplicates,
i.e., that the lists behave as ordered sets. In particular, $U^s_t$
means that $s$ gets replaced by $t$ in $U$, and the duplicate of
$t$ that this may generate is removed.
The table uses abbreviations $\phi \in \alpha, \phi \in \beta, \phi
\in \Ibox{i}, \phi \in \Idia{i}, \phi \in \Icbox{i}, \phi \in \Icdia{i}$
for ``$\phi$ is an $\alpha$ formula'',
and so on. We do not count $\Idia{i} n$ or $\Icdia{i} n$
or $\neg \Ibox{i} \neg n$ or $\neg \Icbox{i} \neg n$
as $\Idia{i}$ or $\Icdia{i}$ formulas, as these `access
formulas' are treated by a separate rule. If $\phi \in \alpha \cup
\beta$, the components of $\phi$ are referred to as $\phi_1, \ldots,
\phi_n$. If $\phi \in \Ibox{i} \cup \Idia{i}\cup \Icbox{i}
\cup \Icdia{i}$, its component is referred to as $\phi'$.
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 violated 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:
\begin{itemize}
\item If the substitution results in new access relations, these
get combined with all box and converse box constraints of the node.
\item If the substitution results in new box constraints, these get
combined with all access relations of the node.
\item If the substitution results in new converse box constraints, these
get combined with all access relations of the node.
\end{itemize}
In the substitution rule in the table, this procedure is abbreviated
as `add stuff to restore the invariant'.
\paragraph{Closure, Success}
A node $(U,A,I,P,N,C,F)$ is closed if either $\bot \in I$ or $P \cap N
\neq \emptyset$, 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 {\em incomplete}\/ if
it is neither closed nor a success node.
\paragraph{Selection Rule}
To develop an incomplete node, use the table from Figure
\ref{PPfig}. Since an incomplete node contains a non-empty list of
pending formulas, and the table has exactly one rule that applies to
the head $\phi$ of the pending formula list, this specifies the {\em
selection rule}\/ of the proof engine.
\paragraph{Search Rule}
To select an incomplete leaf node to develop, use any breadth first
search method for tree traversal. This specifies a {\em search rule}\/
for the proof engine.
\paragraph{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 {\em true}\/ when a success node is encountered, and outputs
{\em false}\/ if the proof procedure ends with closed nodes at all
leaves. For refutation, the refutation procedure outputs {\em false}\/
when a success node is encountered, and outputs {\em true}\/ if the
proof procedure ends with closed nodes at all leaves.
\section{Soundness, Fairness of Proof Engine, Completeness}
\begin{theorem}
The tableau calculus for ${\cal HL}(@,\breve{},\downarrow)$ is
sound.
\end{theorem}
\begin{proof}
By an easy inspection, all tableau rules are sound. Soundness of the
calculus follows from this by induction on tableau structure.
\end{proof}
For completeness, we need a fair proof procedure $P$. Consider the
(possibly infinite) set of tableaux for formula $\phi$, 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 $\bT$ is tableau $\bT'$ computed from $\bT$ according to
$P$. Let $\bT_0$ be the initial tableau for $\phi$. Then there is
a possibly infinite ascending chain $\bT_0, \ldots$ of tableaux
for $\phi$. By Zorn's lemma, this chain has a supremum $\bT_\infty$.
A proof procedure for hybrid logic is fair if the following hold for
all open branches $\bB$ in $\bT_\infty$:
\begin{enumerate}
\item All atomic formulas of the form $@m n$ on $\bB$ were used
were used to perform a substitution on $\bB$.
\item All non-atomic formulas of types other than
$\Ibox{i}$ or $\Icbox{i}$ on $\bB$ were used to expand $\bB$.
\item All formulas of type $\Ibox{i}$ or $\Icbox{i}$ on $\bB$ were
combined with all $mR_in$ accessibilities on $\bB$ to expand
$\bB$.
\end{enumerate}
\begin{theorem} \label{PPfair}
The Constraint Proof Engine of Section \ref{PP} is fair.
\end{theorem}
\begin{proof}
Inspection of the table in Figure \ref{PPfig} 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 set at each node $N$ consists of exactly the $\Ibox{i} \cup
\Icbox{i}$ formulas at the node that were used to expand all
appropriate $mR_in$ accessibilities introduced on the path along $\bB$
from the root up to $N$. Finally, note that formulas resulting from
combining an accessibility relation $mR_in$ and a constraint $@ m
\Ibox{i} \phi$ or $@ n \Icbox{i}\phi$ are appended to the list of
pending formulas, thus ensuring that every formula on the pending
formula list will eventually get treated.
\end{proof}
Call a tableau {\em finished}\/ if it does not contain incomplete end
nodes. It is easy to see that each limit tableau $\bT_\infty$ is
finished. Every open branch of a finished tableau for $\phi$ yields a
Kripke model for $\phi$: take the nominals as worlds, put $m
\stackrel{i}{\longrightarrow} n$ if a $mR_in$ relation
occurs along the branch, make
all proposition letters $p$ with $@m p$ 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 $\phi$.
\begin{theorem}
The tableau calculus for ${\cal HL}(@,\breve{},\downarrow)$ is complete.
\end{theorem}
\begin{proof}
Immediate from Theorem \ref{PPfair}, plus the fact that every open
branch of a finished tableau for $\phi$ yields a Kripke model for
$\phi$.
\end{proof}
\section{Adding the Universal Modality}
We now extend the language with the universal modality $A$ and
its dual $E$, with the following intended meanings:
\begin{eqnarray*}
\M, g, w \forces A\phi & \text{ iff } & \text{ for all }w' \in M
\text{ it holds that } \M, g, w' \forces \phi \\
\M, g, w \forces E\phi & \text{ iff } & \text{ for some }w' \in M
\text{ it holds that } \M, g, w' \forces \phi
\end{eqnarray*}
It is well known that binding together with universal modality makes
it possible to express full quantification. The definition of the
quantifiers is as follows:
\begin{eqnarray*}
\M, g, w \forces \forall x \phi & \text{ iff } & \text{ for all }g'
\text{ with } g \stackrel{x}{\sim} g' \text{ it holds that }
\M, g', w \forces \phi \\
\M, g, w \forces \exists x \phi & \text{ iff } & \text{ for some }g'
\text{ with } g \stackrel{x}{\sim} g' \text{ it holds that }
\M, g', w \forces \phi
\end{eqnarray*}
It is not hard to see that $\forall x \phi$
can be taken as shorthand for $\downarrow\! y . A\downarrow\! x . @ y
\phi$, and $\exists x \phi$ as shorthand for $\downarrow \!y
. E\downarrow \!x . @ y \phi$. So we have full quantification once we
know how to deal with the modalities $A$ and $E$. Tableau rules for
$A$ and $E$ can look like this:
\[
\cfrac{@m A \phi}{@n \phi}\ n \text{ on the branch }
\hspace*{3em}
\cfrac{@m \neg E \phi}{@n \neg \phi} \ n \text{ on the branch }
\]
\[
\cfrac{@m E \phi}{@n \phi}\ n \text{ fresh }
\hspace*{3em}
\cfrac{@m \neg A \phi}{@n \neg \phi} \ n \text{ fresh }
\]
Since the tableau rules for $A$ and $E$ are obviously sound, we
get by induction on tableau structure:
\begin{theorem}
The tableau calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is
sound.
\end{theorem}
\begin{figure}[htbp] \footnotesize
\bc
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{(n:U),A,I,P,N,C,(@ n \phi':F)
+\!\!+\, [@ n \psi \mid A \psi \in C] }
\ \phi \in E, n \text{ fresh }
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{U,A,I,P,N,(\phi:C),F
+\!\!+\, [@ n \phi' \mid n \in U ] }
\ \phi \in A
\]
\[
\cfrac{U,A,I,P,N,C,(@m \Idia{i} n:F)}
{U,(mR_in:A),I,P,N,C, F
+\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C]
+\!\!+\, [@ m \psi \mid @ n \Icbox{i} \psi \in C]
+\!\!+\, [@ m \psi \mid A \psi \in C]}
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{(n:U),(mR_in:A),I,P,N,C,(@ n \phi':F)
+\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C]
+\!\!+\, [@ n \psi \mid A \psi \in C] }
\ \phi \in \Idia{i}, n \text{ fresh }
\]
\[
\cfrac{U,A,I,P,N,C,(@m \Icdia{i} n:F)}
{U,(nR_im:A),I,P,N,C, F
+\!\!+\, [@ n \psi \mid @ m \Icbox{i} \psi \in C]
+\!\!+\, [@ n \psi \mid A \psi \in C] }
\]
\[
\cfrac{U,A,I,P,N,C,(@m \phi:F)}
{(n:U),(nR_im:A),I,P,N,C,(@ n \phi':F)
+\!\!+\, [@ n \psi \mid @ m \Icbox{i} \psi \in C]
+\!\!+\, [@ n \psi \mid A \psi \in C] }
\ \phi \in \Icdia{i}, n \text{ fresh }
\]
\ec
\caption{Modified Constraint Proof Engine for
${\cal HL}(@,\breve{},\downarrow,A)$.}
\label{APEfig}
\end{figure}
Figure \ref{APEfig} lists the modifications in the constraint proof
engine that are necessary to accommodate the universal modality. The
conditions $\phi \in A$, $\phi \in E$ have the obvious
meanings. $A$-type formulas are of the forms $A\psi$, with component
$\psi$, and $\neg E \psi$, with component $\neg
\psi$. $E$-type formulas are of the forms $E\psi$, with component
$\psi$, and $\neg A\psi$, with component $\neg \psi$.
The constraint store $C$ now also contains universal formulas
$A \psi$, and the corresponding constraints have to be imposed on
{\em all}\/ nominals that turn up at the branch.
The results about fairness and completeness extend to the new
calculus and proof engine:
\begin{theorem} \label{APEfair}
The modified Constraint Proof Engine of Figure \ref{APEfig} is fair.
\end{theorem}
\begin{theorem}
The tableau calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is
complete.
\end{theorem}
\section{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 {\em 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:
\begin{description}
\item[Irreflexive Frames for $R_i$]
Modify the start rule to:
\[
\cfrac{\text{start } \phi}
{[m],
[],
[],
[],
[],
[A \downarrow x. \Ibox{i} \neg x],
[@ m \phi]}
\ m \text{ fresh }
\]
\item[Reflexive Frames for $R_i$]
Modify the start rule to:
\[
\cfrac{\text{start } \phi}
{[m],
[],
[],
[],
[],
[A \downarrow x. \Idia{i} x],
[@ m \phi]}
\ m \text{ fresh }
\]
\item[Transitive Frames for $R_i$]
Modify the start rule to:
\[
\cfrac{\text{start } \phi}
{[m],
[],
[],
[],
[],
[A \downarrow x. \Ibox{i}\Ibox{i}\Icdia{i}x],
[@ m \phi]}
\ m \text{ fresh }
\]
\item[S4 Frames for $R_i$]
Modify the start rule to:
\[
\cfrac{\text{start } \phi}
{[m],
[],
[],
[],
[],
[A \downarrow x. (\Idia{i} x \land \Ibox{i}\Ibox{i}\Icdia{i}x)],
[@ m \phi]}
\ m \text{ fresh }
\]
\end{description}
It is obvious that this can be done for any frame class that can be
described (hence characterized) by a formula in the first order
correspondence language of hybrid logic. This is so since we have the
full power of quantification available now; see
\cite{BlaSel:what98}. This gives the following:
\begin{theorem}[General Completeness]
The tableau calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is
complete for any frame class that can be described in the first order
correspondence language of ${\cal HL}(@,\breve{},\downarrow,A)$.
\end{theorem}
\section{Modifying the Calculus for Minimal Model Generation}
A model $\M$ is minimal for $\phi$ if there are $g,w$ with $\M, g, w
\forces \phi$, and for all $\N,h,w'$ with $\N,h, w' \forces \phi$ it
holds that $|N| \geq |M|$. E.g., the formula $\neg c \land
\Box\Diamond \top$ has minimal models of size $2$.
To generate minimal models, replace the $\Idia{i}$ and $\Icdia{i}$
rules by the following trial-and-error versions:
\paragraph{$\Idia{i}$ rules, trial-and-error version}
\[
\cfrac{@n \Idia{i}\phi}{
\begin{array}{c} nRk_1 \\
@ k_1 \phi
\end{array}
|
\cdots
|
\begin{array}{c} nRk_s \\
@ k_s \phi
\end{array}
|
\begin{array}{c} nRm \\
@m \phi
\end{array}
}\text{ $k_1, \ldots k_s$ all nominals on the branch,
$m$ fresh}
\]
\[
\cfrac{@n \neg \Ibox{i} \phi}{
\begin{array}{c} nRk_1 \\
@ k_1 \neg \phi
\end{array}
| \cdots |
\begin{array}{c} nRk_s \\
@ k_s \neg \phi
\end{array}
|
\begin{array}{c} nRm \\
@ m \neg \phi
\end{array}
}\text{ $k_1, \ldots k_s$ all nominals on the branch,
$m$ fresh}
\]
\paragraph{$\Icdia{i}$ rules, trial-and-error version}
\[
\cfrac{@n \Icdia{i}\phi}{
\begin{array}{c} k_1Rn \\
@ k_1 \phi
\end{array}
|
\cdots
|
\begin{array}{c} Rk_sRn \\
@ k_s \phi
\end{array}
|
\begin{array}{c} mRn \\
@m \phi
\end{array}
}\text{ $k_1, \ldots k_s$ all nominals on the branch,
$m$ fresh}
\]
\[
\cfrac{@n \neg \Icbox{i} \phi}{
\begin{array}{c} k_1Rn \\
@ k_1 \neg \phi
\end{array}
| \cdots |
\begin{array}{c} k_sRn \\
@ k_s \neg \phi
\end{array}
|
\begin{array}{c} mRn \\
@ m \neg \phi
\end{array}
}\text{ $k_1, \ldots k_s$ all nominals on the branch,
$m$ fresh}
\]
Similarly, replace the $E$ rule also by its trial-and-error version.
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%
{\Tr{
@ s \Diamond \neg s, @ s \Box \downarrow x. \Diamond (\neg s \land \neg x),
@ s \Box \Box \downarrow x. @ s \Diamond x
}}{
\pstree{\Tr{
sRt, @ t \neg s
}}{
\pstree{\Tr{
t \NEQ s
}}{
\pstree{\Tr{
@ t \downarrow x. \Diamond (\neg s \land \neg x)
}}{
\pstree{\Tr{
@ t \Diamond (\neg s \land \neg t)
}}{
\pstree{\Tr{
tRt', t' \NEQ s, t' \NEQ t
}}{
\pstree{\Tr{
@t \Box \downarrow x . @ s \Diamond x
}}{
\pstree{\Tr{
@t'\downarrow x . @ s \Diamond x
}}{
\pstree{\Tr{
@t' @ s \Diamond t'
}}{
\pstree{\Tr{
@ s \Diamond t'
}}{
\pstree{\Tr{
sRt'
}}{
\pstree{\Tr{
@ t' \downarrow x. \Diamond ( \neg s \land \neg x)
}}{
\pstree{\Tr{
@ t' \Diamond ( \neg s \land \neg t')
}}{
\pstree{\Tr{
t'Rt'', t'' \NEQ s, t'' \NEQ t'
}}{\Tr{\vdots}}
}
}
}
}
}
}
}
}
}
}
}
}
}
$
\end{center}
\caption{Tableau for (\ref{NinfConj}).}
\label{FigNinfConj}
\end{figure}
\begin{figure}[htbp]
\begin{center}
$
\pstree[nodesep=3pt,levelsep=1.2cm,treesep=1cm]%
{\Tr{
@ s \Diamond \neg s, @ s \Box \downarrow x. \Diamond (\neg s \land \neg x),
@ s \Box \Box \downarrow x. @ s \Diamond x
}}{
\pstree{
\Tr{
sRs, @s \neg s
}}{
\Tr{\bot}}
\pstree{
\Tr{
sRt, @ t \neg s
}}{
\pstree{\Tr{
t \NEQ s
}}{
\pstree{\Tr{
@ t \downarrow x. \Diamond (\neg s \land \neg x)
}}{
\pstree{\Tr{
@ t \Diamond (\neg s \land \neg t)
}}{
\pstree{\Tr{tRs, @s(\neg s \land \neg t)}}
{\Tr{\begin{array}{c}
\vdots \\
\bot
\end{array}}}
\pstree{\Tr{tRt, @s(\neg s \land \neg t)}}
{\Tr{\begin{array}{c}
\vdots \\
\bot
\end{array}}}
\pstree{\Tr{
tRt', t' \NEQ s, t' \NEQ t
}}{
\pstree{\Tr{
@t \Box \downarrow x . @ s \Diamond x
}}{
\pstree{\Tr{
@t'\downarrow x . @ s \Diamond x
}}{
\pstree{\Tr{
@t' @ s \Diamond t'
}}{
\pstree{\Tr{
@ s \Diamond t'
}}{
\pstree{\Tr{
sRt'
}}{
\pstree{\Tr{
@ t' \downarrow x. \Diamond ( \neg s \land \neg x)
}}{
\pstree[nodesep=3pt,levelsep=1.7cm,treesep=1cm]{\Tr{
@ t' \Diamond ( \neg s \land \neg t')
}}{
\Tr{\begin{array}{c}
t'Rs \\
\vdots \\
\bot
\end{array}}
\Tr{\begin{array}{c}
t'Rt' \\
\vdots \\
\bot
\end{array}}
\Tr{\begin{array}{c}
t'Rt \\
\vdots \\
\text{open}
\end{array}}
\Tr{\begin{array}{c}
t'Rt'' \\
\vdots
\end{array}}
}
}
}
}
}
}
}
}
}
}
}
}
}
$
\end{center}
\caption{Trial-and-error tableau for (\ref{NinfConj}).}
\label{FigTENinfConj}
\end{figure}
Figure \ref{FigNinfConj} gives an infinite tableau expansion for
Formula \sref{NinfConj}.
\begin{equation} \label{NinfConj}
@ s \Diamond \neg s \land
@ s \Box \downarrow x. \Diamond (\neg s \land \neg x)
\land
@ s \Box \Box \downarrow x. @ s \Diamond x
\end{equation}
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
\ref{FigTENinfConj}.
Again, the new rules are obviously sound, so we get:
\begin{theorem}
The minimal model calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is
sound.
\end{theorem}
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:
\begin{theorem}
The minimal model calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is
complete.
\end{theorem}
\commentout{
\section{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
\cite{Benthem:panicl}. 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 $\phi$ can be used to generate a whole range of
Kripke models for $\phi$, including minimal models. The following node
compression algorithm accomplishes this.
\bc
\begin{center}{ \bf Node Compression Algorithm }\end{center}
Let a finished open constraint tableau node $(U,A,I,P,N,C,[])$ be
given.
\begin{itemize}
\item If there are no pairs of nominals $m,n$ with $m$ preceding $n$
and $m\NEQ n \notin I$ then return the unit list
$[(U,A,I,P,N,C,[])]$.
\item Otherwise, nondeterministically pick a pair of
nominals $m,n$ with $m$ preceding $n$ and $m\NEQ n \notin I$.
\begin{description}
\item[Compression Step] Develop the tableau
$[(U^n_m,A^n_m,I^n_m,P^n_m,N^n_m,[],C^n_m)]$.
\begin{itemize}
\item If this remains open, then compress the finished open nodes
and collect the results.
\item If it closes, then compress $(U,A,(m\NEQ n:I),P,N,C,[])$.
\end{itemize}
\end{description}
\end{itemize}
\ec
\begin{theorem}[Soundness of Node Compression Algorithm]
If the node compression algorithm is applied to a finished open tableau node
for $\phi$, then all finished open tableau nodes that result from the
algorithm satisfy $\phi$.
\end{theorem}
\begin{proof}
Induction on the number of nominal pairs $m,n$
with $m$ preceding $n$ and $m \NEQ n \notin I$ on a finished open
tableau node for $\phi$.
\end{proof}
\begin{theorem}[Completeness of Node Compression Algorithm]
If the node compression algorithm is applied to a finished open tableau
node for $\phi$ it yields at least one open node
\[
(U,A,I,P,N,C,[])
\]
that corresponds to a minimal model for $\phi$.
\end{theorem}
\begin{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\NEQ n:I),P,N,C,[])
\]
is open. Since the resulting open nodes cannot be
compressed any further, at least one of them is minimal.
\end{proof}
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
\cite{Areces:le,AreBlaMar:hlcic}, 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 $\bar{m}
\in {}^k M$ and $\bar{n} \in {}^k N$, any hybrid bisimulation (for
that language) $\stackrel{\omega}{\sim}$ with $(\M, \bar{m})
\stackrel{\omega}{\sim} (\N, \bar{n})$ and $\bar{m}(i) = \bar{m}(j)$
satisfies $\bar{n}(i) = \bar{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.
}
\section{Deciding Some Fragments of Hybrid Logic}
It is well known that ${\cal HL}(@)$ and ${\cal HL}(@,\breve{})$ are
decidable. Theorem \ref{PdecidesAt} states that the constraint proof
engine from Section \ref{PP} decides hybrid logic formulas without
binders.
\begin{theorem} \label{PdecidesAt}
The constraint proof engine for hybrid logic decides satisfiability of
${\cal HL}(@,\breve{})$ formulas.
\end{theorem}
\begin{proof}
The result follows from a modal depth argument. ${\cal
HL}(@,\breve{})$ has a notion of finite degree (\cite{BlaRijVen:ml},
Ch. 7); in particular, modal depth for its formulas can be defined as
follows:
\begin{eqnarray*}
d(p) = d(c) = d(x) & = & 0 \\
d(\phi * \psi) & = & \max(d(\phi), d(\psi)),
* \in \{ \land, \lor, \rightarrow \} \\
d(\neg \phi) & = & d(\phi) \\
d(M \phi) & = & d(\phi) + 1,
M \in \{ \Ibox{i}, \Idia{i}, \Icbox{i}, \Icdia{i} \} \\
d(@ m \phi) & = & d(\phi)
\end{eqnarray*}
Every non-literal formula $\phi \notin \{\Ibox{i}, \Icbox{i} \}$ gets
decomposed by the rule that applies to it. Every formula $\phi \in
\{\Ibox{i},
\Icbox{i} \}$ generates a constraint. When a constraint $@ m \Box
\phi$ is combined with an $mRn$ relation, it generates a new formula
$@ n \phi$ on the list of pending formulas, but $d(\phi) = d(\Box\phi)
- 1$. Thus, the box formula $@m \Box \phi$ gets replaced by a finite
number of $@ n \phi$ formulas, and each of these is appended to the
list of pending formulas, so fairness of the procedure is preserved.
\end{proof}
\commentout{
At first sight, there is something puzzling about the undecidability
of ${\cal HL}(@,\breve{},\downarrow)$, especially since the so-called
standard translation given in \cite{Areces:le,AreBlaMar:hlcic} 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
$\downarrow u . \Box \Box \downarrow w. @ u \Diamond w$. Carrying out
the instruction starting out from $\text{ST}_x(\downarrow u . \Box
\Box \downarrow w. @ u \Diamond w)$, we end up with an injunction to
substitute $x$ for $u$ in $\forall y (Rxy \rightarrow \forall x (Ryx
\rightarrow \exists y (Ruy \land y = x)))$, with capture of $x$ by
$\forall x$ as a result. The standard translation can be repaired by
replacing the instructions for the modalities and the binders as
follows:
\begin{eqnarray*}
\text{ST}_x (\Idia{i}\phi) & := & \exists y (R_ixy \land \text{ST}_y
\phi) \text{ with $y$ a fresh variable,} \\
\text{ST}_x (\downarrow w.\phi)
& := & (\text{ST}_y \phi)^w_y \text{ with $y$ a fresh
variable.}
\end{eqnarray*}
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 $\downarrow$ in the
scope of box modalities that causes undecidability of ${\cal
HL}(@,\breve{},\downarrow)$. Consider the version of ${\cal
HL}(@,\breve{},\downarrow)$ without $\Ibox{i}, \Icbox{i}, \rightarrow$
that can be got by paraphrasing d with the help of $\Ibox{i} \phi
\leftrightarrow \neg \Idia{i}\neg \phi$, $\Icbox{i} \phi
\leftrightarrow \neg \Icdia{i}\neg \phi$, and $(\phi \rightarrow \psi)
\leftrightarrow \neg \phi \lor \psi$. A subformula $\psi$ of $\phi$
is {\em existential}\/ in $\phi$ if every $\Diamond$ that outscopes
$\psi$ in $\phi$ is in the scope of an even number of negation
operators. Thus, $\psi$ is existential in $\Diamond
\neg \psi$ and $@ m \neg(\Diamond m \land \neg \Diamond \psi)$,
but not in $\neg \Diamond \psi$. Call a formula $\phi$ {\em
innocent}\/ if every binder subformula $\downarrow x. \psi$ of $\phi$
is existential in $\phi$.
\begin{theorem}
The innocent fragment of ${\cal HL}(@\breve,\downarrow)$
is decidable.
\end{theorem}
\begin{proof}
Consider the following translation from (located formulas of) ${\cal
HL}(@,\breve{},\downarrow)$ to ${\cal HL}(@,\breve{})$.
\begin{eqnarray*}
(@m p)^T & := & @m p \\
(@m n)^T & := & @m n \\
(@m \neg \phi)^T & := & \neg (@ m\phi)^T \\
(@m \phi \land \psi)^T & := & (@ m\phi)^T \land (@ m\psi)^T \\
(@m \phi \lor \psi)^T & := & (@ m\phi)^T \lor (@ m\psi)^T \\
(@m @n \phi)^T & := & (@ n \phi)^T \\
(@m \Idia{i}\phi)^T & := & @m \Idia{i} (n \land (@ n \phi)^T),
\text{ $n$ a fresh nominal } \\
(@m \Icdia{i}\phi)^T & := & @m \Icdia{i} (n \land (@ n \phi)^T),
\text{ $n$ a fresh nominal } \\
(@m \downarrow x. \phi)^T & := & (@ m \phi [ x:= m])^T
\end{eqnarray*}
Check by induction on formula structure that this translation is
truth-preserving for all formulas in the innocent fragment.
\end{proof}
Another way of seeing this is by observing that the tableaux for
$\phi$ and $\phi^T$ are essentially the same, which leads immediately
to:
\begin{theorem}
The constraint proof engine for ${\cal HL}(@,\breve{},\downarrow)$
decides the innocent fragment.
\end{theorem}
}
Consider the following fragment of {\em existential}\/ formulas of
${\cal HL}(@,\breve{})$:
\begin{eqnarray*}
\psi & ::= & n \mid \neg n \mid \neg \Idia{i} n \mid
\neg \Icdia{i} n \mid \psi \land \psi' \mid \psi \lor \psi'
\mid \Idia{i} \psi \mid \Icdia{i} \psi
\end{eqnarray*}
Use this to define ${\cal HL}(@,\breve{},\downarrow^\exists)$,
by changing the definition of binder formulas from $\downarrow x.
\phi$ to $\downarrow x. \psi$. In other words, binding is only
allowed over existential formulas. If, moreover, we only allow one
binding variable $w$, we get \cite{Marx02:nsas}:
\begin{theorem}[M. Marx]
The language ${\cal HL}(@,\breve{},(\downarrow w)^\exists)$ is
decidable in EXPTIME.
\end{theorem}
\begin{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 \cite{Graedel:otrpog}, existential guards can be dispensed
with, for the sentence $(\forall \bfx . \alpha) \exists \bfy
\phi(\bfx\bfy)$, with $\exists \bfy$ unguarded, is satisfiable if and
only if the properly guarded sentence $(\forall \bfx . \alpha) \exists
\bfy R\bfx\bfy\ \land (\forall \bfx . R\bfx \bfy) \phi(\bfx\bfy)$,
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
\cite{Graedel:otrpog}.
\end{proof}
If we allow an unrestricted number of binding variables $x_1, \ldots$
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 \cite{Graedel:otrpog}.
\begin{theorem}
The constraint proof engine for hybrid logic decides satisfiability of
${\cal HL}(@,\breve{},\downarrow^\exists)$ formulas.
\end{theorem}
\begin{proof}
Suppose the proof engine is invoked to check satisfiability of
$\phi$. We only need to be concerned about formulas of the forms
$\Ibox{i} \downarrow x .\psi$, $\Idia{i} \neg \downarrow x. \psi$,
$\Icbox{i} \downarrow x . \psi$ $\Icdia{i} \neg\downarrow x . \psi$ that
turn up along a tableau branch during the processing of $\phi$, for
these are the formulas that cause binders to appear in the $\Ibox{i}$
and $\Icbox{i}$ constraints. Suppose $@m \Box \downarrow x. \psi$ is
in the box constraint store, and gets combined with an $mRn$
accessibility along the branch. Then $@n \downarrow x. \psi$ will get
appended to the pending formula list. When $@n \downarrow x. \psi$
gets decomposed, it gets replaced by $\psi^x_n$, and further
decomposition will not affect the constraint stores because $\psi$ is
existential.
\end{proof}
\section{Related Work}
%\paragraph{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 \cite{Fitting:pmfmail} is given in
\cite{Tzakova:tcfhl}. This does not yet make full use of the
possibility to let the role of prefixes be played by nominals. In
\cite{Blackburn:ild} 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 \cite{BlaBurWal:hydr01}.
%\paragraph{Comparison with resolution for hybrid logic}
%The resolution approach to modal logic dates back to at least
%\cite{Ohlbach88:arcfml,EnjFar89:mricf}.
A prefixed resolution calculus for description and hybrid logic was
proposed in \cite{AreNivRij:reso01}, and implemented in
\cite{AreHeg01:hylores}. Detailed efficiency comparison with this
is work in progress.
\paragraph{Acknowledgement}
Thanks to the Dynamo team (Wim Berkelmans, Balder ten Cate, Juan
Heguiabehere, Breannd\'an \'O Nuall\'ain) and to Carlos Areces,
Patrick Blackburn and Maarten Marx, for useful comments and fruitful
discussion. This work was carried out as part of the INRIA funded
partnership between LITG (Language and Inference Technology Group at
ILLC, University of Amsterdam) and LED (Langue et Dialogue, LORIA,
Nancy).
\bibliographystyle{acm}
\bibliography{/home/jve/texmacros/mybibAG,/home/jve/texmacros/mybibHZ}
\end{document}