\documentclass[a4paper]{llncs}

%\usepackage{sober}
\usepackage{exptrees}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{latexsym}

\input{ai98defs}

\begin{document}

\title{A Mechanisation of Classical Modal Tense Logics Using Isabelle}

\author{Jeremy E Dawson and Rajeev Gor{\'{e}} }

\institute{Automated Reasoning Project and Department of Computer
  Science \\ Australian National University, 0200, Canberra
          \\ {\tt \{jeremy,rpg\}@arp.anu.edu.au}}

\maketitle

\begin{abstract}
  We present an implementation of an interactive theorem prover for
  the basic tense logic $\Kt$, and many of its extensions,
using the generic proof assistant Isabelle.
The novelty of the implementation is that we use a Display Logic formalism of
$\Kt$ as opposed to a traditional Gentzen system.
 The prover is intended to assist in meta-theoretical studies of
 tense logics rather than to be a fast theorem prover.
Since Display Logic is a generic way to capture multi-modal
 logics, our implementation can be trivially extended to handle
the multi-modal logics of 
 ``time", ``knowledge", ``intentions", ``desires" and ``beliefs" 
 which are used in Artificial Intelligence research.

\textbf{Keywords}
 automated deduction, hybrid logics, logics for knowledge and
 belief, display logic, tense logic, sequent calculus.


\end{abstract}

\section{Introduction}

Formal calculi for reasoning about modalities are an important part of
Artificial Intelligence research where nonclassical logics are often
used to model notions like time, belief and knowledge
\cite{Fagin&Halpern&Moses&Vardi95}. As our understanding of these
calculi increases, so does our ability to model more complicated
notions like Logics of Actions \cite{pratt-action-logic} or Logics of
Information Flow \cite{barwise-gabbay-hartonas-information-flow} using
other, more complicated nonclassical logics like Relevance Logics
\cite{anderson-belnap-entailment-I}, Linear Logic \cite{girard-linear}, or
arbitrary substructural logics
\cite{dosen-schroeder-heister-substructural}. The eventual aim is to
be able to form natural hybrids from these individual logics by
choosing aspects like ``tense'', ``resource consciousness'',
``classicality'' or ``constructivity'' as required by the complex
artificial intelligence task we wish to model.
 
The traditional formalisation of these individual logics is via
Hilbert systems since we have a very good understanding of such
systems for many nonclassical logics. But Hilbert systems are
notoriously bad for proof search, and such formulations are of little
practical use when trying to build a working system.

More modern automated reasoning techniques like resolution are usually
not applicable because non-classical logics rarely possess an analogue
of ``clausal normal form''. For example, there are numerous automated
or semi-automated systems which handle classical tense or temporal
logics in a resolution framework
\cite{fisher-woolridge-dixon-resolution},
\cite{ohlbach-resolution-modal},
\cite{debart-enjalbert-lescot-multi-modal},
\cite{farinal-del-cerro-simple}, but these methods 
do not immediately
lend themselves to handle hybrids like Relevant Tense Logics or even
Intuitionistic Tense Logics because it is not at all clear that
resolution or translation methods can be extended to substructural
logics in general.

As has been argued elsewhere \cite{wallen-book}, cut-free Gentzen
systems are a good formulation for ``backward'' or ``goal-directed''
proof search.  But 
%Gentzen systems for nonclassical logics are not so well-understood, and
it is rare to find an ``off the shelf''
(cut-free) Gentzen system for the particular nonclassical logic one
requires.  Mechanisations of many of these logics do exist in the
literature, but they are invariably for a particular logic, and do not
facilitate the formation of hybrids.  For example, one of the fastest
automated theorem provers for tense logic and multi-modal logics is
the Logics Workbench \cite{heuerding-seyfried-zimmermann-loop}.
Although the Logics Workbench allows you to form multi-modal logics,
it does not allow one modality to be based on \textbf{S4} and another
on \textbf{K45}.

Display logic \cite{belnap-display} is a general Gentzen-style
formulation which not only captures a huge variety of logics, but
which was specifically designed for the formation of hybrid
nonclassical logics.  Display calculi exist for Linear,
Relevant, BCK, Lambek and other substructural logics
\cite{gore-sld-igpl,restall-substructural-I}, for the logic of
Relation Algebras \cite{gore-relalg}, and even for nominal tense
logics \cite{demri-gore-nominal-tense}.  All of these
calculi are not only cut-free, but they are modular in that they can
be easily combined to form cut-free display calculi for natural hybrid
logics like Relevant Tense Logic; see \cite{gore-sld-igpl} for
details. Hence a general mechanisation of display logic would allow us
to capture many different logics in one uniform setting.

Here, we first learn to walk before learning to run by demonstrating
that we can mechanise the displayed tense logics of Wansing
\cite{wansing-sequent} by using Paulson's generic proof assistant
Isabelle \cite{paulson-700}.
This mechanisation uses the generic character of Isabelle, so that
we use $\Dl{\Kt}$ as the ``native'' logic of the implementation,
rather than entering $\Dl{\Kt}$ axioms ``on top of'' (say)
classical logic.
More importantly, it is possible to obtain a vast number of extensions
of displayed tense logics by encoding certain Hilbert axioms as
structural rules of display logic, in a purely modular way. Thus our
implementation not only caters to a vast number of tense and multi-modal
logics, but it is trivially
extendable to handle various other modalities to cater for ``belief''
or ``knowledge'', as long as these modalities are based on classical
modal logic. Our system therefore provides the essential ingredients
for the formation of a hybrid modal or tense logic to suit your needs.

Our current implementation does not provide a decision procedure,
although many of these individual logics are known to be
decidable. But we are currently working on such an extension.  However,
the implementation has already helped with meta-theoretical studies,
as demonstrated in \cite{gore-sld-igpl}.

% We can now turn our attention to the numerous other display calculi
% that exist. The eventual aim is to provide a single uniform
% implemented framework for many different logics, so that natural
% hybrids of these logics can be formed with ease, by the user.  The
% user need not be an expert in these logics, but may want to play with
% various exotic logics until a suitable one is found for his or her
% needs.  For example, ``classicality'' can be removed simply by
% replacing the classical display rules by a display calculus for
% Intuionistic Logic \cite{gore-ilr}, thereby giving an implementation
% for Intuitionistic Tense Logics.

The plan of the paper is as follows. In Section~\ref{cmtl} we define the
syntax of classical modal tense logics. In Section~\ref{cmdl} we briefly
describe the classical modal display logic of Wansing. 
In Section~\ref{Isabelle} we briefly describe the proof assistant Isabelle.
In Section~\ref{dlisa} we explain how we captured displayed tense logics in
Isabelle, explain the various Isabelle tactics which were written, and
give an example of a complicated display logic proof.
In Section~\ref{faxsr} we describe how we can store certain previously proved
theorems for future use in a totally general way.
In Section~\ref{ace} we highlight the beauty of display logic by
desribing an automatic cut-elimination process that 
converts a proof containing cuts into a cut-free proof.
In Section~\ref{fwconcl} we describe future work and conclude.

\section{Classical Modal Tense Logics} \label{cmtl}

The {\bf formulae} of our logics are built using the following BNF
grammar where $A$ and $B$ stand for formulae and $p$ for any primitive
proposition:
$$ %\begin{eqnarray*}
  A \ B \quad :: = \quad p \mid \ExTop \mid \ExBot \mid 
  % A \ B & :: = & p \mid \ExTop \mid \ExBot \mid 
         \WhtDia A \mid \WhtBox A \mid 
         \BlkDia A \mid \BlkBox A \mid \ExNot A \mid
         A \InImp B \mid A \ExAnd B \mid A \ExOr B % \\[-1em]
$$ %\end{eqnarray*}

All the connectives except 
$\WhtDia$, $\WhtBox$, $\BlkDia$ and $\BlkBox$ 
are the familiar ones from classical propositional logic.
The formula $\WhtDia A$ is usually read as ``sometime in the future'',
$\BlkDia A$ as ``sometime in the past'',
$\WhtBox A$ as ``always in the future''
and $\BlkBox A$ as ``always in the past''.
A good introduction to Kripke semantics for modal logics is 
\cite{hughes-cresswell-new-introduction}.

Logics of knowledge and belief are obtained by using multiple
modalities so that, for example, $\WhtBox_i A$ is read as ``agent $i$
knows that $A$ is true'' \cite{Fagin&Halpern&Moses&Vardi95}.  

\section{Classical Modal Display Logic} \label{cmdl}

Display Logic \cite{belnap-display} is a powerful Gentzen formulation designed
to allow the formation of hybrid logics.
Its beauty is a generic cut-elimination theorem.
Display logic is, unfortunately, rather an arcane methodology. It is
best explained via an example which should be familiar to most
readers.

Consider the equation $2x^{2} - 4 \leq 0$, familiar from high school
algebra. It can be solved if we ``make $x$ the subject'' by
manipulating the equation
as follows:\\[0.4em]
\begin{tabular}{lcl}
the equation  & $(2 \times x^{2}) - 4 \leq 0$ & \\
becomes       & $(2 \times x^{2}) \leq 0 + 4$ & by adding $4$ to both sides \\
becomes       & $x^{2} \leq (0 + 4)/2$& by dividing both sides by $2$\\
becomes       & $x \leq \sqrt{(0 + 4)/2}$ & by taking (positive) square
                                         root of both sides \\[0.4em]
becomes       & $x \leq \sqrt{2}$ & by simplification (or rewriting). \\
\end{tabular}\\
Most of these manipulations are only possible because the operations
come in ``opposite'' pairs that undo the effects of each other; namely
$(+, -)$, $(\times, /)$, $(x^{2}, \sqrt{x})$. Thus, the ability to
``make $x$ the subject'' by using ``opposite pairs'' and to rewrite a
term into a simpler (but equivalent) form are fundamental.


Instead of natural numbers and operators like multiplication, display
logic has the following syntax.
In \Dl{K_{t}}, {\bf structures} are built using the {\bf structural
  connectives} $\ExTpBt$, $\blkb$, $\semic$ and $\ast$ according to the
following BNF grammar where $A$ stands for any
formula and $X$, $Y$, and later $V$, $W$ and $Z$, stand for structures:\\
% \begin{center}
% \begin{tabular}{ccl}
  % $X \  Y$:: = & $A \mid \ExTpBt \mid \blkb X \mid \ast
  % X \mid A \semic B$ \\ 
% \end{tabular}
% \end{center}
% \bigskip
  $$X \  Y \quad :: =  \quad  A \mid \ExTpBt \mid \blkb X \mid \ast
   X \mid X \semic Y$$

Note that, unlike in standard Gentzen systems, comma is not a
structural connective, and no structural connective is
automatically polyvalent.

A {\bf sequent} is an expression of the form $X \vdash Y$ with
$X$ the {\bf antecedent} and $Y$ the {\bf succedent}. A {\bf sequent
  rule} is defined from sequents in the usual way with the {\bf
  premises} above the line and the {\bf conclusion} below the line.

Thus, in Display Logic, sequents are the analogues of algebraic
inequations. The display property allows us to pick any 
substructure $X$ of the construct $V \vdash W$, and to ``make $X$
the subject'' on one side by moving all other constituents onto the
other side of the turnstile $\vdash$. The $X$ is said to be
``displayed''.
The ``display property'' is a by-product of special, {\em reversible}
rules, called the {\bf display postulates} , which allow us to unravel
structures. See Figure~\ref{fig:logical-rules-dkt}.

%
%\begin{figure}[htbp]
%  \begin{center}
%\begin{picture}(300, 150)
%\put(0, 360){\urule{$(\mbox{Nec }\vdash)$}
%                    {$\ExTpBt \vdash X$}
%                    {$\blkb \ExTpBt \vdash X$}
%}
%\put(230, 360){\urule{$\vdash (\mbox{ Nec})$}
%                    {$X \vdash \ExTpBt $}
%                    {$X \vdash \blkb \ExTpBt $}
%}
%
%\put(230, 360){$(\ExBot \vdash)\ \ \ExBot \vdash \ExTpBt $}
%\put(0, 360){\urule{$(\ExTop \vdash)$}
%                    {$\ExTpBt \vdash X$}
%                    {$\ExTop \vdash X$}}
%
%\put(0, 320){\urule{$(\ExTop \vdash)$}
%                    {$\ExTpBt \vdash X$}
%                    {$\ExTop \vdash X$}}
%\put(230, 320){$(\vdash \ExTop)\ \ \ExTpBt \vdash \ExTop$}
%
%\put(0, 280){\brule{$(\InImp \vdash)$}
%                    {$X \vdash A$}
%                    {$B \vdash Y$}
%                    {$A \InImp B \vdash \ast X \semic Y$}}
%\put(230, 280){\urule{$(\vdash \InImp)$}
%                     {$X \semic A \vdash B$}
%                     {$X \vdash A \InImp B$}}
%
%\put(230, 240){\brule{$(\ExOr \vdash)$}
%                     {$A \vdash  X$}
%                     {$B \vdash  X$}
%                     {$A \ExOr B \vdash X $}}
%\put(0, 240){\urule{$(\vdash \ExOr)$}
%                    {$X \vdash A \semic B $}
%                    {$X \vdash A \EXOr B $}}
%
%\put(0, 200){\urule{$(\ExAnd \vdash)$}
%                    {$A \semic B \vdash X$}
%                    {$A \EXAnd B \vdash X$}}
%\put(230, 200){\brule{$(\vdash \ExAnd)$}
%                     {$X \vdash  A$}
%                     {$X \vdash  B$}
%                     {$X \vdash A \ExAnd B$}}
%
%\put(0, 160){\urule{$(\ExNeg \vdash)$}
%                    {$\ast A \vdash X$}
%                    {$\ExNeg A \vdash X$}}
%\put(230, 160){\urule{$(\vdash \ExNeg)$}
%                     {$X \vdash \ast A$}
%                     {$X \vdash \ExNeg A$}}
%
%
%\put(0, 140){\urule{$(\BlkDia \vdash)$}
%                    {$\blkb A \vdash X$}
%                    {$\BlkDia A \vdash X$}}
%\put(230, 140){\urule{$(\vdash \BlkDia)$}
%                     {$X \vdash A$}
%                     {$\blkb X \vdash \BlkDia A$}}
%
%\put(0, 100){\urule{$(\WhtBox \vdash)$}
%                    {$A \vdash X$}
%                    {$\WhtBox A \vdash \blkb X$}}
%\put(230, 100){\urule{$(\vdash \WhtBox)$}
%                     {$X \vdash \blkb A$}
%                     {$X \vdash \WhtBox A$}}
%
%\put(0, 60){\urule{$(\BlkBox \vdash)$}
%                    {$A \vdash X$}
%                    {$\BlkBox A \vdash \whtb X$}}
%\put(230, 60){\urule{$(\vdash \BlkBox)$}
%                     {$X \vdash \whtb A$}
%                     {$X \vdash \BlkBox A$}}
%
%\put(0, 20){\urule{$(\WhtDia \vdash)$}
%                    {$\whtb A \vdash X$}
%                    {$\WhtDia A \vdash X$}}
%\put(230, 20){\urule{$(\vdash \WhtDia)$}
%                     {$X \vdash A$}
%                     {$\whtb X \vdash \WhtDia A$}}
%\end{picture}
%    \caption{Logical Rules for \Dl{K_{t}}}
%    \label{fig:logical-rules-dkt}
%  \end{center}
%\end{figure}
%
%
\begin{figure}[t]
  \begin{center}
\setlength\unitlength{0.8pt}
\begin{picture}(300, 420)
\thicklines

\put (120, 400) { Display Postulates }

\put (0, 360) { \invrule{(dp)}
                        {$\ast X \vdash Y$}
                        {$\ast Y \vdash X$}    
}      

\put (120, 360) { \invrule{(dp)}
                          {$X \vdash \ast Y$}
                          {$Y \vdash \ast X$}
}      

\put (230,  360) { \invrule{(dp)}
                          {$\ast \ast X \vdash Y$}
                          {$X \vdash Y$}    
}
     
\put (230,  300) { \doubleinvrule{(dp)}
                              {$Z \semic \ast Y \vdash X$}
                              {$Z \vdash X \semic Y$}
                              {$\ast X \semic Z \vdash Y$}
}

\put (120,  300) { \BlkBlobRP }      

\put (0,  300) { \doubleinvrule{(dp)}
                                {$X \vdash Z \semic \ast Y$}
                                {$X \semic Y \vdash Z$}
                                {$Y \vdash \ast X \semic Z$}
}

\put (120, 260) { Sample Structural Rules }

\put(220, 220){\SemicAssLeft}    \put(-10,   220){\SemicAssLeft}

\put (120,  180) { Sample Logical Rules }

\put(230, 140){\brule{$(\ExOr \vdash)$}
                     {$A \vdash  X$}
                     {$B \vdash  X$}
                     {$A \ExOr B \vdash X $}}
\put(0,   140){\urule{$(\vdash \ExOr)$}
                    {$X \vdash A \semic B $}
                    {$X \vdash A \ExOr B $}}

\put(0,   100){\urule{$(\ExAnd \vdash)$}
                    {$A \semic B \vdash X$}
                    {$A \ExAnd B \vdash X$}}
\put(230, 100){\brule{$(\vdash \ExAnd)$}
                     {$X \vdash  A$}
                     {$X \vdash  B$}
                     {$X \vdash A \ExAnd B$}}

\put(0,   60){\urule{$(\WhtBox \vdash)$}
                    {$A \vdash X$}
                    {$\WhtBox A \vdash \blkb X$}}
\put(230, 60){\urule{$(\vdash \WhtBox)$}
                     {$X \vdash \blkb A$}
                     {$X \vdash \WhtBox A$}}

\put(0,   20){\urule{$(\WhtDia \vdash)$}
                    {$\blkb \ast \blkb A \vdash X$}
                    {$\WhtDia A \vdash X$}}
\put(230, 20){\urule{$(\vdash \WhtDia)$}
                     {$X \vdash A$}
                     {$\blkb \ast \blkb X \vdash \WhtDia A$}}
\end{picture}
    \caption{ Sample Rules for \Dl{K_{t}}}
    \label{fig:logical-rules-dkt}
  \end{center}
\end{figure}
\setlength\unitlength{1pt}

Separate structural rules, using only %couched completely in terms of
structural variables like $X$ and $Y$, enforce certain properties
of the structural connectives like associativity (shown in
Figure~\ref{fig:logical-rules-dkt}), commutativity, weakening,
contraction, etc (not shown). 

Finally, in Figure~\ref{fig:logical-rules-dkt} we give a flavour of
the logical rules that introduce the logical constants and the binary
logical connectives into the antecedent and the succedent. Note that
every introduced principal formula is ``displayed''. Space forbids
the inclusion of all the rules for $\Dl{\Kt}$, but see
\cite{wansing-sequent} and \cite{kracht-power}.

%For every logical  logical connective $c$, one rule is always a
%simple ``rewrite'' in which some structural connective in the {\em
  %premise} turns into the logical connective $c$ in the {\em
  %conclusion}, with everything else {\em remaining the same}
%\cite{gore-ggg-srs}. For example, in the rule $(\ExAnd \vdash)$, the
%structural connective $\semic$ turns into the logical connective
%$\ExAnd$, while in the rule $(\vdash \ExOr)$, the structural
%connective $\semic$ turns into the logical connective $\InOr$.

Thus the logical connectives come in pairs, with each component of a
pair captured by the same structural connective, but in different
(antecedent or succedent) positions. Unlike in
traditional Gentzen systems, antecedent and succedent positions do not
correspond exactly to left hand and right hand sides of sequents.

The display postulates
allow us to dis-assemble and re-assemble any structure
bigger than a formula so that any particular part of the structure can
be made the whole of the antecedent, or the whole of the succedent,
depending on its ``polarity''.  The exact side where a particular
occurrence of a substructure finally rests depends upon whether it is
an ``antecedent part'' or a ``succedent part''.  We formalise this as
follows.

In any structure $Z$, the substructure $X$ occurs 
\textbf{negatively} [respectively \textbf{positively}]
if $X$ appears in the scope of an odd number 
[zero or an even number] of $*$ connectives \cite{belnap-display}.
In a sequent $V \vdash W$, a particular occurrence of $X$ is an 
\textbf{antecedent part} [\textbf{succedent part}]
if it occurs positively in the antecedent $V$ 
[positively in the succedent $W$]
or if it occurs negatively in the succedent $W$
[negatively in the antecedent $V$]
\cite{belnap-display}.

Two sequents $s$ and $s'$ are {\bf structurally equivalent} if we can
pass from one to the other using only the display
postulates shown above.  The name Display Logic comes from the
following theorem (which does not hold for subformulae!).

\begin{theorem}[Belnap]
  For every sequent $s$ and every antecedent/succedent part $X$ of
  $s$, there is a structurally equivalent sequent $s'$ that has $X$
  (alone) as its antecedent/succedent. $X$ is said to be ``displayed''
  in $s'$ \cite{belnap-display}.
\end{theorem}

\begin{proof} 
  By inspection of the display postulates.
\end{proof}

\begin{example}
  The following derivation, read upwards, shows how to display the
  (succedent part) $B$ in the sequent 
  $\ast (\ast A \semic B) \semic C \vdash D$
  as the whole of the succedent in 
  $A \semic (C \semic \ast D) \vdash B$.
  %The annotations at the right name the rule used:
\vspace{-3ex}
\[{
\bpf
\A ; "$A \semic (C \semic \ast D) \vdash B$" 
\U ; "$C  \semic \ast D \vdash \ast A \semic B$" "(dp)"
\U ; "$C \vdash (\ast A \semic B) \semic D$" "(dp)"
\U ; "$\ast (\ast A \semic B) \semic C \vdash D$" "(dp)"
\epf
}\]
\end{example}

\begin{lemma}\label{lemma:id-lifted}
  For any formula $A$, the sequent $A \vdash A$ is provable. 
\end{lemma}


\begin{proof}
  By induction on the formation of $A$.
\end{proof}

The beauty of Display Logic is the following generic cut-elimination
theorem.
\begin{theorem}[cut-elimination]
  If there is a proof of the sequent $X \vdash Y$, then there is a
  cut-free proof of $X \vdash Y$ (in the same display calculus)
  \cite{belnap-display}.
\end{theorem}

%\bigskip

\begin{proof}
  The rules must obey Belnap's conditions C1--C8 \cite{belnap-display}.
\end{proof}

\input{jeddefs}

%\section{Display Logic}
%\input{dl}
%\section{Classical Modal Display Logic}
%\input{cmdl}
\section{Isabelle} \label{Isabelle}
\input{isa}
\section{Capturing Display Logics Using Isabelle} \label{dlisa}
\input{dlisa}
\section{Further Axioms as Structural Rules} \label{faxsr} 
\input{faxsr}
\section{Automatic Cut-Elimination} \label{ace}
\input{ace}
%\section{Automating Proof Search}
%\input{auto}
\section{Further Work and Conclusions} \label{fwconcl}
\input{fwconcl}



%\bibliographystyle{alpha}
%\bibliography{isa,atp,misc,mtl,verif,logic,lp,dl,bern,modeq_lit,modal,relevant}
\input{bib}

\end{document}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
