The seminar usually takes place on Wednesdays, at 10.30am, in the prefab meeting room, at the LIX. You can find a map here. It is mostly aimed at PhD students, and is not only open to the Parsifal team, but to anyone interested. To be informed of the coming talks by e-mail, please contact Anne-Laure Poupon (poupon_AT_lix.polytechnique.fr).
Proof-search for constructive logics
Ivan Gazeau
14 January 2009, 10.30am, prefab meeting room
Abstract : This talk will be based on the article of the same name by Pinto and Dyckhoff, from which this abstract is taken. We present an overview of some sequent calculi organised not for "theorem-proving" but for proof search, where the proofs themselves (and the avoidance of known proofs on backtracking) are objects of interest. The main calculus discussed is that of Herbelin 1994] for intuitionistic logic, which extends methods used in hereditary Harrop logic programming; we give a brief discussion of some similar calculi for other logics. We also point to some related work on permutations in intuitionistic Gentzen sequent calculi that clari es the relationship between such calculi and natural deduction.
Finite Automata as Fixed Points
David Baelde
12 January 2009, 3pm, prefab meeting room
Abstract : Finite automata (NFA) are a natural, well understood class of systems. Yet they express complex behaviors. For example, finite automata are still the main target devices in model-checking. In that area, models and properties are encoded as automata, and satisfaction as automata inclusion. We shall study the treatment of NFA. This constitutes a possible basis for a proof-theoretical foundation for model-checking, but is also a good test for the expressiveness of muMALL. We encode NFA (or rather acceptance by an automaton) by a complex formula involving interleaved fixed points corresponding to the states of the automaton. We show that the logics allows handles such complex formulas in an elegant way, obtaining a nice characterization of automata inclusion as "multi-simulation" and soundness and completeness of muMALL for automata inclusions. Going further, I propose a fragment of "regular formulas", and attempt to extend previous results and methodology directly to the logic. We characterize a nice condition under which internal completeness holds: if an implication of regular formulas holds semantically, it is provable in the logic. This is only a slight extension, but more importantly our characterization can be interpreted in terms of proof-search and invariant generation, giving rise to a possible extension of the notion of cyclic proofs. These are recent results that I developed in chapter 5 of my thesis. My aim here is also to discuss their impact and think about further work along these lines.
Neutrality in logic and games
Olivier Delande
7 January 2009, 10.30am, prefab meeting room
Abstract :
A Presentation of Bedwyr
David Baelde
26 November 2008, 10.30am, prefab meeting room
Abstract : Bedwyr est un langage de programmation logique qui exploite deux avancées récentes en théorie de la démonstration: la notion de point fixe (ou définition) et la quantification générique (nabla). Cela permet un support logique de la negation-as-(finite)-failure. Autrement dit, on passe des capacités usuelles de représentation des langages de programation logique à une capacité de model-checking. Je présenterai la théorie sous-tendant Bedwyr, quelques exemples d'utilisation. Notamment, on verra comment la spécification de la bisimulation pour le pi-calcul transforme Bedwyr en un outil de vérification de bisimulation. Nous verrons les limites de Bedwyr et discuterons comment les repousser.
Semantics for Linear Logic
Anne-Laure Poupon
12 November 2008, 10.30am, prefab meeting room
Abstract : We will discuss different semantics for linear logic, including coherent spaces, the notion of resources, and game semantics. We will also try to consider an equivalent to Hintikka's game of truth in linear logic. One of the aims of this talk will be to share our intuitions about linear logic, and discuss them.
Proof Search and Focusing in the Calculus of Structures
Nicolas Guénot
5 November 2008, 10.30am, prefab meeting room
Abstract : Proof search is usually always done in the same setting, namely the good ol' cut-free sequent calculus. However, the "deep inference" methodology, which has been studied for some years now and lead to the definition of a logical formalism called "calculus of structures", has some interesting effects on the way one should search for proofs. We will present here the benefits but also the disavantvages of using the calculus of structures for proof search. Then, in order to make proof search efficient, the notion of "focused proofs" has been defined in linear logic, with the goal of reducing nondeterminism in this process. We will show that this can also be done in the calculus of structures, thus drastically reducing the problems encountered when building a proof in this formalism. This is implemented in a deep inference focused proof system for MALL that we will present, and for which the completeness proof has to be discussed. Finally, we will describe some variations on this theme, allowed by this deep setting, and the new possibilites it offers.
The Nabla quantifier
David Baelde
29 October 2008, 10.30am, prefab meeting room
Abstract : We come back to the initial design of the nabla quantifier by Miller and Tiu, which we call minimal generic quantification. In the absence of fixed points, it is equivalent to seemingly stronger designs. However, several expected theorems about (co)inductive specifications can not be derived in that setting. We present a refinement of minimal generic quantification that brings the expected expressivity while keeping the minimal semantic,which we claim is useful to get natural adequate specifications. We build on the idea that generic quantification is not a logical connective but one that is defined, like negation in classical logics. This allows us to use the standard (co)induction rule, but obtain much more expressivity than before. We show classes of theorems that can now be derived in the logic, and present a few practical examples.
Focusing in linear meta-logic
Vivek Nigam
22 October 2008, 3pm, prefab meeting room
Abstract : It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof systems. Here, we show that if we adopt different focusing annotations for such linear logic specifications, a range of other proof systems can also be specified.
In particular, we show that natural deduction (normal and non-normal), sequent proofs (with and without cut), tableaux, and proof systems using general elimination and general introduction rules can all be derived from essentially the same linear logic specification by altering focusing annotations. By using elementary linear logic equivalences and the completeness of focused proofs, we are able to derive new and modular proofs of the soundness and completeness of these various proofs systems for intuitionistic and classical logics.
Focusing and Polarization in Intuitionistic Logic
Dale Miller
15 October 2008, 10.30am, prefab meeting room
Abstract : A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof search and the proof normalization approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree oranother. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems.
Reference : Focusing and Polarization in Intuitionistic Logic, by Chuck Liang and Dale Miller. CSL'07: Computer Science Logic, J.Duparc and T.A.Henzinger, editors, LNCS 4646, pages 451-465. Springer-Verlag.
What is Deep Inference ? - An Overview
Lutz Strassburger
9 October 2008, 2pm, bocal
Abstract : Deep Inference is a proof theoretic paradigm that allows to rewrite formulas deep inside arbitrary contexts. Thus, it is very different from shallow formalisms, like the sequent calculus, where formulas are decomposed along their main connective.
In the talk I will give an overview of the research results on deep inference within the last 7 years. In particular, I will focus on the new expressivity and modularity in the design of deductive systems, novel methods for proving cut elimination, new kinds of normal forms for proofs, and possible exponential speed-up for proofs of Boolean tautologies.