headers
Phiniki Stouppa | 2 Jun 2005 21:42
Picon

A cut-free CoS system for S5

Dear all,

attached is a paper (draft) I've written lately on the technical
results of my master thesis (completed last October in Dresden,
supervised by Charles Stewart). It is entitled "a system of deep
inference for the modal logic S5" and presents a cut-admissible system
for S5 in the calculus of structures. A short elaboration on the
importance and consequences of deep inference in modal systems is
given in the introduction.

I am planning to apply the final corrections/changes and submit it for
publication by the end of next week. Comments/suggestions/corrections
are more than welcome.

Regards,
Phiniki
Attachment (report_plain.pdf): application/pdf, 185 KiB
Permalink | Reply | 17 comments |
headers
Ozan Kahramanogullari | 3 Jun 2005 10:27
Picon
Favicon

Paper announcement

Dear All,

I would like to advertise the following paper, which is
accepted at the WoLLIC'05.

cheers,
-Ozan

Title: System BV is NP-complete

Abstract:
System BV is an extension of multiplicative linear logic
(MLL) with the rules mix, nullary mix, and a self-dual,
non-commutative logical operator, called seq. While the
rules mix and nullary mix extend the deductive system,
the operator seq extends the language of MLL. Due to the
operator seq, system BV extends the applications of MLL
to those where sequential composition is crucial, e.g.,
concurrency theory. System FBV is an extension of MLL
with the rules mix and nullary mix. In this paper, by
relying on the fact that system BV is a conservative
extension of system FBV, I show that system BV is
NP-complete by encoding the 3-Partition problem in FBV.
I provide a simple completeness proof of this encoding
by resorting to a novel proof theoretical method for
reducing the nondeterminism in proof search, which is
also of independent interest.

http://www.informatik.uni-leipzig.de/~ozan/Papers/BVnpc.pdf
(Continue reading)

Permalink | Reply | 0 comments |
headers
Richard McKinley | 3 Jun 2005 15:22
Picon
Favicon

New bureacracy/coherence

Hi all,

I was investigating the simulation of LK cut-reduction in SKS (from a 
semantic point of view)
and I came across the following pair of proofs (notation as in Lutz's 
recent paper on proof nets and SKS):

[(A, f ) , (B,C)]
-----------------m
( [A,B] , [f, C])
----------------- up-t
( [A,B] , C)
----------------- s , plus some \sigmas
[ A , (B , C)]

and

[(A, f ) , (B,C)]
------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
[(A, t ) , (B,C)]
--------------------- up-f
[ A , (B , C)]

Has anyone considered this kind of thing before?  The reason behind 
considering the two
equal would be admissibilty of sequent calculus cut reduction in SKS 
(specifically
reduction of cut against contraction).  It also looks like the kind of 
coherence you might want to
hold of a categorical medial law.
(Continue reading)

Permalink | Reply | 2 comments |
headers
Lutz Strassburger | 3 Jun 2005 18:00
Picon

Re: New bureacracy/coherence

On Fri, 3 Jun 2005, Richard McKinley wrote:

> Hi all,
>
> I was investigating the simulation of LK cut-reduction in SKS (from a 
> semantic point of view) and I came across the following pair of proofs 
> (notation as in Lutz's recent paper on proof nets and SKS):
>
> [(A, f ) , (B,C)]
> -----------------m
> ( [A,B] , [f, C])
> ----------------- up-t
> ( [A,B] , C)
> ----------------- s , plus some \sigmas
> [ A , (B , C)]
>
>
> and
>
> [(A, f ) , (B,C)]
> ------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
> [(A, t ) , (B,C)]
> --------------------- up-f
> [ A , (B , C)]
>
> Has anyone considered this kind of thing before?  The reason behind 
> considering the two equal would be admissibilty of sequent calculus cut 
> reduction in SKS (specifically reduction of cut against contraction). 
> It also looks like the kind of coherence you might want to hold of a 
> categorical medial law.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 8 Jun 2005 11:46
Picon
Favicon

Re:New bureacracy/coherence

At 2:22 PM +0100 3.6.05, Richard McKinley wrote:
>I was investigating the simulation of LK cut-reduction in SKS (from 
>a semantic point of view) and I came across the following pair of 
>proofs (notation as in Lutz's recent paper on proof nets and SKS):
>
>[(A, f ) , (B,C)]
>-----------------m
>( [A,B] , [f, C])
>----------------- up-t
>( [A,B] , C)
>----------------- s , plus some \sigmas
>[ A , (B , C)]
>
>
>and
>
>[(A, f ) , (B,C)]
>------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
>[(A, t ) , (B,C)]
>--------------------- up-f
>[ A , (B , C)]
>
>Has anyone considered this kind of thing before?  The reason behind 
>considering the two equal would be admissibilty of sequent calculus 
>cut reduction in SKS (specifically reduction of cut against 
>contraction).  It also looks like the kind of coherence you might 
>want to hold of a categorical medial law.

Hi,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 13 Jun 2005 06:36
Picon
Favicon

Re:A cut-free CoS system for S5

At 21:42 +0200 2/6/05, Phiniki Stouppa wrote:
>attached is a paper (draft) I've written lately on the technical
>results of my master thesis (completed last October in Dresden,
>supervised by Charles Stewart). It is entitled "a system of deep
>inference for the modal logic S5" and presents a cut-admissible system
>for S5 in the calculus of structures. A short elaboration on the
>importance and consequences of deep inference in modal systems is
>given in the introduction.
>
>I am planning to apply the final corrections/changes and submit it for
>publication by the end of next week. Comments/suggestions/corrections
>are more than welcome.

Hello,

I'm sending you several comments privately. I have one issue which 
could be suitable for discussion on the list.

The question is: Are the display calculus or hypersequents deep 
inference formalisms? Should we consider them so?

As far as I know, people in these areas never considered themselves 
as doing deep inference. Am I right? I think the term `deep 
inference' has been invented by Kai, actually. If so, I'm not sure we 
should tag the display calculus or hypersequents with deep inference, 
at least in context where there isn't a thorough discussion.

I see the reasons for the modal logicians: there is a clear 
indication that, in order to do proof theory for modal logic, there 
is a need of *some form* of deep inference. This is clear.
(Continue reading)

Permalink | Reply | 13 comments |
headers
Jon Cohen | 13 Jun 2005 08:56
Picon
Picon

Re:A cut-free CoS system for S5

Ribbit all,

On Mon, 2005-06-13 at 14:36, Alessio Guglielmi wrote:
> The question is: Are the display calculus or hypersequents deep 
> inference formalisms? Should we consider them so?

I don't know much about hypersequents but, from the little I know of
display calculus, I believe that it ought to be considered as a form of
deep inference. For instance, suppose we are working in a display
formalism and want to use a version of switch. Let's look at how to do
this on the left of the turnstile. What we want is a rule that says
something like (where | is "or" and "&" is and):

(R|U)&T |- XoY
---------------  (*)
(R&T)|U |- XoY

How to show that this is admissable? Well, suppose that we have a proof
of (R|U)&T. Let us unravel it:

R |- T*oX   U |- Y
-----------------
  (R|U) |- *ToXoY
  --------------
  (R|U)oT |- XoY
  --------------
  (R|U)&T |- XoY

Now we can yank the proofs of R |- T*oX and U |- Y and travel by a
different path:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Greg Restall | 13 Jun 2005 08:38
Favicon

Re: A cut-free CoS system for S5

I think I concur with Alessio on the matter of the characterisation  
of Deep Inference as "fully deep" inference.

There's no doubt that even the classical sequent calculus can be seen  
as an inference system that is somewhat deep: if you think of a  
sequent of the form X |- Y as consisting of a conditional with a  
conjunction in the antecedent and a disjunction in the antecedent,  
then we can make inferences down to that depth.

Display logic presentations of modal or other substructural logics  
allow inferences to go inside more, allowing for existential  
operators (diamond, or fusion) in antecedent position and universal  
operators (box, or arrow, or fission) in succedent position, together  
with a dualising operator.  There's no doubt that this allows for  
more depth, but it doesn't provide a structure in which formulas can  
be /atomised/, and this is the difference when we compare with CoS.   
A disjunction in antecedent position cannot be converted into  
structure.  (Its inferential power is exhibited by branching in the  
sequent derivation: another way that the difference with CoS  
manifests itself.  Here hypersequents and display sequents are on the  
side of the sequent calculus, and CoS stands apart.)

(I'm beginning to form some ideas of why both approaches have their  
own advantages/disadvantages, but the *detail* is not completely  
clear to me yet.)

I'd be interested to hear if my take on this is thought to be  
idiosyncratic, or if it's a fair statement of the situation.

Best wishes,
(Continue reading)

Permalink | Reply | 10 comments |
headers
Charles A Stewart | 13 Jun 2005 16:37
Picon
Favicon

Re: A cut-free CoS system for S5


Hi Alessio, hi amphimaniacs,

> I'm sending you several comments privately. I have one issue which 
> could be suitable for discussion on the list.

> The question is: Are the display calculus or hypersequents deep 
> inference formalisms? Should we consider them so?

The terminology I'm now favouring is distinguishing three kinds of
depth:
  1. Surface inference: what you get with no-frills Gentzen sequent
  systems: for LK-like systems this means you can swim about
  outermost disjunctions and no deeper.  (Note that one can be less
  deep even than this: ie. the Hilbert calculus, and Alessio has
  suggested one may even be able to get cut-elimination result for
  some such depthless inference systems).
  2. Non-surface inference: able to perform inference deeper than this:
  the hypersequent calculus is an example of this; the system for S5
  allows you to freely act around disjunctions inside necessities
  inside disjunctions, but no deeper.
  3. True deep inference: there is no bound on the logical complexity
  that you're able to move about in.  Hence display logic is truly
  deep.

Display logic does have a catch, and the way I would put it is this:
in order to maintain the subformula property, it is necessary to
"freeze" formulae that are produced by logical (as opposed to
structural) inference rules.  This means that conjunction-like rules
force a separation of their premisses, and so the inference takes
(Continue reading)

Permalink | Reply | 0 comments |
headers
Rajeev.Gore | 14 Jun 2005 01:40
Picon
Picon

Re: A cut-free CoS system for S5


I agree with Greg. Displaying is a type of deep inference. But it is
not the same. Also, to my knowledge, nowhere in the display literature
is there any mention of the idea of rewriting at any depth. This is
explicit in CoS and in the rewriting literature of course. I would
even argue that there are reasons why we might want to avoid deep
inference. That is, it should be derivable but not necessarily built
in from the start to make sure that our rules capture substitution
properly. 

raj
Permalink | Reply | 9 comments |

Gmane