Small Workshop on "Theory and Application of Deep Inference"
Palaiseau
June 21, 2007
Presentation
Participants
David Baelde
(LIX, Palaiseau)
Guillaume Burel
(LORIA, Nancy)
Kai Brünnler
(Universität Bern)
Joëlle Despeyroux
(INRIA Sophia Antipolis)
Christopher Dutchyn
(University of Saskatchewan)
Alessio Guglielmi
(University of Bath)
Tom E. Gundersen
(University of Bath)
Dominic Hughes
(Stanford University)
François
Lamarche
(LORIA, Nancy)
Séverine Maingaud (PPS, Paris)
Richard McKinley
(Universität Bern)
Dale
Miller (LIX,
Palaiseau)
Laurent
Méhats
Michel Parigot (PPS, Paris)
Sylvain Pogodalla
(LORIA, Nancy)
Christian Retoré (LABRI, Bordeaux)
Alexis Saurin (LIX, Palaiseau)
Lutz
Straßburger (LIX, Palaiseau)
Programme
Every speaker has a slot of 40 minutes. These 40 minutes consist of a
talk of 25 minutes and a following discussion of 15 minutes.
Abstracts
-
Kai Brünnler
Title: Deep sequents for modal logic
Abstract:
Let a pure proof system informally be one in which inference rules
only operate on things which correspond to formulas of the logic.
Gentzen's sequent calculus for classical logic is pure: the commas on
the left are conjunction, the ones on the right conjunction and they
are separated by an implication. All systems in the calculus of
structures are of course pure.
There are many approaches to a proof theory for modal logics. The most
successful, by several criteria, is the one based on labelled
sequents, where in some sense Kripke semantics is built into the proof
system. These proof systems are not pure. The question is whether we
can build a similarly successful pure proof theory. I'll talk about
some progress towards that.
-
Guillaume Burel
Title: Proof-length speed-ups
in deduction modulo
Abstract:
In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37
years before: there exists arithmetical
formulae that are provable in first order arithmetic, but whose
shorter proof in second order arithmetic is arbitrarily smaller than
any proof in first order. On the other hand, resolution for higher
order logic can be simulated step by step in a first order narrowing
and resolution method based on deduction modulo, whose paradigm is to
separate deduction and computation to make proofs clearer and shorter.
We first prove that it is possible to find formulae whose smaller
proof in natural deduction modulo a very simple rewrite system is
unboundedly smaller than any proof in pure natural deduction. Then, we
show that i+1-th order arithmetic can be linearly simulated into
i-th order arithmetic modulo some confluent and terminating rewrite
system. We also prove that there exists a speed-up between i-th
order arithmetic modulo this system and i-th order arithmetic
without modulo. These two results allows us to prove that the
speed-up conjectured by Gödel does not come from the deductive part of
the proofs, but can be expressed as simple computation, therefore
justifying the use of deduction modulo as an efficient first order
setting simulating higher order.
-
Tom E. Gundersen
(joint work with Alessio Guglielmi)
Title: Normalisation Control in Deep Inference Via Atomic Flows
Abstract:
We introduce diagrams, called 'atomic flows', that forget much of the
syntactic structure of derivations and only retain causal relations
between atoms. Using atomic flows on propositional logic, we can
design and control several normalisation procedures. In particular, we
can obtain cut elimination as a special case of more general normal
forms. This technique only relies on substituting derivations in the
place of atoms, similarly to natural deduction, and not on permuting
inference steps, as in the sequent calculus. Because they abstract
away from most syntactic details, atomic flows allow for very simple
control of normalisation procedures, which would be otherwise
cumbersome in the bare syntax. We operate in deep inference, a very
general methodology, where normalisation is more difficult to control
than in other syntactic paradigms.
-
Dominic Hughes
Title: Combinatorial proof invariants
Abstract:
Proofs Without Syntax [Ann. Math. '06]
introduced polynomial-time checkable combinatorial proofs for
classical propositional logic. This sequel approaches Hilbert's
24th
Problem with combinatorial
proofs as abstract invariants for sequent calculus proofs, analogous
to homotopy groups as abstract invariants for topological spaces.
The paper lifts a simple, strongly normalising cut elimination from
combinatorial proofs to sequent calculus, factorising away the
mechanical commutations of structural rules which litter traditional
syntactic cut elimination.
Sequent calculus fails to be surjective onto combinatorial proofs: the
paper extracts a semantically motivated closure of sequent calculus
from which there is a surjection, pointing towards an abstract
combinatorial refinement of Herbrand's
theorem.
(Article available on the web: Pdf)
-
Richard McKinley
Title: Herbrand's Theorem and the sequent calculus
Abstract:
A typical proof of Herbrand's theorem involves Gentzen's Midsequent
theorem (the sharpened Hauptsatz), but such a proof does not yield the
full theorem -- rather, it yields the theorem for sequences of
formulae in prenex normal form.
In "An introduction to proof theory" (Handbook of Proof Theory) Buss
gives a proof of the full theorem using the notion of an "Herbrand
Proof", which is incorrect. I will give a corrected proof: a
procedure which, for any cut-free proof in GS yields an Herbrand proof
of the same conclusion. In order to show admissibility of the
contraction rule we use a notion of "deep contraction" similar to that
of the calculus of structures. I will then extend this procedure to
proofs containing cuts, effectively giving a cut-elimination procedure
for Herbrand proofs.
Finally, I will give some examples of the use of Herbrand proofs as an
invariant on GS derivations, showing which proofs are identified.
-
Laurent
Méhats
Title: Categorical equivalences on derivations in
intuitionistic multiplicative linear logic with unit
Abstract:
Structural proof theory applies to category theory insofar as its
syntactical methods enable the study of terms representing morphisms in free
categories. As to category theory, it provides relevant semantics to
equivalences of derivations usually considered in proof theory. I will
illustrate this interplay by addressing the question of coherence in free
and non-free symmetric monoidal closed categories (SMCCs), and of its
proof-theoretical formulation in the sequent calculus for intuitionistic
multiplicative linear logic (IMLL) with unit. The equality of canonical
natural transformations in a SMCC model induces an equivalence on terms in
the free SMCC that can be formulated as an equivalence on derivations. The
proof-theoretical analysis of such equivalences leads to their
axiomatization by sets of "critical pairs" of derivations. In the free case,
this axiomatization implies that the equivalence induced by the SMCC
structure on cut-free derivations coincides with inter-permutability,
suggesting a way towards the definition of proof-nets for IMLL with unit.
-
Christian Retoré
Title: Perfect matchings and directed cographs:
proofnets for pomset logic and the origins of deep inference
Abstract:
In this talk I will recall pomset logic, in a graph theoretical
version which encodes structured contexts a primitive system which
lead Alessio Guglielmi to BV-calculus.
I will present the proof-net calculus with cut-elimination and its
denotational semantics for which we can show that a proofnet is
correct if and only the computation of its semantics is an allowed
semantic object.
I will end with an old but still open graph theoretical conjecture
which would ensure the equivalence of Pomset Logic and BV.
-
Lutz
Straßburger
Title: From deep inference to proof nets, revisited
Abstract:
An important observation of "From deep
inference to proof nets" is that cut elimination is losing
information, when seen from the viewpoint of buraucracy A, B, and C in
deep inference derivations.
In this talk I will show that the slogan "cut elimination is losing
information" is independent from deep inference. I will also show how
arbitrary deductive proofs (in sequent calculus, calculus of
structures, or in Frege systems) are translated into proof
graphs. This includes the extension rule, which can be made
independent from the cut.
Venue
See also
Social Event
Organization