Last CFP: Workshop on Logics for Resources, Processes and Programs (LRPP 2012)

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

Announcement

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@...)
* The closing date for applications is Thursday, December 1st 2011.

Bruno Woltzenlogel Paleo invited you to join him on Google+

Marketing

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

--------------------------------------------------------
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@...>
or
   Kaustuv Chaudhuri <kaustuv.chaudhuri@...>

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

*** May 20, 2011 ***

Sophia Strassburger

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

Hi Bruno,

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

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 

Deeper Cuts in Deep Inference

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

Facebook Pages on Logical Subjects

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

--

-- 

inquiry list: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
knol: http://knol.google.com/k/-/-/3fkwvf69kridz/1
oeiswiki: http://www.oeis.org/wiki/User:Jon_Awbrey

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