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; verification and analysis of programs and
systems. It should help to establish and publicize a research agenda
for such logics and their use in the development of trusted
systems.

The workshop is intended to provide a forum for discussion between
researchers interested in logics of resources (from foundations to
related calculi and applications) and researchers interested in
languages and methods for specification of mobile, distributed,
concurrent systems and their verification.


Topics of interest include, but are not restricted to,
the following:

- Logics for resources: semantics and proof theory;
- Process calculi, concurrency, resource-distribution;
- Reasoning about programs and systems;
- Extensions of logics; e.g., with modalities;
- Languages of assertions, languages based on resource logics (query
  languages, pointers, trees, and graphs) and reasoning;
- Theorem proving and model checking in resource logics:
  decision procedures, strategies, complexity results.

KEYNOTE SPEAKER

Peter O'Hearn (UCL, London,UK)

SUBMISSIONS

Researchers interested in presenting their works are invited to send an
extended abstract (up to 10 pages) by e-mail submissions of PDF files
to D. Galmiche (Didier.Galmiche-/zGXu1G9BXs< at >public.gmane.org) and D. Pym
(d.j.pym-9qr1vRpWqPK1Qrn1Bg8BZw< at >public.gmane.org) by May 20th 2012.

Papers will be reviewed by peers, typically members of
the Programme Committee.

Additional information will be available through WWW address:
http://www.loria.fr/~galmiche/LRPP2012.html.

Hardcopies of the preliminary proceedings will be distributed at the
workshop and a Special Issue of a Journal on these topics is expected
after the workshop.

PROGRAM COMMITTEE

J. Brotherston (Queen Mary, London, UK)
M. Collinson (University of Aberdeen, Scotland)
D. Galmiche (LORIA, Nancy, France: Co-chair)
J. Harland (RMIT University, Melbourne, Australia)
M. Hennessy (Trinity College, Dublin, Ireland)
D. Larchey-Wendling (LORIA, Nancy, France)
F. Pfenning (CMU, Pittsburgh, USA)
D. Pym (University of Aberdeen, Scotland: Co-chair)


IMPORTANT DATES

Submissions:  May 20, 2012
Notifications: May 30, 2012
Final papers: June 10, 2004

Workshop date: July 1st, 2012


MORE INFORMATION

E-mail: Didier.Galmiche-/zGXu1G9BXs< at >public.gmane.org and d.j.pym-9qr1vRpWqPK1Qrn1Bg8BZw< at >public.gmane.org






The University of Aberdeen is a charity registered in Scotland, No SC013683.

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/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

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/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

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/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

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/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

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/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

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/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

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
   from: http://www.logic.at/staff/agata/positions.html.
* Potential applicants are also welcome to send informal inquiries to
   Agata Ciabattoni (agata-DX+603jRYB8< at >public.gmane.org)
* The closing date for applications is Thursday, December 1st 2011.

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%3DADH5u8Vg7IR8k-J4B5Rw0mnLG6fmG_MYTxPGQP4smrJlmxVWL4GJZXMqOJkeYWeWjeSbD6spZdldFrJR5xRKs52HLuMAtD1kqQ31BrL5L1WA69p1cyAIyrZWVRJKos6rhdSi14S-Mq2HZvkUxfR0sEvAo5i8hLwHsg5m8BQLLr6MdqkNU0ZqOoE%26hl%3Den

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 had to compute some money statistics. So, for 
the curious: excluding PhD, and only from 2006, 
deep inference was the main subject in grants for 
overall £4,190,095.25 (at yesterday's exchange 
rate, in euros it's more). I suppose after four 
millions one loses innocence?

-Alessio

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-TgEOGOHWQm0czSlqHMVBIP3zm4ADWneb< at >public.gmane.org>
or
   Kaustuv Chaudhuri <kaustuv.chaudhuri-MZpvjPyXg2s< at >public.gmane.org>

Applications should be sent via email to Lutz Strassburger
<lutz-TgEOGOHWQm0czSlqHMVBIP3zm4ADWneb< at >public.gmane.org> and Kaustuv Chaudhuri
<kaustuv.chaudhuri-MZpvjPyXg2s< at >public.gmane.org>, and should include a CV, a research
statement (1-2 pages), and two recommendation letters. The application
deadline is

*** May 20, 2011 ***

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

Re: Deeper Cuts in Deep Inference

Alessio Guglielmi — 2011-03-17T11:22:31

Hello,

At 21:46 -0300 16/3/11, Bruno Woltzenlogel Paleo wrote:

To clarify: the problem is whether an atomic flow 
and a formula taken as its conclusion, together 
with the association between edges in the flow 
and atom occurrences in the formula, could be 
tested in polynomial time such that the test 
decides if the formula is a tautology.

In other words, the object would be a 
Lamarche-Strassburger proof net with enriched 
identity links, and the problem is to find a 
polynomial-time correctness criterion for it.


1) The flows extracted from proofs have the same 
asymptotic size modulo polynomials (this is a 
fact, the easy paper has been in progress for 
four years but will finally see the light very 
soon).

2) In similar situations in linear proof nets 
polynomial correctness criteria exist.

3) No counterexample emerged yet (but I don't 
know how much effort has been put into this, I 
didn't work on it much myself).


I can't think of any, but I don't understand 
atomic flows very well, so perhaps I'm missing 
something obvious.


Yes, but I think that looking at the proof-search 
problem from a radically different angle than the 
usual one is potentially very fruitful. Flows 
reduce proofs to purely topological objects, so 
they get rid of quite a lot of syntactic chaff, 
and they might help designing proof searchers 
that just have to consider the only really worthy 
matching configurations of atoms, instead of 
pumping around atoms blindly.


I don't know, but you can design your own, 
depending on the properties you're after.

Ciao

-Alessio

Re: Deeper Cuts in Deep Inference

kahramanogullari — 2011-03-17T02:17:46

Hi Bruno,

DPLL
but
moving

It is always possible to add sound and invertible rules to your system to
make it more efficient. However, the main issue here is to achieve
'efficiency' in proof search while preserving as many properties as
possible from those such as modularity, locality, atomicity, symmetry and,
of course, cut-elimination. Splitting technique provides some insight into
this, but in the general setting, this is difficult.

Best regards,
Ozan

Re: Deeper Cuts in Deep Inference

Bruno Woltzenlogel Paleo — 2011-03-17T00:46:16

Hi Alessio,


Ok. Tom was also quite sure that they are.


That's good to know. I hoped so.


Agreed. In principle, to normalize a proof containing the rules I mentioned, we could first replace it by switches and ai^, and then normalize as usual, but of course this wouldn't be as nice as being able to normalize "directly".


What are the arguments in favor of conjecturing that it is a proof system? And what are the arguments against?

Anyway, being a proof system would only mean that its proofs could be checked in polynomial time. Proof search could still be very hard (i.e. if the proof system is not automatizable...)...


In fact, I think that some of the most efficient decision procedures nowadays already use a lot of deep inference. People like to think of DPLL and CDCL as particular strategies for shallow resolution proof search, but things like unit propagation and "decisions" might be more easily understood as a combination of macro-switches and (co)contractions, moving some literals outside the clauses and stacking them on a context for the clauses...


Are there deep inference proof systems that are as close as possible to natural deduction? I know the system of Kai Brünnler and Richard McKinley. Are there others?

Thanks for all the info!

Best regards,

Bruno

Re:Deeper Cuts in Deep Inference

Alessio Guglielmi — 2011-03-15T20:29:45

Hi Bruno,

If I'm not mistaken, the three rules that you propose are, as you 
say, all derivable via switches and cuts (in the sense of SKS cuts 
ai^). They could be further generalised to generic formulae (instead 
of atoms), and still be derivable via switches and cuts.

Conversely, ai^ is an instance of your rules, of course.

As you say, the difference is in the bureaucracy of the proofs: your 
rules are friendlier from the point of view of proof search. However, 
the vanilla ai^ rule seems more manageable and more fundamental for 
investigating normalisation.

It's perhaps interesting to note that all the bureaucracy disappears 
when one turns to atomic flows [1]: all these rules generate the same 
atomic flows. However, we are still far from being able to use atomic 
flows for proof search (it's an open problem whether atomic flows are 
a proof system).

Ozan Kahramanogullari has done extensive work on the design of 
proof-search friendly proof systems, I think all his papers are 
accessible from the deep-inference web page (please let me know if 
anything is missing) [2]. I think it would be interesting to continue 
Ozan's investigation, because there are exponentially shorter 
cut-free proofs in deep inference than in the sequent calculus [3].

Of course, one problem is that the proof-search nondeterminism in 
deep inference seems to be, at first sight, huge and impractical. 
However, it might turn out that eventually deep inference will have 
less nondeterminism than the sequent calculus, because of two recent 
developments:

1) The deep-inference formalism of open deduction eliminates quite a 
lot of bureaucracy in proof construction, and compares favourably to 
the sequent calculus [4].

2) There's a recent result by Anupam Das (still not on the web, as 
far as I know) [5] that shows that in order to access the 
exponentially shorter proofs that I was mentioning above, a very 
small degree of deep inference, just above the sequent calculus, is 
sufficient.

In conclusion: I would expect that some carefully designed cut rules 
like the ones you propose, inside an open-deduction proof system with 
very limited deep inference could make for an excellent proof system 
for proof assistants.

That's all I can think of (in Italy we say: `partire per la tangente').

Ciao,

-Alessio

[1] <http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf>
     <http://www.lmcs-online.org/ojs/viewarticle.php?id=341>
     <http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf>

[2] <http://alessio.guglielmi.name/res/cos/#LD>
     <http://alessio.guglielmi.name/res/cos/#IM>

[3] <http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>

[4] <http://drops.dagstuhl.de/opus/volltexte/2010/2649/>

[5] 
<http://www.bath.ac.uk/comp-sci/people/contact/index.php?contact=Mr_Anupam_Das>


At 15:17 -0300 15/3/11, you wrote:

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 formalized by the inference rule (2) above is a quite natural reasoning pattern. I use it all the time, and I think we can also say that theorem provers implicitly use it whenever they are doing deep replacements during, for example, skolemization.

I guess both (1) and (2) could be simulated in SKS by several applications of the switch rule followed by an application of "ai-up", but this would be quite bureaucratic, in my opinion.

Anyway, these are some things that came to my mind while developing a proof format for an SMT-solver (that does skolemization as a pre-processing step), and I haven't thought much about this yet. So, if you have any comments (e.g. whether it has already been investigated somewhere, whether I am out of my mind and it doesn't make sense to investigate it for some reason,...), please let me know...

Best regards,

Bruno

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 hacking!

-Kai

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

Re: HDR

Laurent Méhats — 2011-01-10T18:09:49

Le 07/01/2011 11:43, Lutz Strassburger a écrit :

Congratulations ! And incidentally, happy new year :)

See you,
Laurent

RE: HDR

Richard Blute — 2011-01-10T08:28:22

I'm sure frogpeople everywhere will be happy to learn that Lutz's habilitation
was a great success. His talk was an excellent advertisement for deep inference 
and categorical logic.

cheers
Rick



________________________________________
From: l. s. [lutz.at.lix-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org] on behalf of Lutz Strassburger [lutz< at >lix.polytechnique.fr]
Sent: Friday, January 07, 2011 5:43 AM
To: Frogs
Subject: [Frogs] HDR

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