gmane.science.mathematics.frogs

Last CFP: Workshop on Logics for Resources, Processes and Programs (LRPP 2012)

Pym, Professor David J. — 2012-05-08T17:30:47

------------------------------------------------------------------------------
Call For Papers

Workshop on Logics for Resources, Processes and Programs
(LRPP 2012)

1st July 2012, Manchester, UK

(affiliated with IJCAR 2012, Manchester, UK)

http://www.loria.fr/~galmiche/LRPP2012.html

Extended deadline: May 20, 2012
----------------------------------------------------------------------

A one day workshop on `Logics for Resources, Processes, and Programs'
will be held the 1st July 2012 in conjunction with the IJCAR 2012
Conference in Manchester, UK, with D. Galmiche and D. Pym as organizers.

The purpose of this workshop would be to discuss recent results on
logics, including systems formulated in the style of Hoare and
Hennessy-Milner, for modelling resources, processes, programs, and
their interactions. We envisage a range of perspectives:
proof-theoretic foundations, including decidability and complexity;
semantic foundations (e.g., new resource semantics); specification of
properties and behaviours; ve

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:32:56

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsof

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:27:40

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifica

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:32:56

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsof

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:27:40

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifica

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:32:56

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsof

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:27:40

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifica

Announcement

Agata Ciabattoni — 2011-09-27T12:34:22

2-YEAR POSTDOCTORAL POSITION ON STRUCTURAL PROOF THEORY

* The Vienna University of Technology is looking to recruit one
   Postdoctoral Research Assistant to work on the FWF-funded
   project "Nonclassical Proofs: theory, applications and tools", under the
   direction of Agata Ciabattoni.
* The work will take place within the Institute of Computer Languages
   (Theory and Logic group) of the Vienna University of Technology.
* The post is for an appointment of up to 24 months
   and is available from January 2012.
* Applicants should have (or shortly expect to receive) a PhD in
   Mathematics, Computer Science or a closely related field, a strong
   background in structural proof theory, nonclassical logics, and
   knowledge of universal algebra or complexity theory.
   Ability to work independently but also with academic colleagues
   and PhD students, flexibility and teamwork, are all important
   qualifications for this position.
* Further particulars, including details of how to apply, are available

Bruno Woltzenlogel Paleo invited you to join him on Google+

Google+ — 2011-07-11T04:13:58

Bruno Woltzenlogel Paleo is using Google+ and invited you to join.

Click here to get started with Google+:  
https://plus.google.com/_/notifications/emlink?emrecipient=102974918492086419375&emid=CMDr48y2-KkCFUWq7AodrKK2Ag&path=%2Fwelcome%3Fgpinv%3DAGXbFGzWAF-ZnkbkVEP6tpIfJ24_YoCVqvJjcuQVq_hyEPTq9IVnDBZxOcHuE-pp0gtffgAeBxRc05FdirpEGWpBB8w1cJ-KSxUhV_qibJ5YbrXsVptjq5I%26hl%3Den

The Google+ project is currently working out all the kinks with a small  
group of testers. If you're not able to access Google+, please check back  
again soon.
------------------------
You received this message because Bruno Woltzenlogel Paleo invited  
frogs.list< at >gmail.com to join Google+. Click here to unsubscribe from these  
emails:  
https://plus.google.com/_/notifications/emlink?emrecipient=102974918492086419375&emid=CMDr48y2-KkCFUWq7AodrKK2Ag&path=%2Fnonplus%2Femailsettings%3Fgpinv%3DAGXbFGzWAF-ZnkbkVEP6tpIfJ24_YoCVqvJjcuQVq_hyEPTq9IVnDBZxOcHuE-pp0gtffgAeBxRc05FdirpEGWpBB8w1cJ-KSxUhV_qibJ5YbrXsVptjq5I%26est%3DADH5u

Marketing

Alessio Guglielmi — 2011-05-06T19:03:26

Hello,

I recently found that several publications for 
the deep inference page escaped me, so I worked a 
couple of days to catch up. Could you please 
check that everything that could be on 
<http://alessio.guglielmi.name/res/cos/> is 
there, and that what is there is correct?

Also, if you have grants that are not listed, I'd like to know.

This is an appeal to conformism, of course, 
primarily to attract further funding,  mostly for 
postdocs. I'm about to apply for a ~£750,000 
project, we have to shine.

BTW, I don't like hosting the deep inference page 
on a domain with my name (because it seems 
misappropriation, in a way). It's like this only 
because of inertia. I also don't like the idea of 
hosting the stuff on University web pages because 
then they have control on the content. (I bought 
that domain when I realised that I wasn't a free 
man.)

The `open problems' web page is badly badly 
outdated, but it takes a lot of time to collect 
and keep the information organised, I'm 
overwhelmed.

I h

Postdoc position in proof theory in Paris

Lutz Strassburger — 2011-04-25T01:49:34

--------------------------------------------------------
Postdoc position in proof theory in Paris
--------------------------------------------------------

There is an opening of a postdoc position on structural and
computational proof theory. The position is financed by
the ANR within the project STRUCTURAL
<http://www.lix.polytechnique.fr/~lutz/orgs/structural.html>

The postdoc will be hosted by the Laboratoire d'Informatique (LIX) at
the Ecole Polytechnique, one of the "Grand Ecoles" in the French
university system, located in the suburbs of Paris.

Applicants must have a Ph.D. or equivalent in computer science or
mathematics, and should have a strong background in proof theory
and related topics. The principal responsibility of the postdoc
will be to carry out research in the area of proof theory within the
project STRUCTURAL. There are no teaching duties.

For further information, see
<http://www.lix.polytechnique.fr/~lutz/orgs/structural-postdoc.html>

or contact
   Lutz Strassburger <lutz-TgEOGOHWQ

Sophia Strassburger

Alessio Guglielmi — 2011-04-16T13:55:24

Hello,

Sophia Strassburger was born this morning, and everybody is well. She 
will make Lutz a civilised person!

-Alessio

Deeper Cuts in Deep Inference

Bruno Woltzenlogel Paleo — 2011-03-15T18:17:33

Hi!

I noticed that in deep inference (I am having the system SKS in mind), the cut is not as "deep" as it could be. What I mean is the following:

consider the "ai-up" (a.k.a. cut) rule of SKS:

S{~a and a}
----------------
S{ false }

This rule is certainly deep in the sense that it can be applied inside any context S. But it is also shallow in the sense that the cut-formulas do not appear inside any context. I can imagine a "deeper" cut-rule as follows:

S{~a and S'{a}}
--------------------  (1)
S{ S'{false} }

and we could go further and have something like this (which is like a deeper application of modus ponens):

S{(~a or b) and S'{a}}
------------------------------  (2)
S{ S'{b} }

and we can try to go even further and find out what happens when both cut-formulas are within arbitrary contexts:

S{S''{~a} and S'{a}}
--------------------------------------------------------------------------  (3)
S{ ?? }    (any of S{S'{S''{false}}} or S{S''{S'{false}}} ???)


I think that deep modus ponens as formalize

deep inference combinators implementation

Kai Brünnler — 2011-02-16T21:14:54

Hi Frogs,

as an exercise, I've started implementing a interpreter for a little
programming language based on deep inference (in the Curry-Howard sense).
The implementation is in Scala and is shared here on
GitHub<https://github.com/kaibr/dicomb>.
Take a look if you're interested. It can already do amazing things: you
could execute a program that takes an ordered pair and returns its first
component!

Comments and contributions are welcome, of course! I've just barely started,
so it should be easy to get into. I'm currently in the process of
implementing a parser (yes, right now programs are given as abstract syntax
trees), and then I'd like to add lots of example programs to test the
interpreter and the type inference and to experiment with the language.

Oh yes, the paper it is based on is "An Algorithmic Interpretation of a Deep
Inference System" by Richard and myself, available from
here<http://www.iam.unibe.ch/%7Ekai/Papers/2008aidis.pdf>,
if you'd like some background.

Best wishes and maybe happy hack

Facebook Pages on Logical Subjects

Jon Awbrey — 2011-01-20T16:08:38

Here's an assortment of Facebook pages I created that may
be of interest to Frog people who like that sort of thing:

http://www.facebook.com/pages/Differential-Logic/119559524768107

http://www.facebook.com/pages/Inquiry-Driven-Systems/119515558104734

http://www.facebook.com/pages/Logical-Graphs/110462975683687

http://www.facebook.com/pages/Minimal-Negation-Operators/168166306533929

http://www.facebook.com/pages/Peirce-Matters/159237477450823

http://www.facebook.com/pages/Relation-Theory/163244363703101

http://www.facebook.com/pages/Riffs-Rotes/167712413262717

http://www.facebook.com/pages/Semeiotics/110200632380093

http://www.facebook.com/pages/Theme-One/134629236593886

Jon Awbrey

a.k.a. "Jonny Cache" http://www.facebook.com/people/Jonny-Cache/1039153428

HDR

Lutz Strassburger — 2011-01-07T10:43:33

Hi Frogs,

my habilitation thesis
"Towards a Theory of Proofs of Classical Logic"

is available here:
<http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf>

The public defense takes place today at 14:00 at Ecole Polytechnique 
(Amphi Bequerel).

Best wishes,
Lutz

REDO meeting in Bath, Sep 14-16

Lutz Strassburger — 2010-08-20T13:10:43

Hi Frogs,

there will be a small meeting on proof theory and related topics in Bath 
from September 14 to September 16.

<http://www.lix.polytechnique.fr/~lutz/orgs/redo-meeting-sep10.html>

Everybody is invited to join.

Since I'll be away from email for the next two weeks, please send an email 
to Alessio Guglielmi (with cc to me) if you are interested in attending 
the meeting or giving a talk.

(Since you are on this mailing list, you have Alessio's email address.)

Best regards,
Lutz

Animated Proofs

Jon Awbrey — 2010-03-14T19:04:45

Hi All --

I finally got around to doing something I've
been thinking about doing since the late 60's,
animating proofs in Peirce's logical graphs.

Here's a rough cut where all I did was flip through
a sequence of images that I had already made up
in storyboard form:

http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Propositional_Equation_Reasoning_Systems#Majority_function_example

Jon Awbrey

Meeting in Vienna

Alessio Guglielmi — 2009-08-05T11:13:35

Hello,

Agata, Lutz and I were thinking of meeting in 
Vienna for a 2/3-day workshop in the period 
24.10-5.11. We are interested in discussing the 
state of the art and perspectives for the proof 
systems of modal and substructural logics.

More in general, the themes should be at least in 
part those of the project Démosthène (Identity 
and Geometric Essence of Proofs) and REDO 
<http://www.lix.polytechnique.fr/~lutz/orgs/redo.html>, 
plus modal logics and whatever interests our 
Austrian hosts.

I liked a lot the format of the recent meeting at 
LIX 
<http://www.lix.polytechnique.fr/~lutz/orgs/redo-meeting-may09.html>, 
so my proposal is to do the same, perhaps on a 
smaller scale.

I would ask the interested people to raise their 
hand and suggest dates (between 24.10 and 5.11), 
so that we can be more specific.

Ciao,

-Alessio

decomposition and splitting for NEL

Lutz Strassburger — 2009-03-30T09:03:10

Hi Frogs,

In preparation for the exciting developments in quantum causal evolution, 
we revised the old paper "A System of Interaction and Structure IV: The 
Exponentials" on the normalisation theory of NEL.

Encouraged from referees, we split the paper into two parts, one about 
decomposition and the other about splitting. We think that this makes the 
whole matter clearer and more accessible. Please do not cite the old 
paper, the new ones are better.

Comments of any kind are very welcome.

Best regards,
Alessio and Lutz

----------------------------------------

Title: A System of Interaction and Structure IV: The Exponentials and 
Decomposition

L. Strassburger and A. Guglielmi

Abstract:
System NEL is the mixed commutative/non-commutative linear logic BV
augmented with linear logic's exponentials, or, equivalently, it is
MELL augmented with the non-commutative self-dual connective
seq. System NEL is Turing-complete, it is able to directly express
process algebra sequential composition and it faithfull

Quasipolynomial normalisation in deep inference

Alessio Guglielmi — 2009-03-25T12:07:49

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 nonan