We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a (...) natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al. (shrink)

This paper proposes a synthetic presentation of the proof construction paradigm, which underlies most of the research and development in the so-called “logic programming” area. Two essential aspects of this paradigm are discussed here: true non-determinism and partial information. A new formulation of Focussing, the basic property used to deal with non-determinism in proof construction, is presented. This formulation is then used to introduce a general constraint-based technique capable of dealing with partial information in proof construction. One of the baselines (...) of the paper is to avoid to rely on syntax to describe the key mechanisms of the paradigm. In fact, the bipolar decomposition of formulas captures their main structure, which can then be directly mapped into a sequent system that uses only atoms. This system thus completely “dissolves” the syntax of the formulas and retains only their behavioural content as far as proof construction is concerned. One step further is taken with the so-called “abstract” proofs, which dissolves in a similar way the specific tree-like syntax of the proofs themselves and retains only what is relevant to proof construction. (shrink)

Investigating Girard's new propositionnal calculus which aims at a large scale study of computation, we stumble quickly on that question: What is a multiplicative connective? We give here a detailed answer together with our motivations and expectations.

This paper proposes a synthetic presentation of the proof construction paradigm, which underlies most of the research and development in the so-called “logic programming” area. Two essential aspects of this paradigm are discussed here: true non-determinism and partial information. A new formulation of Focussing, the basic property used to deal with non-determinism in proof construction, is presented. This formulation is then used to introduce a general constraint-based technique capable of dealing with partial information in proof construction. One of the baselines (...) of the paper is to avoid to rely on syntax to describe the key mechanisms of the paradigm. In fact, the bipolar decomposition of formulas captures their main structure, which can then be directly mapped into a sequent system that uses only atoms. This system thus completely “dissolves” the syntax of the formulas and retains only their behavioural content as far as proof construction is concerned. One step further is taken with the so-called “abstract” proofs, which dissolves in a similar way the specific tree-like syntax of the proofs themselves and retains only what is relevant to proof construction. (shrink)