Proof and refutation in MALL as a game

Annals of Pure and Applied Logic - Tập 161 - Trang 654-672 - 2010
Olivier Delande1, Dale Miller1, Alexis Saurin2,1
1INRIA Saclay - Île-de-France and LIX/École Polytechnique, Route de Saclay, 91128 Palaiseau Cedex, France
2Università degli Studi di Torino, Corso Svizzera 185, 10149 Torino, Italy

Tài liệu tham khảo

Abramsky, 1994, Games and full completeness for multiplicative linear logic, The Journal of Symbolic Logic, 59, 543, 10.2307/2275407 Abramsky, 2000, Full abstraction for PCF, Information and Computation, 163, 409, 10.1006/inco.2000.2930 Abramsky, 1999, Concurrent games and full completeness, 431 Andreoli, 1992, Logic programming with focusing proofs in linear logic, Journal of Logic and Computation, 2, 297, 10.1093/logcom/2.3.297 Blass, 1992, A game semantics for linear logic, Annals of Pure and Applied Logic, 56, 183, 10.1016/0168-0072(92)90073-9 Chaudhuri, 2008, Canonical sequent proofs via multi-focusing, vol. 273, 383 Cosmo, 1998, A game semantics foundation for logic programming (extended abstract), vol. 1490, 355 Danos, 1989, The structure of multiplicatives, Archive for Mathematical Logic, 28, 181, 10.1007/BF01622878 Delande, 2008, A neutral approach to proof and refutation in MALL, 498 Faggian, 2002, Designs, disputes and strategies, vol. 2471, 713 Galanaki, 2008, An infinite-game semantics for well-founded negation in logic programming, Annals of Pure and Applied Logic, 151, 70, 10.1016/j.apal.2007.10.004 J.-Y. Girard, A fixpoint theorem in linear logic, an email posting to the mailing list [email protected]. Feb. 1992 Girard, 2001, Locus solum: From the rules of logic to the logic of rules, Mathematical Structures in Computer Science, 11, 301, 10.1017/S096012950100336X Girard, 1999, On the meaning of logical rules I: syntax vs. semantics, 215 Girard, 1987, Linear logic, Theoretical Computer Science, 50, 1, 10.1016/0304-3975(87)90045-4 Girard, 1996, Proof-nets: The parallel syntax for proof-theory, vol. 180, 97 Hallnäs, 1991, A proof-theoretic approach to logic programming. II. Programs as definitions, Journal of Logic and Computation, 1, 635, 10.1093/logcom/1.5.635 H. Herbelin, Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes, Ph.D. Thesis, Université Paris 7, 1995 W. Hodges, Logic and games, in: E.N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy, Stanford University, 2004 Hyland, 2000, On full abstraction for PCF: I. models, observables and the full abstraction problem, II. dialogue games and innocent strategies, III. A fully abstract and universal game model, Information and Computation, 163, 285, 10.1006/inco.2000.2917 M.I. Kanovich, Simulating linear logic with 1-linear logic, Preprint 94-02, Laboratoire de Mathématiques Discrètes, University of Marseille, 1994 Lakatos, 1976 Lincoln, 1992, Decision problems for propositional linear logic, Annals of Pure and Applied Logic, 56, 239, 10.1016/0168-0072(92)90075-B J.-V. Loddo, Généralisation des jeux combinatoires et applications aux langages logiques, Ph.D. Thesis, Université Paris VII, 2002 Loddo, 2000, Playing logic programs with the alpha–beta algorithm, vol. 1955, 207 P. Lorenzen, Ein dialogisches konstruktivitätskriterium, in: Infinitistic Methods: Proceed. Symp. Foundations of Math., PWN, 1961, pp. 193–200 Melliès, 2004, Asynchronous games 2: The true concurrency of innocence, Theoretical Computer Science, 358, 200 Miller, 2006, A game semantics for proof search: Preliminary results, vol. 155, 543 Pym, 2004, Reductive logic and proof-search: Proof theory, semantics, and control, vol. 45 A. Saurin, Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique), Ph.D. Thesis, Ecole Polytechnique, Sep. 2008 Saurin, 2008, Towards ludics programming: Interactive proof search, vol. 5366, 253 Smullyan, 1995 Stirling, 1999, Bisimulation, modal logic and model checking games, Logic Journal of the IGPL, 7, 103, 10.1093/jigpal/7.1.103 van Emden, 1986, Quantitative deduction and its fixpoint theory, Journal of Logic Programming, 3, 37, 10.1016/0743-1066(86)90003-8