Paris-Vienne Workshop 2004 : Abstracts

Matthias Baaz Skolem Functions: the hidden quantifier complexity of proofs

In this lecture we compare the model theoretic and the proof theoretic approach to Skolem functions. We describe general conditions for re-Skolemization and demonstrate by analyzing these algorithms, that large classes of functions can serve as Skolem functions in the proof theoretic sense (Hilberts systems of disparate functions.).This leads us to the discussion of hidden Skolem-functions in mathematical proofs. Candidates are especially trigonometric functions in proofs of elementary geometry (RCF). We construct decidable classes from these observations. Finally we describe a new method of Skolemization for Intuitionistic Logic developed together with Rosalie Iemhoff.

Arnold Beckmann Viewing proofs in bounded arithmetic as programs

Bounded arithmetic theories are first order theories of arithmetic which are strongly connected to low level complexity. E.g., it is possible to capture the polynomial time computable functions as a class of definable functions in some bounded arithmetic theory (cf. [1]).
In this talk we will discuss how proofs in bounded arithmetic theories can directly be viewed as programs, and how known connections of bounded arithmetic theories to propositional proof systems ([2],[3]) immediately give upper bounds on the complexity of such functions.
[1] S. Buss: Bounded Arithmetic. Studies in Proof Theory. Lecture Notes, 3. Bibliopolis, Naples, 1986.
[2] A. Beckmann: Dynamic ordinal analysis. Arch. Math. Logic 2003, 42: 303-334.
[3] Arnold Beckmann and Jan Johannsen: Bounded Arithmetic and Resolution-Based Proof Systems. Collegium Logicum Volume 7: ESSLLI 2003 - Course Material III. KGS Wien, 2004.

Kai Brünnler Deep Inference and Cut Elimination for Predicate Logic

In my thesis I gave a proof of cut elimination for the presentation of predicate logic in the calculus of structures. This proof is indirect: it translates a proof to the sequent calculus by introducing lots of new cuts, makes use of Gentzen's cut elimination result, and translates back the cut-free proof. My talk will be about a new, direct proof without any reference to the sequent calculus.

Agata Ciabattoni Automated Generation of Analytic Calculi for Logics with Linearity

We show how to automatically generate analytic hypersequent calculi for a large class of logics containing the linearity axiom (lin) (A -> B) \/ (B -> A) starting from existing cut-free sequent calculi for the corresponding logics without (lin).

Chris Fermüller Revisiting Giles: On Bets, Dialogue Games, Fuzzy logics, and Hypersequents

Already in the 1970s Robin Giles demonstrated that a combination of Lorenzen's dialogue game with a specific way to calculate expected losses associated with bets on the results of `atomic experiments' leads to a characterization of Lukasiewizc logic. We extend Giles remarkable result in several ways that lead to a characterization of other important fuzzy logics, including Gödel and Product logic. In particular we indicate how one can obtain uniform hypersequent calculi from a systematic search for winning strategies in appropriate versions of the game.

Alessio Guglielmi Reasons and methods of deep inference

Structural proof theory suffers from excessive rigidity in the traditional formalisms, like sequent calculus and natural deduction. This rigidity manifests itself in several fashions, among which: 1) manipulating proofs in desired ways is sometimes impossible, for example permuting inference rules which should be permutable but are not; 2) designing deductive systems with worthy properties is impossible, for example employing only local or atomic rules; 3) there is only one reasonable notion of normal form, while several would be useful.
Deep inference provides for an escape from all those constraints, by inspiring the design of formalisms which are at the same time simpler and more general than all others, like the calculus of structures (CoS). Deep inference opens up the way for new possibilities, especially a satisfying settling of the open question of identity of proofs. Along the way, we obtained already several results. The most spectacular is the presentation in CoS of several logics--classical, linear, modal, non-commutative and others---in analytic deductive systems enjoying properties of locality, modularity and uniformity, impossible in other formalisms. CoS also inspired the conception of a new class of proof nets and a new semantics for classical proofs which elegantly gets around the so-called Lafont and Girard counterexamples.
More information on deep inference and CoS is at http://alessio.guglielmi.name/res/cos

Alexander Leitsch CERES: Cut-Elimination by Resolution

We present a cut-elimination method for Gentzen's LK which is based on the resolution calculus. The first step consists in a structural analysis of a proof P of a sequent S and the extraction of a clause term X(P). X(P) encodes an abstract structure of the derivations of cut formulas and represents an unsatisfiable set of clauses C(P). A resolution refutation R of C(P) then serves as a skeleton of an LK-proof P' of S with only atomic cuts. P' itself can be obtained from the resolution refutation R via so-called projections of the proof P w.r.t. the clauses in C(P). The main algorithmic advantage of this method, called CERES, lies in the integration of efficient theorem provers (constructing the resolution refutation R). Moreover the clause term of the proof paves the way for an algebraic analysis and a mathematical comparison of different cut-elimination methods. In particular it can be shown that CERES asymptotically outperforms a large class of cut-elimination methods including the methods of and Gentzen Tait and the cut-projection method.

Stéphane Lengrand Explicit operators and proof-nets

We present a simple term language with explicit operators for erasure, duplication and substitution enjoying a sound and complete correspondence with the intuitionistic fragment of Linear Logic's Proof Nets. We establish some fundamental properties such as confluence, Preservation of Strong Normalisation, strong normalisation of well-typed terms and step by step simulation of beta-reduction.
This formalism is the first calculus with explicit substitutions having full composition and preserving strong normalisation. The confluence on open terms is conjectured. In contrast to lambda x, adding the introduction and elimination rules of the intersection types yields a typing system characterising strongly normalising terms.

Norbert Preining Gödel logics and Kripke frames (joint work with Arnold Beckmann)

That there is a strong relation between linear Kripke frames and (the truth value sets of) Gödel logics is well known, but the exact correlation has never been thoroughly discussed. We will present the exact correspondences of these two semantics.

Clemens Richter The Cut-Elimination Program CERES

CERES is a resolution-based method for the elimination of nonatomic cuts in LK-proofs. The use of resolution suggests a computational implementation able to handle rather complex cut-elimination problems. In this talk we present an implementation of CERES, in particular the basic algorithms, the input format and the integration of the well-known automated theorem prover Otter. Finally we demonstrate the program on some examples.

Sebastiaan Terwijn Logic and probabilistic induction

We discuss the probabilistic induction of logical formulas. First we give a probabilistic interpretation of such formulas based on the sampling of atomic truths from a unknown given model. We compare the resulting logic to classical and intuitionistic logic. We then develop a notion of probabilistic induction based on Valiants notion of pac-learning and discuss the induction of logical formulas in this context.

Olivier Laurent Polarized Proof-Nets.

We will present the proof-net syntax of linear logic, explaining why the polarization constraint is useful and meaningful in this context. We will focus on the correctness criterion and on cut-elimination. Finally we will discuss the relation with the lambda-calculus and the way this relation can be extended to the lambda-mu calculus.

Michel Parigot On constructive existence.

I will discuss a characterization of constructive existence in classical logic due to Matthias Baaz and Christian Fermueller. I will give a simple proof of it based on cut elimination which allow to extend this characterization to any logic having a reasonable cut elimination theorem.