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.