Re: Pomset vs BV

Hi Jon,

>In Christian Retore's paper on Pomset Logic, he shows (via coherence
>semantics) that there is only one self-dual noncommutative binary
>operator which can be added to MLL. Since BV gives such an operator,
>can't one just conclude that it captures the Pomset operator? That is,
>do we *really* need to consider the proof nets for Pomset (of which
>there are two flavours - the one in Retore's original paper, and the one
>based on "directed cographs"). 
>

The problem is that of completeness, that is, whether BV captures all 
provable
pomset-logic formulas. Lutz has shown in his thesis that BV is sound 
with respect
to Pomset logic. There's just a little "gap" in the completeness proof 
(Lutz can tell
you more about it) that we are unable to bridge for four years now!
I'll be interested if you have any thought about it.

Best regards,
-Alwen