Workshop STRUCTURAL

Paris, June 15-17 2011

175, rue du Chevaleret, Paris

Metro Chevaleret, line 6

Supported by: ANR-FWF project STRUCTURAL and Kurt Gödel Society

Talks
Programme
Venue

Talks :

• Matthias Baaz (Vienna University of Technology): The epsilon-calculus in non-classical logics
• Thomas Ehrhard (PPS): A stack-based classical calculus
• Oliver Fasching (Vienna University of Technology): Phase transitions between Goedel logic and Lukasiewicz logic
• Chris Fermüller (Vienna University of Technology): How to justify your favorite logical system? - A case study
• Nicolas Guénot (LIX): Nested Proof Search as Reduction in the lambda-calculus
• Tom Gundersen (PPS): A tentative atomic calculus for natural deduction
• Hugo Herbelin (PPS / INRIA - πr²): On the computational content of Gödel's completeness theorem
• Stefan Hetzl (PPS): Towards algorithmic cut-introduction
• Thierry Joly (PPS): Combinatory Head Reduction, 80 years after Curry
• Chuck Liang (LIX): A Kripke Semantics and Sequent Calculus for Combining Classical and Intuitionistic Logics
• Tomer Libal (Vienna University of Technology): Second order unification with constraints
• Richard McKinley (University of Bern): Canonical, polytime checkable proof-nets for classical logic: now with cut-elimination!
• Dale Miller (LIX): Reasoning about Computations Using Two-Levels of Logic
• Georg Moser (Innsbruck University): The Epsilon Theorems and Herbrand Complexity
• Giselle Reis (Vienna University of Technology): Specification of Systems in Linear Logic with Subexponentials
• Lutz Strassburger (LIX): NEL
• Kazushige Terui (RIMS, Kyoto University): An algebraic approach to proof theory for substructural logics.

Programme:

Wednesday, June 15

Thursday, June 16

Friday, June 17

Abstracts:

Abstract: We prove that the first epsilon theorem does not hold for all logics devoid of fork sentences. The reason is, that the critical formulas imply under fairly weak conditions all classically valid quantifier shift rules. We show, that intuitionistic first order logic extended by epsilon symbols and critical formulas is conservative over intutionistic logic with all classically valid quantifier shift rules, providing the other direction for superintuitionistic logics.
An unexplored research direction omitting impredicative critical formulas might reestablisch the first epsilon theorem for systems with linearity. .

Abstract: We introduce a stack-based classical calculus derived from Parigot's λµ-calculus, a type system for this calculus, its operational properties (Church-Rosser, normalization) and its denotaional semantics.

Abstract: . Gödel logic and Łukasiewicz logic are, together with product logic, the three main t-norm-based fuzzy logics. The validity of formulae in the propositional fragments of these logics can be exactly characterised by calculi that result from Hájek's basic logic by adjunction of a single axiom scheme. In first-order logic, the situation is quite different: Gödel logics admits a proof-system that is sound and complete because of its order-theoretic nature and its close relationship to intuitionistic logic, but Łukasiewicz logic cannot have such a proof-system due to a result by Scarpellini. In fact, Ragaz proved the validity problem for Łukasiewicz logic to be Pi_2-complete. We investigate this phase transition in the sense of Weiermann and introduce an extension of Gödel logic by a unary operator for this purpose: This logic has a propositional fragment with a simple axiomatisation but its first-order fragment is not r.e. This operator can also be understood as a modal operator that is interpreted as real-valued functions with certain monotonicity properties. We give axiom systems for the propositional fragment of the logic generated by this function class and present results on generalisations for even larger classes. .

Abstract: Logics are traditionally presented semantically, or by Hilbert-style system. Closer to our interest are characterisations via (cut-free) Gentzen-type systems. However even in the later case, in particular if one moves from standard sequent calculi to less familiar systems like hypersequent systems, the connection with first principles about logical reasoning is often very indirect at best. We present a case were a seemingly exotic variant of a hypersequent system can be justified and actually derived from an argueably rather simple and natural game based model of reasoning about "dispersive experiments". .

Abstract:I'll present a proof system for purely implicative intuitionistic logic at the propositional level in the formalism of the calculus of structures, which is a generalisation of the sequent calculus implementing the deep inference methodology. This system can be shown sound and complete with respect to the usual sequent calculus, and I'll consider a restricted system for a restricted class of formulas. Then, I'll show how to encode lambda-terms with explicit substitutions inside formulas of this restricted system and establish a correspondence between its proof search and reduction in a lambda-calculus with explicit substitutions. Finally, I'll present a further restriction (based on focusing) allowing to establish the same correspondence with the standard lambda-calculus equipped with beta-reduction. This illustrates how we can prove results on reductions of lambda-calculi by proving results on derivations in a deep inference system.

Abstract: We present a term calculus with explicit contraction and weakening, together with a set of reduction rules that are atomic, in the sense that they never copy or erase unbounded subterms. Finally, we give an interpretation of our calculus in terms of the lambda calculus and show how our reduction can simulate beta reduction. .

Abstract: We analyse Henkin's proof of Gödel's completeness theorem and extracts from it a short program for building derivations from validity proofs. We study this program in comparison with the normalisation algorithm (NbE) that C. Coquand, Okada and others obtained by adequately composing soundness and completeness with respect to a rich semantics such as Kripke or phase semantics. However, we don't know at the current time how to modify Henkin's proof so that it produces cut-free proofs (if ever this is possible).

Abstract: Computer-generated proofs are essentially cut-free. Proofs with cut however have several advantages, the most obvious of which is their reduced size. In this talk, I will speak about a general approach to cut-introduction in first order logic based on a separation into two phases: 1) compute a compressed representation of an Herbrand-disjunction and 2) check whether this compression corresponds to a proof with cut. I will present a concrete algorithm for the case of a single \Sigma_1 cut yielding a quadratic compression at most.

Abstract: Classical realizability has recently raised a new requirement in the art of translating the lambda-calculus into combinatory logic : weak head reductions of the lambda-calculus must be simulated with the help of combinatoric head reductions only.
Quite amazingly, this was achieved just before the lambda-calculus was invented and never again since then. Haskell Curry actually did it in the late 20's for what we now call supercombinators, i.e. for any lambda-terms up to lambda lifting. Nevertheless, Curry's representation of the supercombinators is quadratic in their size, hence O(n^4) in the worst case for a lambda-term of size n.
We will present:
i. ideas to get combinatoric translations that work by head reduction
ii. a nice way to measure the size complexity of such a translation ... leading to a translation of optimal size, i.e. O(n ln n).

Abstract: We combine intuitionistic and classical logics into a new logic called Polarized Intuitionistic Logic. This logic is based on treating Gentzen’s distinction between “left” and “right” in two-sided sequents as a form of polarity. We give this logic both a Kripke-style semantics as well as a sequent calculus. The latter bares essential similarities to Girard’s LC proof system for classical logic although our proof system encompasses both classical and intuitionistic logic. We show that soundness and completeness hold for these notions of semantics and proof, from which it follows that cut is admissible in the proof system and that the propositional fragment of the logic is decidable. We also discuss certain traditional intuitionistic concepts such as Glivenko’s theorem in the context of this logic.

Abstract: The unification problem in higher order logic is undecidable already for second order logic, although some classes were shown to be decidable. We propose to replace a subset of the unification problem, which is the cycles, by constraints. The cycles are first proved to be the source of undecidability in unification in second order logic. Then, conditions on the constraints are imposed that will allow for a unification algorithm based on the well-known Huet's algorithm and using these constraints to be complete and sound. The aim of such an algorithm, besides possible performance optimization, is to analyze decidability in second order unification problems, due to the fact that if all cycles can be replaced by constraints, the algorithm always terminates. Currently we try to show decidability of unification in known decidable classes, like Monadic second order (Farmer '89), by use of this method.

Abstract: Expansion nets are a form of proof-net for classical logic for which correctness is polynomial-time checkable, with sequentialization into a calculus which replaces weakening with the additive (as well as multiplicative) rule for disjunction. Cut-elimination against structural rules is via the notion of subnet: we will show a new property of subnets (contiguousness) which is helpful in defining this cut-elimination in the presence of the mix rule.

Abstract: Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called G which represents relations over λ-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in G. We also describe an interactive theorem prover called Abella that implements G and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations.

Abstract: Hilbert's epsilon calculus is based on an extension of the language of predicate logic by a term-forming operator. Two fundamental results about the epsilon calculus, the first and second epsilon theorem, play a r\^ole similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. In the talk, we investigate the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.

Abstract: Since Prolog was developed, lots of attempts have been made in order to enhance the power of the underlying logic on logical programming languages. Some languages like lambda-Prolog and LO can capture, for example, features such as modularity, data-abstraction and some issues of concurrency. As far as abstract programming languages are concerned, the main development so far was the proof that linear logic is, in fact, a programming language itself. Recently, a refinement of linear logic was proposed with the use of subexponentials, allowing the incorporation of the concept of locations. In this way, it is possible to prove that algorithms correspond, in fact, to proof search. In this talk I will present linear logic with subexponentials and some examples that make clear the increase in expressiveness. I will also talk about recent developments in implementing a programming language based on this logic.

Abstract: In this talk I will present the basic ideas behind the decomposition theorem and the splitting lemma for systems presented in the calculus of structures. I will also show how the cut elimination theorem can be derived from them. The running example will be the logic NEL, which is a non-commutative extension of multiplicative exponential linear logic, and which cannot be presented in the sequent calculus.

Abstract: We will give a tutorial on an algebraic approach to proof theory for substructural logics, which have been developed together with Agata Ciabattoni, Nikolaos Galatos and Lutz Strassburger. In particular, we will discuss how finding a suitable proof system for substructural logics is systematically connected to finding a suitable method of completion for corresponding algebras.