gmane.science.mathematics.frogs

Second Call: Workshop on Logics for Resources, Processes and Programs (LRPP 2013)

Pym, Professor David J. — 2013-06-14T18:08:11

Apologies for any cross-postings.

--------------------------------------------------------------------------------------
Call For Papers

Workshop on Logics for Resources, Processes and Programs
(LRPP 2013)

16 September 2013, Nancy, France

(affiliated with Tableaux 2013, Nancy, France)

http://www.loria.fr/~galmiche/LRPP2013.html

Deadline: June 24, 2013
----------------------------------------------------------------------

A one day workshop on `Logics for Resources, Processes, and Programs'
will be held the 16th September 2013 in conjunction with the Tableaux
Conference in Nancy, France, with D. Galmiche and D. Pym as co-chairs.

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); spec

Bruno Woltzenlogel Paleo invited you to Workshop on Proof Compression

Bruno Woltzenlogel Paleo (Google+ — 2013-05-10T10:06:49

Bruno Woltzenlogel Paleo invited you to Workshop on Proof Compression
Mon, September 16, 9:00 AM CEST
Nancy, France

View Invitation:  
https://plus.google.com/_/notifications/emlink?emr=13582153857752024032&emid=CMDjr5qli7cCFaYYQAodDnoAAA&path=%2Fevents%2Fcm5o4cb9g5rbmp43mc8f7gueqm0%3Fauthkey%3DCMuwpNG75fviwgE%26gpinv%3DAMIXal9HmxCFDJYu2YNZ6FJ64pXHAh4mzmmbHD0Bhb4WQoGWYaU54QP-lvpJjBCMU8hX8QQALLZDvOHG-_zBLWrO4UcqVNDxzG1ry_LFoncDlTo8f72q3_g%26gpsrc%3Dgpev0&dt=1368180409794&uob=14
See details in the workshop's page:
http://www.logic.at/people/bruno/MediaWiki/index.php/Third_Workshop_of_the_Amadeus_Project_on_Proof_Compression

Affiliated with Tableaux 2013 (http://tableaux13.loria.fr)
Be thoughtful about who you share this email with; anyone can reshare it.

PhD Research Project: Efficient and Natural Proof Systems

Alessio Guglielmi — 2013-03-18T17:33:33

Hello, could you please help us advertise the 
following position? Ciao,   -Alessio



*** PhD Studentship ***

Research Project: Efficient and Natural Proof Systems
<http://www.cs.bath.ac.uk/ag/ENPS/>

Institution: University of Bath - Department of Computer Science

PhD Supervisors: Alessio Guglielmi and/or Guy McCusker
<http://alessio.guglielmi.name>
<http://www.cs.bath.ac.uk/~gam23/>

Application Deadline: 17 April 2013

Math is growing more complex each day, to the 
point that the assistance of computers is 
becoming necessary even for the most 
theoretically inclined among the mathematicians 
(see this recent article by Natalie Wolchover on 
Wired: <http://is.gd/Qf2qpd>). After centuries of 
producing proofs in our heads and then describing 
them in papers, we are moving fast towards a 
future of proofs conceived by humans together 
with computers, which in turn will guarantee 
their correctness and availability.

But what is a proof? What could a common language 
between humans and computers be? A sat

Two preprints

Anupam Das — 2013-02-22T19:03:49

Dear all,

I would like to advertise the following two preprints (abstracts below):

The pigeonhole principle and related counting arguments in weak monotone
systems
http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf

Rewriting with linear inferences in propositional logic
http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf

Any feedback would be greatly appreciated. I would also like to thank those
on this list who have already responded to preliminary versions of these
works for their helpful comments.

Kind regards,
Anupam


The pigeonhole principle and related counting arguments in weak monotone
systems

We construct quasipolynomial-size proofs of the propositional pigeonhole
principle for weak fragments of the monotone sequent calculus, implemented
in the simplest deep inference system for propositional logic. The argument
given, inspired by previous work on the monotone calculus, utilizes
propositional formulae that compute certain counting f

Linear inferences and derivations 3

Anupam Das — 2013-02-19T15:23:12

[This is the third of 3 emails to the Frogs list concerning linear 
inferences and derivations in deep inference. The first is about linear 
inferences that are independent of the usual basis {switch, medial}. The 
second concerns the size of linear derivations in deep inference, in the 
presence of units, and the third will present recent work towards 
efficiently automating the checking and search of new linear inferences.]

Dear all,

I would like to advertise the following work of Alvin Sipraga (title and 
abstract below):

http://arcturus.su/mimir/autolininf.pdf

and website:

http://arcturus.su/mimir/

Alvin did an undergraduate project with me last year and this work 
implements an approach towards conducting proof-search in the linear 
fragment of propositional deep inference. In upcoming work it is proved 
that proof-search in arbitrary Gentzen/Frege systems can be reduced (in 
polynomial-time) to proof-search in the linear fragment.

Kind regards,
Anupam


An automated search of linear inference ru

interana: interactive prover for Multiplicative Linear Logic

Ozan Kahramanogullari — 2013-02-18T14:46:59

Hello,

The members of this group might be interested in the following paper
and the tool. The tool implements the ideas in the paper.  Comments on
both are most welcome.

Kind regards,
Ozan

---
Interaction and Depth against Nondeterminism in Proof Search

Deep inference is a proof theoretic methodology that generalises the
standard notion of inference of the sequent calculus, whereby
inference rules become applicable at any depth inside logical
expressions. Deep inference provides more freedom in the design of
deductive systems for different logics and a rich combinatoric
analysis of proofs. In particular, construction of exponentially
shorter analytic proofs becomes possible, however with the cost of a
greater nondeterminism than in the sequent calculus. In this paper,
building on our previous work on proof search with deep inference, we
show that, by exploiting an interaction and depth scheme in the
logical expressions, the nondeterminism in proof search can be reduced
without losing the shorter proofs a

Two recent books

Alessio Guglielmi — 2013-01-29T15:47:29

Hello,

Two theses are now available as books. The one with the yellow-eyed 
frog costs 20 EUR more:

<http://is.gd/KHe72o>
<http://is.gd/vvrnOA>

Ciao,

-Alessio

Postdoc position in proof theory in Paris

Lutz Strassburger — 2013-01-10T12:35:40


--------------------------------------------------------
  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 INRIA and 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.

The successful candidate will be working within the PARSIFAL team.

<http://team.inria.fr/parsifal/>

Starting date should be between February and April 2013.

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.

Re: Post-doc in Bath on the semantics of a

Alessio Guglielmi — 2013-01-09T17:34:15

Hello, the application web page is now online, with more information: 
<https://www.bath.ac.uk/jobs/Vacancy.aspx?ref=VH1457>. Ciao, 
-Alessio

Re: Post-doc in Bath on the semantics of a

Alessio Guglielmi — 2013-01-07T17:04:53

Dear Karn,

No, there are no implementations in the project as is, but, of 
course, there is sufficient flexibility to include one if that will 
turn out to be a good idea.

Ciao,

-Alessio

Re: Post-doc in Bath on the semantics of a bureaucracy-free formalism

Karn Kallio — 2013-01-04T20:33:16

Does the EPSRC project include a software implementation (eg in Isabelle) of 
Formalism B?

Saludos,
Karn

Post-doc in Bath on the semantics of a bureaucracy-free formalism

Alessio Guglielmi — 2013-01-04T15:31:41

Hello,

We have a new project starting this February. We are looking for 
somebody who could help us use semantics to design a formalism that 
is free of every kind of known bureaucracy. The official advert, with 
salary and instructions on how to apply, will probably be ready this 
Monday and I will send it to the major mailing lists, but Frogs 
deserves a preview.

I'll be happy to answer any questions regarding this position and I 
encourage you to get in touch if you are interested. If you know 
somebody who might be interested, please let them know as soon as 
possible, because we aim to hire in the next few hours.

Ciao,

-Alessio


Research officer (post-doc), proof theory and semantics (fixed term 
for up to three years)

The post is associated with the three-year EPSRC project "Efficient 
and Natural Proof Systems". The project is about developing an 
ambitious, modern semantic-motivated proof theory for representing 
natural proofs of minimal complexity.

We are looking for a researcher who can wor

PhD opportunities

Alessio Guglielmi — 2012-11-18T19:17:25

Hi,

If any of you has outstanding students that might be interested in a 
PhD in our Math Foundations group in Bath, please encourage them to 
apply as specified below. Deadline: 18th December. I'll be happy to 
answer questions and help with the application.

These are the only open studentships for this year. Most likely there 
will be more positions available in the next months, but these will 
be on specific projects that we hope will be financed.

The logic & semantics people of our group are:

   Paola Bruscoli
  Anupam Das
Alessio Guglielmi
  Willem Heijltjes
     Jim Laird
     Guy McCusker
    John Power
     Cai Wingfield

Ciao,

-Alessio


At 14:34 +0000 14/11/12, Jim Laird wrote:
>Jim

Linear inferences and derivations 2

Anupam Das — 2012-09-26T17:10:04

[This is the second of 3 emails to the Frogs list concerning linear 
inferences and derivations in deep inference. The first is about linear 
inferences that are independent of the usual basis {switch, medial}. The 
second concerns the size of linear derivations in deep inference, in the 
presence of units, and the third will present recent work towards 
efficiently automating the checking and search of new linear inferences.]

Dear all,

I would like to advertise the following note (title and abstract below):

http://www.anupamdas.com/items/LinCompDI/LinCompDI.pdf

This note forms part of ongoing work with Paula Bruscoli, Alessio 
Guglielmi and Lutz Strassburger [BGS] on the size of linear derivations 
in deep inference. In particular we focus on the situation when units 
are present, and reduce it to the case when there are no units, internal 
to the {switch, medial} system, whence better bounds can be obtained by 
the work of [BGS].

Kind regards,
Anupam

The size of linear derivations in deep inference

Linear inferences and derivations 1

Anupam Das — 2012-09-26T16:22:22

[This is the first of 3 emails to the Frogs list concerning linear 
inferences and derivations in deep inference. The first is about linear 
inferences that are independent of the usual basis {switch, medial}. The 
second concerns the size of linear derivations in deep inference, in the 
presence of units, and the third will present recent work towards 
efficiently automating the checking and search of new linear inferences.]


Linear inference rules are negation-free inferences where each variable 
appears exactly once in both the premiss and conclusion. In deep 
inference we often consider the following rules:

          A ^ [B v C]             (A ^ B) v (C ^ D)
switch --------------    medial -------------------
         (A ^ B) v C              [A v C] ^ [B v D]


But there are many more that one may consider, for example by composing 
the two rules above in various combinations. But as Strassburger shows 
in his paper Extension Without Cut, these two rules are not complete for 
the set of linear inferen

Re: Quasipolynomial cut-elimination in CoS

Tom Gundersen — 2012-08-03T11:10:16

Dear Giorgi,

On Fri, Aug 3, 2012 at 8:18 AM, Giorgi Japaridze
<giorgi.japaridze-Knhbg2ZS0VuFhjwBz98joA< at >public.gmane.org> wrote:

A cut-free SKS proof can be transformed to a KS+cocontraction proof
without increasing it's size. Simply permute all coweakenings "up" in
the proof. What will happen is:
1) coweakenings simply pass through linear rules
2) coweakening meeting a weakening or a cocontraction erase both rules
3) coweakening meeting a contraction removes the contraction and puts
two coweakenings in its place
4) coweakening meeting an axiom will erase the coweakening and the
axiom and replace them with a weakening


Proposition 7.3.1 on page 78 of
<http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf>;
alternatively
Theorem 4.12 on page 19 of
<http://www.lmcs-online.org/ojs/viewarticle.php?id=341>.

Cheers,

Tom

Quasipolynomial cut-elimination in CoS

Giorgi Japaridze — 2012-08-03T06:18:07

Dear all,



Does KSg+cocontraction or KS+cocontraction allow quasipolynomial cut elimination? (I know that SKS does, but it is not "analytic" because of coweakening.)



If yes, any detailed references, including page and/or theorem numbers, will be greatly appreciated.





Giorgi Japaridze
http://www.csc.villanova.edu/~japaridz/

Note: Pigeonhole principle in deep inference

Anupam Das — 2012-06-04T19:45:11

I have written a short note on the proof complexity of the propositional 
pigeonhole principle for `cut-free' deep inference:

http://www.anupamdas.com/items/PHPProofs/PHPProofs.pdf

An outline of the material is given below this message.

Together with some other results, I am planning to expand this to a full 
article on the complexity of combinatorial principles in deep inference, 
using broadly the same techniques as presented here.

Unfortunately the note currently relies on much of the existing 
literature, hindering the accessibility of any article derived from it.

I would appreciate any feedback on this, especially regarding any 
possible simplifications or existing confusions.

Kind regards,
Anupam

A note on proofs of the pigeonhole principle in deep inference.

The propositional pigeonhole principle (PHP) is known to have 
polynomial-size proofs in systems with cut [Bus], and 
quasipolynomial-size ( n ^ (log^c n) ) proofs in deep inference systems 
that are cut-free but exhibit dag-like behaviour

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; ve

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/>
Microsof

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/notifica