%%
%%
\documentclass[a4paper,11pt]{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

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

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\title{Embedding Display Calculi into Logical Frameworks}
\author{Jeremy E. Dawson
\thanks{Supported by an Australian Research Council Small Research Grant.}
\and Rajeev Gor\'e 
\thanks{Supported by an Australian Research Council Queen Elizabeth II 
Fellowship.}}
% \institute{Department of Computer Science and
% Automated Reasoning Group, 
% Computer Sciences Laboratory, \\ 
% Australian National University,
% Canberra ACT 0200, Australia \\ 
% \texttt{jeremy@csl.anu.edu.au} \ \ 
% \texttt{rpg@csl.anu.edu.au}
%\\[1ex]
%Tel: +61-2-6249-5138 \ \ Fax: +61-2-6249-0010
% }
\institute{
\begin{tabular*}{0.8\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
Formal Methods Group & Automated Reasoning Group      \\ 
Dept.\ of Computer Science & Computer Sciences Laboratory   \\ 
Fac.\ of Eng.\ and Inf.\ Tech. & Res.\ Sch.\ of Inf.\ Sci.\ and Eng.\ \\ 
\end{tabular*}\\
    Australian National University \\
\begin{tabular*}{0.8\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
\texttt{jeremy@csl.anu.edu.au} & \texttt{rpg@csl.anu.edu.au}
\end{tabular*}
}


\date{\today}

\newcommand\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 
\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}
\newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}}
\newcommand\NRA{\textbf{NRA}}
\newcommand\RA{\textbf{RA}}
%\newcommand\M{$\mathcal M$}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\1{\textbf 1}
\newcommand\0{\textbf 0}

% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{plain}
\raggedbottom

\begin{document}

%% Title 
\maketitle

\begin{abstract}
We compare several methods of implementing the display (sequent) calculus
\dRA\ for relation algebra in the logical frameworks Isabelle and Twelf.
We aim for an implementation enabling us to formalise
within the logical framework 
proof-theoretic results such as the cut-elimination theorem for \dRA\,
and any associated increase in proof length.
We discuss issues arising from this requirement.
%
%We then show how the implementation can be used to prove results comparing
%alternative formalisations of relation algebra
%from a proof-theoretic perspective.
\\[1ex]
\textbf{Keywords:} logical frameworks, higher-order logics,
proof systems for relation algebra, 
non-classical logics, automated deduction, 
display logic.
\end{abstract}

\sloppy 

%\newpage

%% Here begins the main text


\section{Introduction}

Relation algebras \cite{maddux-introductory}
are extensions of Boolean algebras;
whereas Boolean algebras model subsets of a given set,
relation algebras model binary relations on a given set.
Thus relation algebras have operations such as
relational composition and relational converse.
As each relation is itself a set (of ordered pairs),
relation algebras also have the Boolean operations such as intersection
(conjunction) and complement (negation).
Relation algebras form the basis of relational databases 
\cite{elmasri-navathe-database}
and of the specification and proof of correctness of programs.

Display Logic \cite{belnap-display} is a generalised sequent framework
for non-classical logics,
based on the Gentzen sequent calculus \cite{gallier-logic}.
%It can be applied to give syntactic proof systems for various logics.
Its advantages include a generic cut-elimination theorem, which
applies whenever the rules for the display calculus satisfy certain,
easily checked, conditions.
It is an extremely general logical formalism, applicable to many
(classical and non-classical) logics
in a uniform way \cite{gore-sld-igpl}, \cite{wansing-displaying-modal-logic}.
The generality of the display framework means that essentially the same
meta-level proofs work for many different logics.
A rigorous mechanical
formalisation of such proofs is then widely applicable and worth
pursuing.
In this paper we discuss the implementation of \dRA, a display calculus
for relation algebras, as a case study for exploring various methods for such a
mechanical formalisation of display calculi in general.
\comment{
Display calculi resemble the Gentzen sequent calculus \textbf{LK},
but with significant differences.
For example, the rules for introducing the connective `$\lor$'
(on the right) in \textbf{LK} and some display calculi are
\label{|-v}
$$\frac {\Gamma \vdash \Delta, P, Q}
{\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor )
\qquad \textrm{ and } \qquad
\frac {X \vdash P , Q}
{ X \vdash P \lor Q}(\mbox{DC-}\vdash \lor )
$$
Whereas, in \textbf{LK},
$\Gamma$ and $\Delta$ denote comma-separated lists of formulae,
in a display calculus, $X$ denotes a \emph{structure},
which can involve several \emph{structural} connectives (one of which is `,').
A structure can be either a \emph{formula} (such as $P$ or $P \lor Q$)
or the result of a
structure operator acting on smaller structure(s) (such as $P , Q$).
Display calculi extend the Gentzen calculus with extra structural connectives,
such as `*' (meaning negation) and, for \dRA, operators with relational
meanings.
}

Display calculi extend Gentzen's language of sequents with extra, complex,
$n$-ary structural connectives, in addition to Gentzen's sole 
structural connective, the ``comma''.
\comment{
Whereas Gentzen assumed the comma to be associative, commutative and inherently
poly-valent, display calculi make no such implicit assumptions.
Properties such as these are explicitly stated as structural rules.
For example, \dRA-sequents are built using a binary comma, a binary semicolon,
and unary $*$ and $\bullet$ structural connectives.
Thus, whereas Gentzen's sequents $\Gamma \vdash \Delta$ assume that 
$\Gamma$ and $\Delta$ are comma-separated lists of formulae,
\dRA-sequents $X \vdash Y$ assume that 
$X$ and $Y$ are complex tree-like structures built from formulae
together with comma, semicolon, $*$ and $\bullet$.

The defining feature of display calculi is that in all logical introduction
rules, the principal formula is always ``displayed'' as the whole of the
right-hand or left-hand side.  
For example, the rule $(\mbox{\textbf{LK}-}\vdash \lor )$, shown below left,
is typical of Gentzen's sequent calculi like \textbf{LK}, while the rule
$(\mbox{\dRA-}\vdash \lor )$ shown on the right is typical of display calculi:
$$\frac {\Gamma \vdash \Delta, P, Q}
{\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor )
\qquad  \qquad
\frac {X \vdash P , Q}
{ X \vdash P \lor Q}(\mbox{\dRA-}\vdash \lor )
$$
Intuitively, to use this display calculus rule
downwards on a sequent $X' \vdash Y'$,
everything other than $(P,Q)$
%that ``belongs on the right of $\vdash$''
must be moved into the complex structure $X$ on the left of $\vdash$,
thereby displaying the structure $(P,Q)$ as the whole of the
right-hand side.  There are rules which always enable this to be done.
After the rule application we can ``undisplay'' the moved material
back to its original position, so that the sole purpose of this rule
is to ``rewrite'' some $(P,Q)$ to $P \lor Q$ somewhere inside $Y'$.  }
Their defining feature is that in all logical introduction rules, the
principal formula is always ``displayed'' as the whole of the
right-hand or left-hand side.  There are rules (the ``display
postulates'') which always enable a given structures to be displayed, as
required for using the logical introduction rules.  See
\cite{gore-relalg} for a full account.

Isabelle is an automated proof assistant \cite{isabelle-ref}.
Its meta-logic is an intuitionistic typed higher-order logic,
% and typed $\lambda$-calculus,
sufficient to support the built-in inference steps of 
higher-order unification and term rewriting.
Isabelle accepts inference rules of the form
``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''
where the $\alpha_i$ and $\beta$ 
are expressions of the Isabelle meta-logic,
or are expressions using a new syntax, defined by the user, for some
``object logic'' $\mathcal F$.
An Isabelle user can encode a particular calculus
$\mathcal C _L$ for some object logic $\mathcal L$ using
these rule templates by encoding the set of inference rules for 
$\mathcal C _L$.
%This is supplemented with the user's choice of 
%object logic in which to perform proofs.
For example, if $\mathcal C _L$
is a natural deduction calculus, then 
the $\alpha_i$ and $\beta$ will be formulae of $L$,
whereas if $\mathcal C _L$ is a sequent calculus, then 
the $\alpha_i$ and $\beta$ will be sequents of $\mathcal C _L$.
Such an encoding is called an ``object logic'', even though it is 
a (typically natural deduction or sequent) \emph{calculus} for some
particular logic $L$.
In practice most users would build on one of the
comprehensive ``object logics'' already supplied \cite{isabelle-object}.

Twelf \cite{pfennig-schurmann-twelf} is an implementation of the 
Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework},  
which is based on a typed $\lambda$-calculus with dependent types.
Logics are represented using a \emph{judgements as types} principle,
where each judgement 
of the form $\Gamma, x : Q \vdash y : P$
is identified with the types of its proofs.
Twelf also accepts inference rules of the form
``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$'',
But now, the rule is expressed as the declaration of a 
$\lambda$-calculus term of type
$\alpha_1 \to \alpha_2 \to \ldots \to \alpha_n \to \beta$.
Once again, if the calculus we are trying to capture is a natural deduction
calculus, then the $\alpha_i$ and $\beta$ will be formulae (types), 
but if the calculus is a sequent
calculus, then the $\alpha_i$ and $\beta$ will be sequents (types). 

In an earlier paper \cite{dawson-gore-dra-jelia98},
we described the Isabelle implementation of \dRA,
a display calculus for relation algebra \cite{gore-relalg},
as an object logic for Isabelle.
In that paper we described how we had
used the implementation to prove results comparing
alternative formalisations of relation algebra
from a proof-theoretic perspective.
However we had not proved those results themselves \emph{in} Isabelle.
\comment{
in the sense we now explain.

Suppose we have a logic $L$ (in the sense of
%, a set of well-formed formulae, and a subset of these, the theorems),
a set of formulae which we regard as valid with respect to some semantics)
and two calculi $\mathcal P$ and $\mathcal Q$ for $L$ 
(each consisting of axioms and inference rules).
Further suppose that we have mechanical implementations of 
$\mathcal P$ and $\mathcal Q$.
Then one can use the implementation of 
$\mathcal P$ to derive in $\mathcal P$ every axiom and rule of $\mathcal Q$.
One could then go outside the mechanical system and argue
(by induction on the size, or on the structure, of a $\mathcal Q$-derivation) 
that therefore every $\mathcal Q$-derivable object
(typically a formula or sequent) is also 
$\mathcal P$-derivable.

The results referred to in \cite{dawson-gore-dra-jelia98}
were proved in this manner.
An alternative and, when one's aim is the mechanical proof of
proof-theoretical results, better, approach would be one which enabled
the inductive argument above to be carried out in the mechanical
theorem-prover.
This would require a different style of implementation of the 
calculi $\mathcal P$ and $\mathcal Q$
in the prover, so as to enable reasoning about 
the shape and form of
$\mathcal P$-derivations and $\mathcal Q$-derivations.
Typically this would require modelling, in the theorem prover,
the ``tree'' of steps
used in a derivation and the fact that each step is an instance of a rule
of the calculus
$\mathcal P$ or $\mathcal Q$;
this in turn requires modelling the form of 
the statement of an inference rule of $\mathcal P$ or $\mathcal Q$,
and a method of obtaining particular substitutional instances of such 
rules of inference.
%and substitution of a term for a variable in it.
The terms ``shallow embedding'' and ``deep embedding'' 
are often used to distinguish these styles of implementation
\cite{boulton-et-al-hdl}.
}
%
In this paper we describe work done
so far towards such a ``deep embedding'' of \dRA.  
We explored the possibility of implementation in Twelf, Isabelle/CTT
and Isabelle/HOL.
In the subsequent sections we describe 
% the original Isabelle/Pure implementation and 
this further work.







\section{The Isabelle/Pure implementation} \label{pure}

\comment{
Isabelle is an interactive computer-based proof system,
described in \cite{isabelle-ref}.
Its capabilities include higher-order unification and 
term rewriting.
It is written in Standard ML \cite{ML-definition};
when it is running, the user can interact with it by
entering further ML commands, and can program complex proof sequences in ML.
As stated previously, the basic Isabelle constructs 
available to a user include inference rule templates of the form 
``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''.
These can be used ``forwards'', to obtain $\beta$ from the $\alpha_i$,
or ``backwards'', to reduce a given goal $\beta$ to subgoals 
$\alpha_1, \alpha_2, \ldots, \alpha_n$.
Isabelle provides a number of basic operations for
backwards proof and proof-search
(\emph{tactics}\index{tactic|textbf}), as well as 
\emph{tacticals}\index{tactical|textbf}
for combining these.
%Isabelle automatically keeps track of the subgoals generated by this backward
%search procedure and the user can choose to work on any subgoal.
%The user can also write complex proof tactics in ML;
%many complex tactics and tacticals are supplied with
%Isabelle or its standard object logics.
Isabelle also supports forward proof.

The inference rules collectively form a simple meta-logic:
an intuitionistic typed higher-order logic.
%typed $\lambda$-calculus.
There are three logical operators: 
\texttt{==>} (implication, or deducibility),
\texttt{==} (equality, or substitutability), and
\texttt{!!} (universal quantification).
For example, 
\mbox{\texttt{[| A1; A2 |]~==>~B}},
which is an abbreviation for 
\texttt{A1 ==> (A2 ==> B)},
is the Isabelle representation for 
``from $\alpha_1, \alpha_2, \mbox{ infer } \beta$''.
These operators satisfy certain properties arising from their intended meanings.
For example, since %the Isabelle proposition
\mbox{\texttt{[| A1; A2 |]~==>~B}}
means that $\beta$ can be deduced from 
$\alpha_1$ and $\alpha_2$,
% and can be proved by deducing $\beta$
% from $\alpha_1$ and $\alpha_2$,
% we have that
% \mbox{\texttt{[|~(A~==>~B);~A~|] ==> B},}
% and that
it should also be possible to deduce 
$\beta$ from $\alpha_2$ and $\alpha_1$.
Indeed, using Isabelle, we can prove a new rule, shown below, that states
``if (from $\alpha_1, \alpha_2, \mbox{ infer } \beta$) is a rule,
then (from $\alpha_2, \alpha_1, \mbox{ infer } \beta$) is a rule''.
{\par\noindent\centering
\texttt{[| [| A1; A2 |] ==> B |] ==>
([| A2; A1 |] ==> B)}.
\par\noindent}
That is, \texttt{==>} can be seen as the analogue of the horizontal bar
used to state rules in a natural deduction system, in which the order of
premises is not significant.
Likewise, since 
\texttt{A == B}
means that \texttt{A} can be replaced by \texttt{B}, or vice versa,
\texttt{==} is reflexive, symmetric and transitive.

This meta-logic is known as Isabelle's \texttt{Pure} theory.
Mostly the user would augment this by defining 
additional constants to capture the syntax of the object logic.
For example, to capture set theory, we would add a constant \texttt{mem}
(say) to stand for the $\in$ symbol, while sequents would require  
constants `\texttt{|-}' and `\texttt{,}'.
% an object logic containing operators and inference rules;
% these would usually include all the usual logical operators 
% and inference rules,
% and often much more, such as operators and rules for set theory.
Several such object logics are packaged with the Isabelle distribution 
\cite{isabelle-object}.
Once these syntactic elements of the object logic are in place, we can build
object-logic expressions into the $\alpha_i$ and $\beta$.
For example, in \dRA, the $(\vdash \lor)$ rule uses the 
meta-logical operator \texttt{==>} discussed above,
and could be entered as \texttt{"[| \$X |- P, Q |] ==> \$X |- P v Q"}.
(The \texttt{\$} distinguishes \dRA-structures such as \texttt{X}
from \dRA-formulae such as \texttt{P}.)
This rule is an instance of the form 
``from $\alpha \mbox{ infer } \beta$''.

However \dRA\ was implemented in Isabelle directly on top of the
\texttt{Pure} theory,
so that the only
inference rules available are those of \dRA.
%(Thus you can't write $(P \vdash Q) \lor (R \vdash S)$, for example,
%as you could if \dRA\ were built on top of Isabelle/HOL).
As far as the Isabelle meta-logic is concerned, we can think of the atomic
propositions as the formulae of the object-logic.
In this case these are \dRA-sequents of the form $X \vdash Y$, built using
object-logic ``connectives'' 
`$\vdash$', `,', `;', `*', `$\bullet$', `$\land$', `$\lor$', etc.
These can be combined into more complex propositions using the Isabelle
meta-logic connectives \texttt{==>}, \texttt{==} and \texttt{!!}.
Thus each Isabelle proposition 
is either a \dRA\ sequent $X \vdash Y$, or is
made up of sequents combined into inference rules
using the three Isabelle/Pure logical operators. 
It follows that expressions such as
\texttt{X |- (P ==> Q)} or \texttt{A v (B ==> C)}
are not possible.
Note that the $\alpha_i$ and $\beta$ as discussed above would most commonly 
simply be \dRA-sequents, but could be ``complex'' Isabelle propositions.


We may declare axioms and inference rules of the \dRA\ calculus to Isabelle.
For example, the sequent $p \vdash p$ is an initial sequent (axiom) in \dRA;
thus it is declared in Isabelle as a ``rule'', \texttt{P |- P}.
(For a rule with no premises, this notation is used rather than 
\texttt{[| |] ==> P |- P}.)
Similarly, each rule of \dRA\ is declared as an Isabelle rule, as in the
example of the $(\vdash \lor)$ rule above.
These, and further derived sequents and rules, are called Isabelle
``theorems''.
%Isabelle theorems may be object logic formulae or may 
%involve Isabelle's metalogical operators.
Thus, in the Isabelle implementation of \dRA, an Isabelle theorem
may be either a simple sequent of \dRA, 
or a sequent \emph{rule}.
Whereas an initial
sequent of \dRA\ becomes an Isabelle theorem of the form \texttt{X |- Y},
a sequent rule becomes an Isabelle theorem containing also 
the operators \texttt{==>} (implication) or \texttt{==} (equality).
}
In \cite{dawson-gore-dra-jelia98} we described an implementation of \dRA\
 which used Isabelle's  \texttt{Pure} theory,
so that the only inference rules available were those of \dRA.
Thus, in the Isabelle implementation of \dRA, an Isabelle theorem
may be either a simple sequent of \dRA, 
or a sequent \emph{rule}.
Whereas a sequent derivable in 
\dRA\ becomes an Isabelle theorem of the form \texttt{X |- Y},
a sequent rule becomes an Isabelle theorem containing also 
the meta-logical operators \texttt{==>} (implication) or \texttt{==} (equality).

That this is a shallow embedding is reflected in the fact that the 
horizontal bar of sequent rules becomes the Isabelle \texttt{==>} operator.
In a deep embedding, as in Section \ref{hol}, the 
horizontal bar also becomes an object-level constant.
\comment{
% For example, the (cut) rule (shown on \page{id}) appears as
% {\par\noindent\centering
% \texttt{"[| \$?X |- ?A; ?A |- \$?Y |] ==> \$?X |- \$?Y"}
% \par\noindent}
For example, the ($\vdash \lor $) rule (shown in \S\ref{|-v}) appears as
$$\texttt{"\$?X |- ?A, ?B ==> \$?X |- ?A v ?B"}$$
in Isabelle. 
(The `\verb:?:' denotes a variable which can be instantiated,
and the `\verb:$:' denotes a structural variable or constant.)
The variant $A \vdash A$ of the (id) rule (see \S\ref{otm})
appears as \texttt{"?A |- ?A"}.
The bi-directional \texttt{dcp} rule, shown in \fig{sdr},
appears as \texttt{"\$?X |- \$?Y == * \$?Y |- * \$?X"}.
}

In this shallow embedding, access to and manipulation of the shape
of \dRA\ constructs (ie, sequents, structures, formulae)
and derivations was provided only at the ML level.
For example, in \cite{dawson-gore-dra-jelia98}
we described having programmed a procedure
to perform cut-elimination for \dRA.
The input to this was a \dRA\ derivation (represented
as a tree of sequent rule instances),
and the output was a derivation not containing
an instance of the cut rule.  
This required examining the shape of a derivation (represented as a tree
of \dRA\ rule instances) and of the Isabelle terms representing sequents.
While the shape of an Isabelle term is easily accessible (by ML code),
we wrote additional ML code to record a proof in the form of a derivation tree,
so that our procedure could examine its shape.
\comment{
a derivation step is represented as a function;
a complex derivation is the composition of functions representing the 
elementary derivation steps.
Therefore, to look at the shape of a derivation (for example, to ask
what rule was used in the final \dRA\ inference step) involved changing the
Isabelle code somewhat,
so as to record the elementary \dRA\ rules used and to construct
a derivation-tree while a derivation was being performed.
}

What we aim to do (as described later) is to perform the
cut-elimination {\em proof} entirely within a theorem prover, rather
than writing a cut-elimination {\em program} in ML.  We will therefore
need to model derivation trees within the object language of the
theorem prover.  We would also need to model the set of elementary
inference rules of the calculus, so as to be able to say that every
rule in a given derivation tree is an instance of one of the inference
rules in that calculus.

\comment{
In \cite{dawson-gore-dra-jelia98} we also described using the Isabelle 
\dRA\ implementation
to show the soundness of certain other calculi for relation algebra.
In these cases, we in fact showed that all the axioms and 
rules of the other calculi were derivable in \dRA. 
The argument that followed, namely that 
therefore an entire derivation in one of those other calculi could have
been performed in \dRA, was outside the scope of the mechanical
theorem prover. 

Again, doing this within the theorem prover requires modelling the shape of
sequents or formulae of the calculus in question, of derivations, and of
the rules used in them.
Similar work has been done by Mikhajlova and von Wright
for classical first-order logic proof systems
in \cite{mikhajlova-vonwright-isomorphism}.
But note that their work assumes that the second and third
clauses of the definitions given at 
\cite[p.~302]{mikhajlova-vonwright-isomorphism} are sound,
and we suspect one is not.
We are currently trying to show whether their definitions 
are derivable using their previous definitions.
}


\section{Dependent Type Theory implementations}
\subsection{Introduction}

In a dependent type theory, a type may be parametrised over a type
variable {\em and} a term variable.  This, coupled with the
\emph{judgements as types} principle, where a judgement is identified
with the types of its proofs, enables us to express the derivation of
a display calculus derived rule.

\comment{
A simpler situation where the Curry-Howard isomorphism can be seen is
in the simply-typed $\lambda$-calculus and 
a natural deduction calculus \textsf{NDInt}
for intuitionistic propositional logic.
Let $A$ and $B$ be formulae, and $\pi$ be a derivation of $A$ 
in \textsf{NDInt}.
Suppose also that $A \to B$ is derivable
in \textsf{NDInt},
and consider an \textsf{NDInt}-derivation of $A \to B$
%in the Natural Deduction style,
where one assumes $A$ and derives $B$.
That is, it is a derivation of $B$ in which $A$ is regarded as true;
at the points where $A$ is used, it would contain some notation $\xi$ meaning
``true by assumption''.
Let $\rho(\xi)$ be this derivation of $B$.
%where $x$ is a place-holder for some
%notation meaning ``true by assumption'',
%as will appear in the derivation of $B$ wherever $A$ is used. 
So if we substitute $\pi$ (the derivation of $A$) for $\xi$ in $\rho(\xi)$, 
we get a derivation $\rho(\pi)$
of $B$ which does not rely on $A$ as an assumption.

Then, using $\pi : A$ to mean ``$\pi$ is a derivation of $A$'',
we can write the rule

\begin{center}
\slrule { \pi : A \qquad \rho(\xi) : A \to B } { \rho(\pi) : B }
\end{center}

Erasing the annotations $\pi$ $\rho$ and `:' 
gives the well-known $(\to E)$ natural deduction rule for intuitionistic logic;
the rule as it stands also shows how to derive $B$.
As indicated above, we can equally think of $\rho(.)$
as a derivation of $A \to B$
or as a function which takes,
as argument, a derivation of $A$ such as $\pi$, and returns a derivation of $B$.
If we also think of $A$ as the type ``derivations of proposition $A$''
(and similarly for $B$) 
we get the functional type-theory interpretation,
under which $A \to B$ means the type of functions which take an argument
of type $A$ and return a result of type $B$.
(Conveniently, the same symbol `$\to$'
is conventionally used for both purposes.)
}

The Curry-Howard isomorphism, in the simply-typed $\lambda$-calculus,
identifies terms with proofs and types with propositions. So if $A$ is
a type (proposition), and $\pi$ is a term, then $\pi : A$ means
``$\pi$ is a derivation of $A$''.

Dependent types extend what can be done in the simply-typed
$\lambda$-calculus in two distinct ways.  Firstly, consider a type $I$
of individuals, and a parametrised type $A(i)$. That is, for each
individual $i \in I$, there is a type $A(i)$.  Consider a function
$\rho$ whose domain is $I$, such that for each $i \in I$, $\rho(i) \in
A(i)$.  The type of such a function is written $\prod i : I . A(i)$
denoting how the type of $\rho(i)$ \emph{depends} on the \emph{value}
of $i$.

Let $A$ be a predicate, and therefore each $A(i)$ be a proposition
taking the value true or false, and let each $\rho(i)$ be a derivation
of $A(i)$.  That is, $\rho$ is a function which, for each individual
$i$, gives a derivation of $A(i)$; we can think of such a $\rho$ as a
derivation of $\forall i A(i)$.  At the same time, if we think of each
type $A(i)$ as the type ``derivations of proposition $A(i)$'', then
the functions $\rho$ of type $\prod i : I . A(i)$ are the derivations
of $\forall i A(i)$.

Secondly, we install an object-logic at the level of terms so that
formulae of the object-logic become terms of the dependently-typed
$\lambda$-calculus.  That is, we install a syntax for terms using the
connectives of the chosen object logic, and declare a type constructor
$P(.)$, so that for each term $t$, $P(t)$ will mean ``derivation of
formula $t$''.  This was our approach for modelling \dRA\ where
instead of $P(t)$, we used $X \vdash Y$, with $X$ and $Y$ being the
left and right-hand sides of a sequent.

Regarding a formula $t$ as derivable when we have a term of type
$P(t)$ has certain consequences.  For example, since from functions of
type $X \to Z$, $U \to V \to W$ and $S \to S \to T$ we can construct
functions of type $X \to Y \to Z$, $V \to U \to W$ and $S \to T$, we
unavoidably have weakening, exchange and contraction.  However, in our
formulation of \dRA, these are at the meta-logic level, not in the
object logic.

Two theories based on dependent types are the
Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework}
and Constructive Type Theory (CTT) \cite{martin-lof-CTT}.  

\subsection{The Twelf implementation}

Twelf \cite{pfennig-schurmann-twelf} is an implementation of the 
Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework}.  
This is based on a typed $\lambda$-calculus with dependent types.
Twelf is written in Standard ML, and the user can interact with the system
using its ``ML Interface'', but only a very limited range
of functions is available.

Here is an extract of our Twelf source file.

\begin{tabular}{c@{\quad}l}
1 & \texttt{str : type.      } \\
2 & \texttt{|- : str -> str -> type.   \%infix none 10 |-.} \\
3 & \texttt{*  : str -> str.          \%prefix 200 *.} \\
  & \\
4 & \texttt{\% Display postulates } \\
5 & \texttt{sA :    (* X |- Y) -> (* Y |- X).} \\
6 & \texttt{sS :    (X |- * Y) -> (Y |- * X).} \\
  & \\
7 & \texttt{\% Derived structural rules} \\
8 & \texttt{ssASl = [D] sA (sS D).      \% (X |- * * Y) -> (* * X |- Y)} 

\end{tabular}

Line~1 declares 
\texttt{str} as a new type to represent the \dRA\ structures.
Line~2 declares 
\texttt{|-} as a binary type constructor,
taking two \emph{term} arguments of type
\texttt{str} and returning a \emph{type}.
Thus, for structures \texttt{X} and \texttt{Y},
the construct
\texttt{X |- Y} represents derivations of the sequent $X \vdash Y$.
Line~3 declares 
\texttt{*} as a unary structure operator.
Lines 4 and 7 are comments.

In lines 5 and 6 the terms \texttt{sA} and \texttt{sS} (which stand
for ``star in the antecedent'' and ``star in the succedent'') are
declared with the types
%showing that they denote
that represent derivations of the \dRA\ rules
\begin{center}
\slrule { *X \vdash Y } { *Y \vdash X } (\ttdef{sA}) \qquad
\hspace{20mm}
\slrule { X \vdash *Y } { Y \vdash *X } (\ttdef{sS}) \qquad
\end{center}
We can think of these declarations as assertions that there are
derivations called \texttt{sA} and \texttt{sS}) of these rules,
or as defining these as new ``primitive'' one-step rules.

Now, by treating \texttt{sA} and \texttt{sS} as functions that take a
derivation of a sequent to a derivation of another sequent, we can
form their composition for some given sequent $U \vdash * * V$ as
below:
$$
\stackrel {\mbox{derivation of}}{U \vdash * * V} \quad
\stackrel{\texttt{sS}} \longrightarrow \quad
\stackrel {\mbox{derivation of}}{* V \vdash * U} \quad
\stackrel{\texttt{sA}} \longrightarrow \quad
\stackrel {\mbox{derivation of}}{* * U \vdash V} 
$$
The definition of \texttt{ssSAl} does this; the notation means
$\lambda D. \textit{sA} (\textit{sS} \ D)$.
Twelf computes the type of the function \texttt{ssSAl},
giving $(S1 \vdash * * S2) \to (* * S1 \vdash S2)$.
Note that $X, Y, S1$ and $S2$ are variables.


Twelf offers Prolog-like \cite{prolog-standard} queries such as

\texttt{
\_ssASl :        (X1 |- * * Y1) -> (* * X1 |- Y1).}

\noindent
which searches for a term of the specified type (ie, searches for
a derivation of the stated rule)
and instantiates \texttt{\_ssASl} with that term.
In this example, because Twelf allows substituting for 
\texttt{X1} and \texttt{Y1} in the query as well as for the variables
\texttt{X} and \texttt{Y}
in the declarations of \texttt{sA} and \texttt{sS},
the search proceeds along an infinite branch in the wrong direction.

On the other hand, the code 

\begin{verbatim}
% Using the theorem prover
%theorem
ssASl\_th : exists 
  {D:{S1:str} {S2:str} (S1 |- * * S2) -> (* * S1 |- S2)} true.
%prove 2 {} (ssASl\_th D).
\end{verbatim}

\noindent
successfully uses Twelf's theorem prover to find the derivation, returning

\noindent
\texttt{
/ssASl\_th/:  ssASl\_th ([S1:str] [S2:str] [X1:S1 |- * * S2] sA (sS X1)).}

\noindent
(Here the variables \texttt{S1} and \texttt{S2} need to be explicitly
abstracted over -- in the earlier code they were free variables.)
Twelf's theorem prover is not extensively documented.

We found that certain extremely useful aspects of Isabelle are absent
from Twelf.  Isabelle offers a substantial number of user
``commands'', in the form of well-documented ML functions, which
enable the user to programme proof procedures, or to examine the shape
of a term or type expression.  Twelf appears to offer no comparable
capabilities to the user.  Thus, although the theorem prover did
successfully find the derivation above, we felt uncertain that it
would be capable of finding all required derivations, particularly as
it is stated to be under extensive development.

\comment{
At this point we should refer to the proof of a cut-elimination theorem,
using Twelf, described in \cite{pfennig-structural-cut-elimination}.
This uses a rather ingenious representation of sequents; 
a cut-free proof of a traditional Gentzen
sequent $A \vdash B$ is represented as 
the type \texttt{neg A -> pos B -> @}, and
a cut-free proof of it as 
\texttt{neg A -> pos B -> \#}.
The two rules shown below left
are represented as the type shown on the right:
\begin{center}
\slrule {\Gamma, A \vdash \Delta} {\Gamma, A \& B \vdash \Delta}
\quad
\slrule { A \vdash } { A \& B \vdash }
\quad
\texttt{(neg A -> \#) -> (neg (A and B) -> \#)}
\end{center}
In fact, the second rule shown would be directly represented by
the type shown, 
but the first rule shown would be directly represented by
\begin{center}
\texttt{(neg $\Gamma$ -> pos $\Delta$ -> neg A -> \#) -> \qquad \mbox{}\\ 
  (neg $\Gamma$ -> pos $\Delta$ -> neg (A and B) -> \#)}
\end{center}
However the existence of a term (function) of the type shown first 
trivially implies the existence of a term (function) of the type
shown second.
Further constructed types represent stages of the transformation of
a proof into a cut-free proof, and a termination checker checks that the
function performing the entire transformation from a proof to a cut-free proof
terminates.  
However, this termination checker only checks that the function 
would not run forever.
It does not check that it terminates with a cut-free derivation --
it does not complain if the code is run with some cases deleted.

This work on the cut-elimination theorem is 
based on an ingenious way of representing the problem in a way that fits into
Twelf;
even so, getting a proof of the cut-elimination theorem from it relies on 
the heuristically-based termination checker and upon a manual check that
all possible cases for the rules used just above the ``cut''
have been covered.
On the other hand, the Twelf type-checker proves that each individual step
is correct, in that the changed derivation in fact does derive
the sequent which it purports to derive.

Thus this proof of cut-elimination lies between our previous work
(where we just programmed a cut-elimination function in ML)
and a fully formal proof.
}



\subsection{The Isabelle/CTT implementation}

We then turned to the \texttt{CTT} theory of Isabelle, since 
it is based on a logic which is very similar to 
that of Twelf, in that it includes dependent types.

We implemented \dRA\ similarly to its implementation in Twelf, 
so that we had, for example, (omitting premises of the from
\texttt{?X : str}, which were fairly ubiquitous)

\texttt{
"sA : * ?X |- ?Y --> * ?Y |- ?X" : thm \\
\indent "sA oo sS : ?X |- * * ?Y --> * * ?X |- ?Y" : thm
}

\noindent
where \texttt{oo} denotes function composition.  We wrote tactics to
determine the type of a term variable \texttt{?t} by solving a goal
such as \texttt{sA oo sS : ?t}, corresponding to the derived rule
obtained by the given combination of these rules.  We explored tactics
to search for a term (i.e.\ proof) of a given type (i.e.\ sequent), by
solving a goal such as the one below, which contains the term variable
\texttt{?P}.

\texttt{"?P : ( X |- * * Y) --> ( * * X |- Y)"}.

The \texttt{CTT} theory of Isabelle is not extensively developed so we
found it necessary to prove some fairly elementary though general
theorems.

%\subsection{Dependent type theory -- conclusions}
\subsection{Conclusions}

We experimented with Twelf because we thought we could get our hands
on the proofs ``for free''. That is, in the course of deriving a
sequent or sequent rule, we produce a term which embodies the
derivation performed.  Given our intention to do a fully mechanised
proof of the cut-elimination theorem (in which we manipulate
derivations extensively) it had seemed that this feature of Twelf
would be useful.  Our work with Isabelle/CTT seemed to indicate that
the same things could be done in it as in Twelf (with some effort to
produce appropriate derived rules and tactics).

However we realised that although we could produce a term which
represented the derivation and showed the elementary steps from which
it is composed, we could not analyse derivations, \emph{in the logic
  of the theorem prover}, in the required ways: for example, to ask
which rule was used in the final step of the derivation.  In the light
of this, there seemed to be no benefit in pursuing an implementation
using dependent type theory.

%We have referred to a proof in Twelf of the sequent calculus 
%cut-elimination theorem, noting that it was based on
%an ingenious way of representing the problem in a way that fits into
%Twelf, and that it was not a fully formal proof.
%Since we are aiming for a fully formal proof, using techniques which
%would be applicable equally to other proof-theoretic results,
%we felt that this cut-elimination proof does not indicate that
%dependent type theory would be powerful enough for our needs.




\section{The Isabelle/HOL implementation} \label{hol}

\texttt{HOL} is an Isabelle theory based on the higher-order logic of
Church \cite{church-types} and the HOL system of Gordon
\cite{HOL-introduction}.  Thus it includes quantification and
abstraction over higher-order functions and predicates.  The
\texttt{HOL} theory uses Isabelle's own type system and function
application and abstraction: that is, object-level types and functions
are identified with meta-level types and functions.  Isabelle/HOL
contains constructs found in functional programming languages (such as
\texttt{datatype} and \texttt{let}) which greatly facilitates
re-implementing a program in Isabelle/HOL, and then reasoning about
it.  However limitations (not found in, say, Standard ML itself)
prevent defining types which are empty or which are not sets, or
functions which may not terminate.

The work of embedding \dRA\ in Isabelle/HOL is still underway.
However it is clear at this stage that the facility for \texttt{datatype}
type declarations and associated primitive recursive function definitions
is of enormous help.
For example, we model \dRA\ structure expressions (see
\cite{gore-relalg}) as below:
\begin{verbatim} 
datatype structr = Comma structr structr
                 | SemiC structr structr
                 | Star structr
                 | Blob structr
                 | I
                 | E
                 | Structform formula
                 | SV string
\end{verbatim} 
The first six lines correspond to the structure operators of \dRA\ and
the next line is for ``casting'' a \dRA\ formula into a \dRA\ 
structure.  The last line had no analogue in the shallow embedding,
where an Isabelle variable such as \texttt{?S} referred to any
\dRA-structure.  In the deep embedding, \texttt{SV ``X''} will refer
to the variable named \texttt{X} appearing in (say) the statement of a
rule.  We therefore need to define Isabelle/HOL functions which (for
example) find all the variables in a structure expression, or
substitute a given structure for such a variable. (We wrote such
functions for the work described in Section \ref{pure}, but in
Standard ML, not in Isabelle.)

On the other hand, when writing Isabelle tactics which involve
analysing the shape of a rule, we can write (for example) 
\texttt{(SV Comma ?V ?S)} 
to match any structure expression consisting of two
substructures joined by the comma operator of which the first must be
a variable.  This matching and any related substitution is performed
by Isabelle.

For describing the structure of a derivation we have
\begin{verbatim} 
datatype pftree = Pr rule (pftree list)
                | Unf sequent
\end{verbatim} 
where \texttt{Pr r pts} is a derivation whose last step uses a \dRA\ rule 
whose instantiation is \texttt{r},
and the premises of that last step are the conclusions of the 
derivations in the list \texttt{pts}.
\texttt{Unf} (``unfinished'') means that a leaf is a sequent which is not
an axiom, so is an assumption (or a ``premise'' of the derivation tree as a
whole).
We define functions which check that such a structure is a valid
derivation (for example, that the premises of a rule really are the
conclusions of the trees above, and that each step uses a valid rule 
and instantiates it correctly).
For example, to list the ``premises'' of the whole derivation tree,
\begin{verbatim} 
primrec
  "premsPT (Unf seq) = [seq]"
  "premsPT (Pr rule pts) = premsPTs pts"

  "premsPTs [] = []"
  "premsPTs (pt # pts) = premsPT pt @ premsPTs pts"
\end{verbatim} 


Each datatype declaration generates a number of theorems
which are made available for proofs, and of which some are installed
in rule sets used by the more automated proof tactics.
These theorems include ones expressing that a \texttt{datatype} type
is a disjoint union and that the constructors are 1-1 functions,
and one expressing a structural induction principle. 

As noted above, this work is still in progress.  We still need to
specify and reason about derivability and derivation trees; for
example, we need to express the requirement that each step of a
derivation uses a \dRA\ rule {\em instance} of a \dRA\ rule found in a
given set.  It appears at this stage that the Isabelle/HOL logic is
well-equipped for writing specifications which imitate a program
written in functional programming style, and for reasoning about the
behaviour of that program; Isabelle/HOL seems to offer the
capabilities we will require.


\section{Conclusion}

We have reviewed earlier work in which a shallow embedding of the \dRA\
calculus into the Isabelle/Pure logic, and noted its drawbacks for 
proving proof-theoretic results in Isabelle itself.
Attracted by the notion that the tools based on dependent type theory 
would give expressiveness about proofs ``for free'', we then looked at
the Twelf tool. 
While the Twelf tool is still under active development,
we noted how a similar logic is available in Isabelle/CTT, which
offers the advantages of Isabelle, such as access to a wide 
range of documented ML functions for programming proof tactics.
However we also found that, while Twelf and Isabelle/CTT facilitate 
identifying the derivation of a sequent or derived rule,
they do not facilitate reasoning about the shape of that derivation,
or of the sequents found in it.
Thus we turned to Isabelle/HOL, which appears to offer the best facility 
for deep embedding of a logic such as \dRA, and reasoning about derivability,
derivation trees and the associated concepts we will need.
Needless to say, this was the advice we received from Larry Paulson from the
start.


% \vspace{2ex}
% \textbf{Acknowledgement}.  
% The second author is supported by the Australian Research Council 
% via a Queen Elizabeth II Fellowship.
\comment{
} %endcomment
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

%\bibliography{./awcl,/home/arp/disk1/rpg/bib/fm,/home/arp/disk1/rpg/bib/modal,/home/arp/disk1/rpg/bib/mtl,/home/arp/disk1/rpg/bib/logic,/home/arp/disk1/rpg/bib/tl,/home/arp/disk1/rpg/bib/paracon,/home/arp/disk1/rpg/bib/linear,/home/arp/disk1/rpg/bib/algebra,/home/arp/disk1/rpg/bib/relevant,/home/arp/disk1/rpg/bib/dl}

%\bibliographystyle{plain}

\begin{thebibliography}{10}

\bibitem{belnap-display}
N~D {Belnap}.
\newblock Display logic.
\newblock {\em Journal of Philosophical Logic}, 11:375--417, 1982.

\bibitem{boulton-et-al-hdl}
Boulton, Gordon, Gordon, Harrison, Herbert, and van Tassel.
\newblock Experience with embedding hardware description languages in hol.
\newblock In {\em Proceedings of IFIP TC10/WG 10.2, International Conference on
  Theorem Provers in Circuit Design: Theory, Practice and Experience}, pages
  129--156. North-Holland/Elsevier, 1992.

\bibitem{church-types}
Alonzo Church.
\newblock A formulation of the simple theory of types.
\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.

\bibitem{dawson-gore-dra-jelia98}
J~Dawson and R~Gor{\'{e}}.
\newblock A mechanised proof system for relation algebra using display logic.
\newblock In {\em JELIA98:}, LNAI 1489:264--278. Springer, 1998.

\bibitem{prolog-standard}
P~Deransart, A~Ed-Dbali, and L~Cervoni.
\newblock {\em Prolog: The Standard}.
\newblock Springer-Verlag, 1996.

\bibitem{elmasri-navathe-database}
Ramez~A Elmasri and Shamkant~B Navathe.
\newblock {\em Fundamentals of Database Systems}.
\newblock Benjamin/Cummings, Redwood City, 2 edition, 1994.

\bibitem{gallier-logic}
J.~H. Gallier.
\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
  Proving}.
\newblock John Wiley and Sons, 1987.

\bibitem{HOL-introduction}
M~J~C Gordon and T~F Melham.
\newblock {\em Introduction to HOL: a Theorem Proving Environment for Higher
  Order Logic}.
\newblock Cambridge University Press, 1993.

\bibitem{gore-relalg}
R~Gor{\'{e}}.
\newblock Cut-free display calculi for relation algebras.
\newblock In CSL96: LNCS 1258:198--210. Springer, 1997.

\bibitem{gore-sld-igpl}
R~Gor{\'{e}}.
\newblock Substructural logics on display.
\newblock {\em Logic Journal of the Interest Group in Pure and Applied Logic},
  6(3):451--504, 1998.

\bibitem{harper-honsell-plotkin-framework}
Robert Harper, Furio Honsell, and Gordon Plotkin.
\newblock A framework for defining logics.
\newblock {\em Journal of the ACM}, 40:143--184, 1993.

\bibitem{maddux-introductory}
R~D Maddux.
\newblock Introductory course on relation algebras, finite-dimensional
  cylindric algebras, and their interconnections.
\newblock In H.~Andreka, J.~D. Monk, and I.~Nemeti, editors, {\em Algebraic
  Logic}, volume~54 of {\em Colloquia Mathematica Societatis Janos Bolyai},
  pages 361--392. North-Holland, Amsterdam, 1991.

\bibitem{martin-lof-CTT}
Per Martin-L\"{o}f.
\newblock {\em Intuitionistic Type Theory}.
\newblock Bibliopolis, 1984.

\bibitem{mikhajlova-vonwright-isomorphism}
Anna Mikhajlova and Joakim von Wright.
\newblock Proving isomorphism of first-order proof systems in hol.
\newblock In TPHOLS98, LNCS 1479:295--314. Springer, 1998.

\bibitem{ML-definition}
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen.
\newblock {\em The Definition of Standard ML (Revised)}.
\newblock The MIT Press, 1997.

\bibitem{isabelle-ref}
Lawrence~C Paulson.
\newblock {\em The Isabelle Reference Manual}.
\newblock Computer Laboratory, University of Cambridge, 1995.

\bibitem{isabelle-object}
Lawrence~C Paulson.
\newblock {\em Isabelle's Object-Logics}.
\newblock Computer Laboratory, University of Cambridge, 1995.

\bibitem{pfennig-structural-cut-elimination}
Frank Pfennig.
\newblock Structural cut elimination.
\newblock In Proc.\ LICS95, pages 156--166. IEEE Computer Society Press,
  1995.

\bibitem{pfennig-schurmann-twelf}
Frank Pfennig and Carsten Sch\"{u}rmann.
\newblock System description: Twelf - a meta-logical framework for deductive
  systems.
\newblock In CADE-16, LNAI 1632:202--206.
  Springer, 1999.

\bibitem{wansing-displaying-modal-logic}
Heinrich Wansing.
\newblock {\em Displaying Modal Logic}, volume~3 of {\em TRENDS IN LOGIC}.
\newblock Kluwer Academic Publishers, Dordrecht, August 1998.

\end{thebibliography}

\end{document}




