PhD Thesis
 G. Bellin.
``Mechanizing Proof Theory.
ResourceAware Logics and Proof Transformation
to Extract Implicit Information''.
Ph.D. thesis, Department of Philosophy, Stanford University, June 1990
Papers
Prooftheory
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. 146165.
ps file  categorical classical logic pdf
 G.Bellin, M.Carrara, D.Chiffi and A.Menti
"A pragmatic dialogic interpretation of biintuitionism"
revised version for Logic and Logical Philosophy January 2014
(mathematical and philosophical interpretations of ``polarized''
biintuitionism  for linear and nonlinear systems).
pdf file
 G. Bellin
"Assertions, hypotheses, conjectures, expectations:
Roughset semantics and prooftheory",
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: 9789475473.
(paper for the Proceedings of the
Natural Deduction Conference, Rio de Janeiro, July 26, 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 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 (IMLAFLOC 2002),
V.de Paiva, R.Gore' and M. Mendler eds.,
Volume 14, Number 4, 2004, pp. 473506.
ps file  pragmatics of biintuitionism 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 IMLAFLOC'02 workshop, Copenhagen, 2002.
ps file  S4 translation for biintuitionism pdf
 G. Bellin and Corrado Biasi.
"CutElimination 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 IMLAFLOC'02 conference.)
ps file  pdf file
 G. Bellin and Kurt Ranalter.
"A Kripkestyle semantics for the intuitionistic logic of pragmatics
ILP"
"Journal of Logic and Computation", vol. 13, n. 5, 2003,
pp.755775
special issue for the Dagstuhl Seminar n. 01141
on Semantic Foundations of Proofsearch, 16 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
 G. Bellin.
``Chu's Construction: A Prooftheoretic Approach''
in Ruy J.G.B. de Queiroz editor,
"Logic for Concurrency and Synchronisation",
Kluwer Trends in Logic n.18, 2003, pp.93114.
(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.115150.
(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.
``Subnets of Proofnets in multiplicative linear logic with MIX''
Mathematical Structures in Computer Science vol.7, pp.663699 (1997).
Copyright Cambridge University Press 1997
dvi file  subnets in MLL with Mix ps file
 G. Bellin and J. van de Wiele.
``Subnets of Proofnets in MLL''
in: Advances in Linear Logic
JY. 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 LFCS91161
Department of Computer Science, University of Edinburgh, May 1991
dvi file  proof nets for MALL ps file
Other
 G. Bellin, Valeria de Paiva and Eike Ritter.
``Extended CurryHoward 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 2930, 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 CarnegieMellon University
Contemporary Mathematics 106,
AMS, 1990, pp. 1737.
 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. 285300.
Intuitionistic Herbrand Theorem pdf file
Theoretical Computer Science
 G. Bellin and P.J.Scott.
``On the Picalculus and linear logic''
in: Theoretical Computer Science 135 (1994) 1165
Copyright 1994  Elsevier Science Publishers B.V. All rights reserved
dvi file  pi calculus and linear logic ps file
Automated Deduction
 G. Bellin and J. Ketonen.
``Experiments in Automatic Theorem Proving''
Technical Report No. STANCS871155
back home