1 Nov 2004 08:01

### Re:ICALP workshop proposal: Applications of New Proof Theory

At 15:24 +0200 28.10.04, Charles A Stewart wrote:
>I talked yesterday with Alessio about the possibility of putting
>together a workshop that would highlight the kind of proof theory
>that we like: deep inference, rewriting modulo, and generally
>good proof theory.  I think the idea of "new proof theory" is a way
>to get away from the unhealthy conservatism that cripples so much
>work on proof theory done in the LICS community.

I think the workshop might be a good idea. I checked with Catuscia
(who's PC chair) and she told me that what we do fits ICALP very well.

I'm not sure about "new proof theory" etc. I would go for a lower,
technical profile rather than an ideological one.

The workshop organisation might be a collaboration with Nancy, also
as a nice way to conclude our Procope project. What do you think
Francois?

A theme could be "Deep inference and proof nets", or something like
that, joining in the broadest sense our common themes. Since we
organised in Dresden already several workshops along these lines, we
should have a certain credibility. One common goal to state could be
getting to deductive proof nets.

A more provocative idea could be to dedicate the workshop to
something like "towards deductive proof nets", but I don't know how
many people share my feelings about the subject...

One thing I'd like to do is having a face-to-face discussion about
the issues in the last several emails about strategic goals, ways to

(Continue reading)

1 Nov 2004 07:11

### Re: Splitting, cut elimination and classical logic

At 18:05 +0200 21.10.04, Lutz Strassburger wrote:
>  > Take
>>
>>      S = [ ([a,b],[c,d]) , ([-a,-c],[-b,-d]) ] .
>>
>>  S is provable by a proof of the shape
>>
>>                      _
>>                      | {s,ai_}
>>                      |
>>        [ (a,c),(b,d) ,([-a,-c],[-b,-d])]
>>      m --------------------------------- .
>>        [([a,b],[c,d]),([-a,-c],[-b,-d])]
>>
>>  However, it is also possible to prove it by a proof of this shape
>>
>>                      _
>>                      | {s,ai_}
>>                      |
>>        [([a,b],[c,d]), (-a,-b),(-c,-d) ]
>>      m --------------------------------- .
>>        [([a,b],[c,d]),([-a,-c],[-b,-d])]
>>
>>  If P = [a,b] and Q = [c,d] and R = ([-a,-c],[-b,-d]), the splitting
>>  theorem should capture the migration' of medial from the proof above
>>  (P,Q) to the generated proof above R.
>
>from the point of view of proof nets, the two proofs are identical. If you
>apply splitting to one of them and then put the pieces together, you
>should end up with the other.

(Continue reading)

1 Nov 2004 14:36

### Re:ICALP workshop proposal: Applications of New Proof Theory

At 8:01 Uhr +0100 01.11.2004, Alessio Guglielmi wrote:
>At 15:24 +0200 28.10.04, Charles A Stewart wrote:
>>I talked yesterday with Alessio about the possibility of putting
>>together a workshop that would highlight the kind of proof theory
>>that we like: deep inference, rewriting modulo, and generally
>>good proof theory.  I think the idea of "new proof theory" is a way
>>to get away from the unhealthy conservatism that cripples so much
>>work on proof theory done in the LICS community.
>
>I think the workshop might be a good idea. I checked with Catuscia
>(who's PC chair) and she told me that what we do fits ICALP very
>well.

Well, if it fits then we should try.

>I'm not sure about "new proof theory" etc. I would go for a lower,
>technical profile rather than an ideological one.

Me neither. From one hand it is not informative, and from the other
it can sound offensive for those that make "old proof theory": does
it bring any good hurting their sensibility? (Can we claim our
ideology is that of an ecological proof theory respecting all
amphibians, at the very first place?)

A title can be found after we know the topics we want to include.

>The workshop organisation might be a collaboration with Nancy, also
>as a nice way to conclude our Procope project. What do you think
>Francois?
>

(Continue reading)

2 Nov 2004 18:58

### Paper anouncement


Hi Frogs,

since there was a recent discussion on cut elimination and proof nets for
classical logic, there might be some interest in the following paper that
we submitted to TLCA'05:

Title: Naming Proofs in Classical Propositional Logic

Authors: Francois Lamarche and Lutz Strassburger

Abstract:
We present a theory of proof denotations in classical propositional
logic. The abstract definition is in terms of a semiring of weights,
and two concrete instances are explored.  With the Boolean semiring
we get a theory of classical proof nets, with a geometric
correctness criterion, a sequentialization theorem, and a strongly
normalizing cut-elimination procedure. With the semiring of natural
numbers, we obtain a sound semantics for classical logic, in which
fewer proofs are identified. Though a real'' sequentialization
theorem is missing, these proof nets have a grip on complexity
issues.  In both cases the cut elimination procedure is closely
related to its equivalent in the calculus of structures, and we get
Boolean'' categories which are not posets.

The paper is available on the web at
http://www.ps.uni-sb.de/%7elutz/papers/namingproofsCL.pdf

Comments are welcome.


(Continue reading)

2 Nov 2004 21:07

### Re:Paper anouncement

At 18:58 +0100 2.11.04, Lutz Strassburger wrote:
>there might be some interest in the following paper that we
>submitted to TLCA'05:
>
>Title: Naming Proofs in Classical Propositional Logic
>
>Authors: Francois Lamarche and Lutz Strassburger

Nice introduction. I would have made some room for citing the CSL 04
paper (referee persuasion!).   -Alessio


3 Nov 2004 01:03

### Re:ICALP workshop proposal: Applications of New Proof Theory


> >Another thing I'd be interested in doing is having a discussion with
> >the display calculus people. Perhaps Rajeev would be around in
> >Europe and willing to do this. Rajeev?

Yes, I can try to be there. I don't know my dates yet but they usually
revolve around TABLEAUX.

http://www.uni-koblenz.de/~beckert/Events/Tableaux2005/

The other possibility would be to have a related workshop at TABLEAUX
2005 which will be in Germany this year (probably
Koblenz). Unfortunately, TAB is in Sept and ICALP in July. I doubt if
I could make it to both.

> >>Who do we know would be willing to do the soul-destroying task of
> >>refereeing submissions?

As I suggested privately to Charles, we could have an informal PC for
this. Many people are willing to devote time and energy to workshops
if we just ask them.

> >That's something I can do. IMPORTANT CONDITION: for the usual
> >political reasons I'm willing to participate only if there are no
> >(widely disseminated) proceedings. Subsequent publication in
> >journals is fine, of course, after further, careful journal-standard
> >reviewing.
> I have no specific opinion on refereeing yet, as it depends on the
> topics and number of submissions we expect to collect. I would like
> to preserve the same spirit of meetings we had so far.

(Continue reading)

8 Nov 2004 09:49

### Re: Paper announcement


Hi Frogs,

Carsten Fuehrmann and David Pym made some comments about our classical
logic paper that has recently been announced here. These comments might be
of interest for frogs people.

Cheers,
Lutz

On Thu, 4 Nov 2004, Carsten Fuhrmann wrote:

> Dear Francois and Lutz,
>
> Thanks for making us aware of your TLCS article; I have now read it,
> with pleasure. One difference between our works is of course that you
> add MIX explicitly, and therefore can obtain a confluent
> cut-elimination procedure. By contrast, we consider MIX to be defined
> by using Cut:
>
>         \pi_1				           \pi_2
>         .                                           .
>         .                                           .
>         .                                           .
> \Gamma1 |- \Delta1                        \Gamma2 |- \Delta2
> -----------------------    ------------   -----------------------
> \Gamma1 |- \Delta1,\bot    \bot |- \top   \top,\Gamma2 |- \Delta2
> ----------------------------------------------------------------- two cuts
>            \Gamma1,\Gamma2 |- \Delta1,\Delta2
>

(Continue reading)

11 Nov 2004 12:26

### Mailing list

Hello,

I thought it's not very appropriate that the home page of this list
resides on my domain, so I moved it to
<http://www.prooftheory.org/frogs/index.html>.

It is possible to use Frogs@... for sending messages, in
addition to the old address.

Ciao,

-Alessio


18 Nov 2004 07:02

### Web page on open problems

Hello,

I've got many requests for theses topics (both MSc and PhD), so I
started putting together a web page trying to list all open problems
and topics we're working on, requests of collaborations, etc.

The page is at <http://alessio.guglielmi.name/res/cos/crt.html>. As
you see, it's still a draft. I'd appreciate getting suggestions and
descriptions of open problems of which you're knowledgeable. I plan
to finish with this page in the next very few days, please help me!

I think it's important to have something like this, many students,
especially at ESSLLI, asked me for this already.

Ciao,

-Alessio


25 Nov 2004 15:46

### Proposal for a workshop in Lisbon

Hello,

as many of you know, we are about to submit a proposal for a workshop
to be held in Lisbon, next July, attached to the ICALP conference.
I'm sending this email to the invited speakers, the PC members and
the Frogs mailing list. (For those who don't know Frogs, here is a
description: <http://www.prooftheory.org/frogs>). I'm asking you to
provide feedback on a call for papers outlining the themes of the
workshop.

In the past we organised a series of workshops in Dresden, more or
less about the same topics of the following proposal.
<http://www.computational-logic.org/iccl/events/WPT-2004/>
<http://www.ki.inf.tu-dresden.de/%7eguglielm/WSPT/index.html>
<http://www.cl.inf.tu-dresden.de/compulog/events/workshop.html>

This time we feel that we are ready for a broader participation, and
we also think this is a good way of terminating a two-year research
grant we shared between Nancy and Dresden that has been extremely
fruitful.

So, I'm asking you for comments and suggestions about the call for
papers, which you find below, and whether you might consider
submitting a paper to this workshop. It is very important for us to
have an estimate of the number of participants, so please let us know.

It is very urgent, the proposal and the number of expected
participants must be sent before Sunday, please answer now. (Sorry
for the hurry: the idea occurred to Charles only very recently).

`
(Continue reading)

Gmane