Quasipolynomial normalisation in deep inference

Alessio Guglielmi <[email protected]> Wed, 25 Mar 2009 13:07:49 +0100
Newsgroups gmane.science.mathematics.frogs
Message-ID <49ca1e9b.1a67f10a.39fd.ffffbf36SMTPIN_ADDED__36630.7397060611$1264448683$gmane$org@mx.google.com>
Hello,

We would like to announce the paper mentioned 
below, which continues a line of work  on 
normalisation in deep inference, where we get 
quasipolinomial normalisation procedures for 
propositional logic. This is essentially due to 
our dealing with a more general notion of 
analyticity than in the sequent calculus, and to 
the novel symmetry of proofs, typical of deep 
inference.

You can find information about deep inference at 
<http://alessio.guglielmi.name/res/cos/>.

Comments are very welcome, of course. Please note 
that the web site where the paper resides will 
not be available during this coming week-end.

Best regards,

-Alessio


Quasipolynomial Normalisation in Deep Inference 
via Atomic Flows and Threshold Formulae
<http://cs.bath.ac.uk/ag/p/QuasiPolNormDI.pdf>
--------------------------------------------------
P Bruscoli, A Guglielmi, T Gundersen and M Parigot

Jerábek showed that analytic propositional-logic 
deep-inference proofs can be constructed in 
quasipolynomial time from nonanalytic proofs. In 
this work, we improve on that as follows: 1) we 
significantly simplify the technique; 2) our 
normalisation procedure is direct, i.e., it is 
internal to deep inference. The paper is 
self-contained, and provides a starting point and 
a good deal of information for tackling the 
problem of whether a polynomial-time 
normalisation procedure exists.