report.tex

\documentclass[]{article}

\title{Properties of Deep Inference \\ 24 Month Progress Report}

\author{Tom Gundersen}

\begin{document}

\maketitle

\section{Overview of the work}

We study normalisation for propositional classical logic.

We present normalisation techniques which, contrary to our expectations,
\begin{itemize}
\item do not involve logical connectives or logical inference rules and
\item do not involve any permutations and hence are largely syntax independent.
\end{itemize}

The novelty of our work is the introduction of \emph{atomic flows}. The atomic flow of a derivation, $\Phi$, is a graph obtained by tracing the atom occurences in $\Phi$. An atomic flow contains no information about logical connectives nor about logical inference rules. Yet, it contains enough information to study many aspects of normalisation.

We define several normal forms of derivations, mostly based on the notion of \emph{streamlining} which is a generalisation of cut elimination. The normal forms are defined in terms of atomic flows and we say that a derivation is streamlined if its associated atomic flow has a certain shape.

We present normalisation procedures to obtain our normal forms. Each normalisation procedure is given both for atomic flows and derivations and we prove soundness results showing that whatever normalisation step can be applied to an atomic flow the corresponding step can be applied to the derivation. The novelty of these normalisation procedures is that they are dictated in their entirety by the atomic flows of the derivations they normalise.

The results we present are in the formalism calculus of structures, but as it turns out atomic flows, and hence our normalisation results, are not strongly dependent on our choice of formalism. As long as the formalism has certain properties, like atomicity of structural rules and linearity of logical rules, our methods will apply.

The intention is for this work to help in the search for better representations of proofs and to help in the study of complexity and identity of proofs. In particular the open problems in complexity we might hope to contribute to are
\begin{itemize}
 \item Interpolation --- What is the lower bound on the interpolant of two formulae and
 \item Polynomial simulations of proof systems --- E.g. does Frege polynomially simulate extended Frege?
\end{itemize}


\section{Work done so far}

\begin{itemize}
\item Atomic flows were introduced in the paper \emph{Normalisation Control in Deep Inference via Atomic Flows} (attached) published in \emph{Logical Methods for Computer Science}. This was work done jointly with Alessio Guglielmi.
\item There is a draft (attached) of a follow-up paper preliminarily called \emph{Normalisation Control in Deep Inference via Atomic Flows II}. This is also work done jointly with Alessio Guglielmi. The results are all done, but the paper needs extensive writing before it can be published.
\item There is an almost finished draft paper (attached), \emph{Quasipolinomial Normalisation in Deep Inference}. This is work done jointly with Paola Bruscoli and Alessio Guglielmi. My contribution to the paper is a simplification of the \emph{threshold functions}, which is a technical device used in the paper.
\end{itemize}

\section{Remaining work}

\begin{itemize}
\item I have a, so far unpublished, technique which would allow the results about quasipolinomial normalisation to work for streamlining and not only cut elimination. This would be worth while writing up. However, this way of solving the problem is not very elegant and I would like to spend some time on finding an elegant solution, possibly along the lines of \emph{Atomic Flows II}.
\item Alessio Guglielmi and Michel Parigot are working on a paper about a new formalism, \emph{Formalism B}. My plan is to contribute a normalisation result, probably based on \emph{Atomic Flows II}, to this paper.
\item There is a draft of a paper showing the polynomial relationship between the sizes of derivations and atomic flows written by Paola Bruscoli, Lutz Stra\ss{}burger and Alessio Guglielmi, which I hope to contribute to.
\item It would be interesting to see how our techniques extend beyond propositional classical logic. It seems possible that classical modal logic could be studied in the remaining time of the PhD, so this is something I would like to attempt (possibly in parallel with writing up).
\end{itemize}

\end{document}