\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: