%%
%%
\documentclass{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

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

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

\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{A Mechanised Proof System for Relation Algebra using Display Logic}
\author{Jeremy E. Dawson
\thanks{Supported by the Defence Science and Technology Organization}
\and Rajeev Gor\'e 
\thanks{Supported by an Australian Research Council QEII Fellowship}}
\institute{Department of Computer Science and
Automated Reasoning Project, \\ 
Australian National University,
Canberra ACT 0200, Australia \\ 
\texttt{jeremy@arp.anu.edu.au}, \ \ 
\texttt{rpg@arp.anu.edu.au}
%\\[1ex]
%Tel: +61-2-6249-5138 \ \ Fax: +61-2-6249-0010
}

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

\begin{document}

%% Title 
\maketitle

\begin{abstract}
We describe an implementation of the Display Logic calculus
for relation algebra as an Isabelle theory.
Our implementation is the first mechanisation of
any display calculus.
%but also provides a useful interactive proof assistant for relation algebra.
The inference rules of Display Logic are coded directly as Isabelle theorems,
thereby guaranteeing the correctness of all derivations.
Our implementation %is the first mechanisation of any display calculus, and
generalises easily to handle other display calculi. It also
provides a useful interactive proof assistant for relation algebras.

\comment{
This serves as a first case study of the implementation of
any Display Logic calculus.
The implementation
also provides a proof assistant for relation algebra in which 
relation algebra axioms are used directly on top of 
the Isabelle metalogic.
This guarantees the soundness of results derived.
Isabelle's metalogic allows both theorems and inference rules of 
Display Logic to be represented as Isabelle theorems.
}
We describe 
various tactics and derived rules developed for simplifying proof search,
including an automatic cut-elimination procedure,
and example theorems proved using Isabelle.
We show how some relation algebraic
theorems proved using our system
can be put in the form of structural rules of Display Logic,
facilitating later re-use.
We then show how the implementation can be used to prove results comparing
alternative formalizations of relation algebra
from a proof-theoretic perspective.
\\[1ex]
Keywords: proof systems for relation algebra, 
non-classical logics, automated deduction, 
display logic, description logics
\end{abstract}

\sloppy 

%\newpage

%% Here begins the main text

\input{intro}
\input{ra}
\input{raisa}

\section{Results from the \dRA\ implementation}
\input{thms}

\input{other}

\section{Conclusion}
\input{concl}
% \vspace{2ex}
% \textbf{Acknowledgement}.  The first author wishes to thank 
% the Australian
% Defence Science and Technology Organization for support during the
% period when the work described in this paper was done.
% The second author is supported by the Australian Research Council 
% via a Queen Elizabeth II Fellowship.
\comment{
} %endcomment
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

\newpage
\input{bib}

\end{document}