Small Paris-Vienna 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 first-order 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
co-induction. We show that this logic, named muMALL, satisfies
the cut-elimination 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 co-induction. 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 co-induction.
-
Olivier Delande,
LIX, Ecole Polytechnique
Title: Game semantics for propositional multiplicative-additive linear logic
Abstract:
We present a two-player 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 work-in-progress 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 cut-free 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,
call-by-name/value evaluation. Andreoli proved this theorem for
first-order 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: Cut-elimination and epsilon-elimination
Abstract:
We compare these most ancient methods of cut-elimination and consider their
extension to non-classical logics.
-
Gilles Dowek,
LIX, Ecole Polytechnique
Title: Super-Consistency 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 B-valued model for some non trivial truth values
algebra B. A theory that has a B-valued model for all
truth values algebras B is said to be super-consistent.
We prove that super-consistency is a model-theoretic sufficient
condition for strong normalization.
-
Stefan Hetzl,
Theory and Logic Group, Vienna
Title: Proof Transformations and Structural Invariance
Abstract:
Cut-Elimination by Resolution (Baaz, Leitsch, 2000) is a cut-elimination 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 cut-free 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 negation-normal-form and show that the
profile is not changed if the cut-formulas 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. cut-elimination, 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
negation-as-finite 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ödel-Löb
modal logic of provability. In all cases,
except Cumulative logic, the calculi are cut-free and hence strongly
analytical. In case of the weakest Cumulative logic, a cut-rule is
needed; this rule may however be restricted (non-trivially) 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