headers
Alessio Guglielmi | 1 Nov 2004 08:01
Picon
Favicon

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)

Permalink | Reply | 2 comments |
headers
Alessio Guglielmi | 1 Nov 2004 07:11
Picon
Favicon

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)

Permalink | Reply | 0 comments |
headers
Paola Bruscoli | 1 Nov 2004 14:36
Picon
Favicon

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)

Permalink | Reply | 1 comment |
headers
Lutz Strassburger | 2 Nov 2004 18:58
Picon

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)

Permalink | Reply | 3 comments |
headers
Alessio Guglielmi | 2 Nov 2004 21:07
Picon
Favicon

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
Permalink | Reply | 0 comments |
headers
Rajeev.Gore | 3 Nov 2004 01:03
Picon
Picon

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)

Permalink | Reply | 0 comments |
headers
Lutz Strassburger | 8 Nov 2004 09:49
Picon

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)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 11 Nov 2004 12:26
Picon
Favicon

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
Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 18 Nov 2004 07:02
Picon
Favicon

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
Permalink | Reply | 0 comments |
headers
Paola Bruscoli | 25 Nov 2004 15:46
Picon
Favicon

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)

Permalink | Reply | 0 comments |

Gmane