• G. Bellin.
  ``Mechanizing Proof Theory.
  Resource-Aware Logics and Proof Transformation
  to Extract Implicit Information''.
  Ph.D. thesis, Department of Philosophy, Stanford University, June 1990

Classical Logic, Categorical Logic

• G.Bellin, M.Hyland, E.Robinson and C.Urban.
  "Categorical Proof Theory of Classical Propositional Calculus"
  Theoretical Computer Science - Vol. 364, 2, November 2006, pp. 146-165.
  ps file | categorical classical logic pdf

• G.Bellin.
  "Categorical Proof Theory of Co-Intuitionistic Linear Logic"
  submitted to LOMECS, autumn 2012.
  categorical cointuitionistic pdf

Logic for Pragmatics

• G.Bellin, M.Carrara, D.Chiffi and A.Menti
  "A pragmatic dialogic interpretation of bi-intuitionism"
  revised version for Logic and Logical Philosophy January 2014
  (mathematical and philosophical interpretations of ``polarized'' bi-intuitionism - for linear and non-linear systems).
  pdf file

• G. Bellin
  "Assertions, hypotheses, conjectures, expectations: Rough-set semantics and proof-theory",
  In L.C.Pereira, E.H.Haeusler and V.de Paiva eds., Advances in Natural Deduction
  Trends in Logic, Studia Logica Library, Vol 39, Springer Netherlands, Dordrecht, 2014 ISBN: 978-94-7547-3.
  (paper for the Proceedings of the Natural Deduction Conference, Rio de Janeiro, July 2-6, 2001 last revision April 2011).
  Assertions Hypotheses Conjectures Expectations pdf
  

• Editorial by G. Bellin, S. Berardi and T. Crolard to the special issue of Fundamenta Informaticae 84 (2008) dedicated to the Logic for Pragmatics

• G.Bellin, M.Carrara and D.Chiffi
  "A pragmatic framework for intuitionistic modalities: Classical logic and Lax logic",
  submitted to the Journal of Logic and Computation,
  April 2012.
  pragmatics of intuitionistic modalities pdf

• G. Bellin
  "A Term Assignment for Dual Intuitionistic Logic",
  conference paper presented at the LICS'05-IMLA'05 Workshop, Chicago, IL, June 30, 2005
  ps file | Term Assignment for cointuitionistic logic pdf
  

• G. Bellin
  "Natural Deduction and term assignment for co-Heyting algebras in Polarized Bi-Intuitionistic Logic",
  Submitted to the Proceedings of the Natural Deduction Conference, Rio de Janeiro, July 2-6, 2001
  (revised summer 2004)
  ps file | proofs and term assignment for cointuitionistic logic pdf
  

• G. Bellin and Corrado Biasi
  "Towards a logic for pragmatics: Assertions and conjectures",
  In: Journal of Logic and Computation Special Issue with the Proceedings of the Workshop on
  Intuitionistic Modal Logic and Application (IMLA-FLOC 2002), V.de Paiva, R.Gore' and M. Mendler eds.,
  Volume 14, Number 4, 2004, pp. 473-506.
  ps file | pragmatics of bi-intuitionism pdf
  

• G. Bellin.
  "Towards a formal pragmatics:
  an intuitionistic theory of assertive and conjectural judgements with an extension of Goedel, McKinsey and Tarski's S4 translation"
  conference paper presented at the IMLA-FLOC'02 workshop, Copenhagen, 2002.
  ps file | S4 translation for bi-intuitionism pdf
  

• G. Bellin and Corrado Biasi.
  "Cut-Elimination for the logic of pragmatics"
  (This is work in progress, which summarizes dr Corrado Biasi's Tesi di Laurea.
  It substantially refines and develops the ideas and the direction of research
  presented at the IMLA-FLOC'02 conference.)
  ps file | pdf file

• G. Bellin and Kurt Ranalter.
  "A Kripke-style semantics for the intuitionistic logic of pragmatics ILP"
  "Journal of Logic and Computation", vol. 13, n. 5, 2003, pp.755-775
  special issue for the Dagstuhl Seminar n. 01141
  on Semantic Foundations of Proof-search, 1-6 April 2001,
  ps file | Logic of assertions, obligations and causal implication pdf

• G. Bellin and Carlo Dalla Pozza.
  A pragmatic interpretation of substructural logics
  in Reflections on the Foundations of Mathematics, Essays in Honor of Solomon Feferman,
  W.Sieg, R.Sommer and C.Talcott eds. ASL Lecture Notes in Logic ; 15, 2002.
  ps file | Pragmatics of substructural logics pdf

Linear Logic

• G. Bellin.
  ``Chu's Construction: A Proof-theoretic Approach''
  in Ruy J.G.B. de Queiroz editor, "Logic for Concurrency and Synchronisation", Kluwer Trends in Logic n.18, 2003, pp.93-114.
  (Submitted April 1999, revised July 2000).
  Copyright 2001 Kluwer Academic Publishers. All rights reserved.
  dvi file | Chu's construction ps file

• G. Bellin.
  ``Two paradigms of logical computation in Affine Logic?''
  in Ruy J.G.B. de Queiroz editor, "Logic for Concurrency and Synchronisation", Kluwer Trends in Logic n.18, 2003, pp.115-150.
  (Submitted October 1999, revised June 2001).
  Copyright 2001 Kluwer Academic Publishers. All rights reserved.
  dvi file | proof nets for affine logic ps file

• G. Bellin and A. Fleury.
  ``Planar and Braided Proof-nets for MLL with Mix''
  Archive for Mathematical Logic 1998, 37, pp.309-325.
  dvi file | planar and braided proof nets ps file

• G. Bellin.
  ``Subnets of Proof-nets in multiplicative linear logic with MIX''
  Mathematical Structures in Computer Science vol.7, pp.663-699 (1997).
  Copyright Cambridge University Press 1997
  dvi file | subnets in MLL with Mix ps file

• G. Bellin and J. van de Wiele.
  ``Subnets of Proof-nets in MLL-''
  in: Advances in Linear Logic J-Y. Girard, Y. Lafont and L. Regnier eds.
  London Mathematical Society Lecture Note Series 222, 1995
  Copyright Cambridge University Press 1995
  dvi file | subnets in proof nets for MLL ps file

• G. Bellin.
  ``Proof Nets for Multiplicative and Additive Linear Logic''
  Technical Report LFCS-91-161
  Department of Computer Science, University of Edinburgh, May 1991
  dvi file | proof nets for MALL ps file

• G. Bellin, Valeria de Paiva and Eike Ritter.
  ``Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic''
  paper presented at the conference Methods for Modalities 2,
  Institute for Logic, Language and Computation, University of Amsterdam, November 29-30, 2001.
  Constructive K ps file

• G. Bellin.
  ``Ramsey Interpreted: A Parametric Version of Ramsey's Theorem''
  in: Logic and Computation: Proceedings of a Symposium held at Carnegie-Mellon University
  Contemporary Mathematics 106, AMS, 1990, pp. 17-37.
  

• G. Bellin.
  ``A system of natural deduction for GL''
  in: Theoria LI, 2 1985, pp. 89-114. natural deduction and normalization for GL pdf file
  

• G. Bellin.
  ``Herbrand's Theorem for Calculi of Sequents LK and LJ''
  in: Proceedings of the Fifth Scandinavian Logic Symposium
  Aalborg University Press, 1979, pp. 285-300. Intuitionistic Herbrand Theorem pdf file
  

• G. Bellin and A. Menti.
  "On the pi-calculus and co-intuitionistic logic. Notes on logic for concurrency and lambda P systems"
  pi calculus, cointuitionistic logic and membrane computing pdf file Accepted by Fundamenta Informaticae, December 2012.

• G. Bellin.
  ``On the Pi-calculus and distributed calculi for co-intuitionistic logic''
  pi calculus and cointuitionistic logic pdf file
  Paper accepted at LAM'11, (Logics, Agents and Mobility), CONCUR 2011, Aachen, Germany, 10 Sept 2011.

• G. Bellin and P.J.Scott.
  ``On the Pi-calculus and linear logic''
  in: Theoretical Computer Science 135 (1994) 11-65
  Copyright 1994 - Elsevier Science Publishers B.V. All rights reserved
  dvi file | pi calculus and linear logic ps file

• G. Bellin and J. Ketonen.
  ``A decision procedure revisited: Notes on direct logic, linear logic and its implementation''
  in: Theoretical Computer Science 95 (1992) 115-142
  Copyright 1992 - Elsevier Science Publishers B.V. All rights reserved
  dvi file

• G. Bellin and J. Ketonen.
  ``Experiments in Automatic Theorem Proving''
  Technical Report No. STAN-CS-87-1155
  

back home