Small ParisVienna Workshop on "The Realm of Cut
Elimination"
Palaiseau
May 14, 2007
Presentation
This workshop is part of the bilateral PAI project "The Realm of Cut
Elimination" beween research groups in Paris (LIX and PPS) and Vienna (Theory and Logic Group).
Participants
Matthias Baaz (Theory and Logic Group, Vienna)
David Baelde
(LIX, Palaiseau)
Agata Ciabattoni (Theory and Logic Group, Vienna)
Olivier
Delande (LIX,
Palaiseau)
Gilles
Dowek (LIX,
Palaiseau)
Dov Gabbay
(Group of
Logic, Language and Computation, King's College London)
Valentina Gliozzi
(Dipartimento di Informatica
Università degli Studi di Torino)
Stefan Hetzl (Theory and Logic Group, Vienna)
Dale
Miller (LIX,
Palaiseau)
Vivek Nigam (LIX, Palaiseau)
Nicola Olivetti (LSIS, Marseille)
Michel Parigot (PPS, Paris)
Vincent Risch (LSIS, Marseille)
Alexis Saurin (LIX, Palaiseau)
Lutz
Straßburger (LIX, Palaiseau)
Programme
Abstracts

David Baelde,
LIX, Ecole Polytechnique
Title: Least and greatest fixed points in linear logic
Abstract:
The firstorder theory of MALL (multiplicative, additive linear logic)
over only equalities is an interesting but weak logic since it cannot
capture unbounded (infinite) behavior. Instead of accounting for
unbounded behavior via the addition of the exponentials (! and ?),
we add least and greatest fixed point operators and develop
a proof theory for this natural setting for induction and
coinduction. We show that this logic, named muMALL, satisfies
the cutelimination elimination theorem and has a complete, focused
proof system. We then consider applying these results about muMALL
to derive a focused proof system for an intuitionistic logic extended with
induction and coinduction. The traditional approach to encoding
intuitionistic logic into linear logic relies heavily on using
the exponentials, which unfortunately weaken the focusing discipline.
We get a better focused proof system by observing that certain
fixed points satisfy the structural rules of weakening and contraction
(without using exponentials). The resulting focused proof system
for intuitionistic logic is closely related to the one implemented
in Bedwyr, a recent model checker based on logic programming.
We discuss how our proof theory might be used to build a computational
system that can partially automate induction and coinduction.

Olivier Delande,
LIX, Ecole Polytechnique
Title: Game semantics for propositional multiplicativeadditive linear logic
Abstract:
We present a twoplayer game setting in which winning
strategies can be seen as focused proofs in propositional MALL. We
adopt a neutral approach to proof and refutation and point out
symmetries of the proof system. This workinprogress extends work by
Miller & Saurin ("A game semantics for proof search: Preliminary
results" in Mathematical Foundations of Programming Semantics, 2005)
by developing a way to encode unrestricted uses of the multiplicative
connectives.

Alexis Saurin,
LIX, Ecole Polytechnique
Title: From proofs to focused proofs: a modular proof of Focalization in
Linear Logic
Abstract:
Probably the most significant result concerning cutfree sequent
calculus proofs in linear logic is the completeness of focused
proofs. This completeness theorem has a number of proof theoretic
applications
 e.g. in games semantics, Ludics, and proof search  and more
computer science applications  e.g. logic programming,
callbyname/value evaluation. Andreoli proved this theorem for
firstorder linear logic 15 years ago. We give a new proof of the
completeness of focused proofs in terms of proof transformation. A
key component of our proof is the construction of a focalization
graph which provides an abstraction over how focusing can be
organized within a given proof. Using this graph abstraction allows
us to provide a detailed study of atomic bias assignment in a way
more refined that is
given in Andreoli's original proof. Focalization graphs can be used
to justify the introduction of an inference rule for multifocus
derivation: a rule that should help us better understand the
relations between
sequentiality and concurrency in linear logic.

Matthias Baaz,
Computational Logic Group, Vienna
Title: Cutelimination and epsilonelimination
Abstract:
We compare these most ancient methods of cutelimination and consider their
extension to nonclassical logics.

Gilles Dowek,
LIX, Ecole Polytechnique
Title: SuperConsistency and Normalization
Abstract:
We extend the notion of Heyting algebra to a notion of truth
values algebra and prove that a theory is consistent if and only if
it has a Bvalued model for some non trivial truth values
algebra B. A theory that has a Bvalued model for all
truth values algebras B is said to be superconsistent.
We prove that superconsistency is a modeltheoretic sufficient
condition for strong normalization.

Stefan Hetzl,
Theory and Logic Group, Vienna
Title: Proof Transformations and Structural Invariance
Abstract:
CutElimination by Resolution (Baaz, Leitsch, 2000) is a cutelimination method
that works by extraction of a characteristic clause set from a proof with cuts.
Any resolution refutation of this set of clauses can then serve as a skeleton
for a cutfree proof.
In this talk, we define an improved variant of this characteristic clause set:
the profile of a proof. It has the property that it is invariant under rule
permutations which  as a corollary  shows that two proofs having the same
proof net have the same profile.
But the abstraction from the concrete structure of the proof is much stronger:
We define a large class of proof transformations ("simple transformations")
including e.g. the transformation to negationnormalform and show that the
profile is not changed if the cutformulas in the proof are subjected to such
transformations. This shows that the profile can be considered a structural
invariant of a proof w.r.t such transformations.
As two proofs having the same profile have the same behavior
w.r.t. cutelimination, proofs obtained by these simple transformations can be
considered equal in this sense. We will also give a comparison to related
work by Danos, Joinet and Schellinx on computational isomorphisms in
classical logic.

Vivek Nigam,
LIX, Ecole Polytechnique
Title: Incorporating tables into proofs
Abstract:
We consider the problem of automating and checking the use of
previously proved lemmas in the proof of some main theorem. In
particular, we shall call the collection of such previously proved
results a table and use a partial order on the table's entries
to denote the (provability) dependency relationship between tabled
items. Tables can arise in a number of situations: in automated
deduction via previously proved subgoals or in interactive theorem
proving via a sequence of lemmas introduced by a user to direct the
proof system towards its final theorem. We link tables involving
literals with sequent calculus proofs using two ideas. First, cuts
are used to incorporate tabled items into a proof: one premise of the
cut requires a proof of the lemma and the other branch of the cut
inserts the lemma into the set of assumptions. Second, in order to
require that that inserted lemma is not reproved, we exploit the fact
that in focused proofs, atoms can have different polarity.
As we shall see in two specific setting, such a use of focused proofs
along with atoms of either positive or negative polarities allows
tables to be merged with proofs in such a way that simple logic
engines that do focused proof search (such as logic programming
interpreters) will be able to check proofs for correctness with
guarantees that previous work will not be redone. We illustrate these
ideas with tables of literals in two specific logics: one involving
Horn clauses and the other that generalizes Horn clauses with
negationasfinite failure. We also discuss how such integration of
tables into proof can, at times, significantly compress proofs and
discuss how this work might be used within a proof carry code setting.

Nicola Olivetti,
LSIS, Marseille
Title: Analytic Calculi for Kraus Lehmann Magidor
Logics
Abstract:
We present tableaux calculi for the logics of default reasoning by
Kraus, Lehmann and Magidor (KLM), namely: Preferential, Rational,
Cumulative, and Loop Cumulative logic. The calculi are based on a
novel modal interpretation of these logics, and more specifically, on
a connection with GödelLöb
modal logic of provability. In all cases,
except Cumulative logic, the calculi are cutfree and hence strongly
analytical. In case of the weakest Cumulative logic, a cutrule is
needed; this rule may however be restricted (nontrivially) in an
analytic way. Our calculi are the base of decision procedures that
match the complexity bounds, for the logics whose bounds are known,
and allow to obtain unpreviously known complexity bounds for some
other logics.

Dov Gabbay,
King's College, London
Title: tba
Abstract:
tba
Venue
The workshop will be held at Laboratoire d'Informatique
d'École Polytechnique (LIX). Directions can be found here.
Organization
Lutz Straßburger