Submitted
 Disjunctive Axioms and Concurrent LambdaCalculi: a CurryHoward Approach
(with F. Aschieri and F. Genco).
Preprint (last update 6/2/2018)
Books
 Logica a informatica, McGrawHill, 1997 (with A. Asperti). In Italian.
(The book is used for
these logic courses)
Special Issues Edited

Concepts and Meaning  Papers in honour of Alexander Leitsch on the occasion of his 60th birthday.
Journal of Logic and Computation. To appear (with M. Baaz, Dov M. Gabbay, S. Hetzl and D. Weller)
 MFCS and CSL 2010 Satellite Workshops: Selected Papers. Fundamenta Informaticae 123(1), IOS Press, 2013
(with R. Freivalds, A. Kucera, I. Potapov and S. Szeider)
 Algebraic and Prooftheoretic Aspects of Nonclassical Logics
 Papers in honour of Daniele Mundici on the occasion of his 60th birthday, LNCS 4460, Springer, 2007
(with S. Aguzzoli, B. Gerla, C. Manara and V. Marra).
 Proceedings of COS04 and Ercim (Volume I), Special Issue of the Logic Journal of IGPL
13(4), July 2005 (with M. Baaz, D.M. Gabbay, and P. Hájek).
 Proceedings of COS04 and Ercim (Volume II), Special Issue of the Logic Journal of IGPL
13(5), September 2005 (with M. Baaz, D.M. Gabbay, and P. Hájek).
International Journals
 Hypersequents and Systems of Rules: Embeddings and Applications. ACM TOCL Accepted.
(with F. Genco).
PDF
 Algebraic proof theory: hypersequents and hypercompletions,
Annals of Pure and Applied Logic, 168(3): 693737, 2017 (with N. Galatos and K. Terui).
PDF
 From cutfree calculi to automated deduction: the case of bounded contraction, Accepted for publication in
ENTCS, (with B, Lellmann, C. Olarte and E. Pimentel).
PDF
 Power and limits of structural display rules. ACM TOCL 17(3), 2016
(with R. Ramanayake). PDF
 Understanding Prescriptive Texts: Rules and Logic as elaborated by the Mimamsa school.
Accepted for publication in Confluence: Online Journal of World Philosophies , (with E. Freschi, F. Genco and B. Lellmann).
PDF
 Proof Search and CoNP Completeness for ManyValued Logics. Fuzzy Sets and Systems 292: 130149 (2016)
(with M. Bongini and F. Montagna). PDF
 Proof theory of witnessed Goedel logic: a negative result. Journal of Logic and Computation 26(1): 5164 (2016)
(with M. Baaz) PDF
 Uniform proofs of standard completeness for extensions of firstorder MTL.
Theoretical Computer Science vol. 603: 4357 (2015)
(with P. Baldi)
 Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. TOCL 16(1): 5 (2014)
(with O. Lahav, L. Spendier and A. Zamansky)
PDF
 Software
 Hypersequent and display calculi  a unified perspective. Studia Logica 102(6): 12451294 (2014)
(with R. Ramanayake and H. Wansing)
PDF
 Proof theory for locally finite manyvalued logics: semiprojective logics. Theoretical Computer
Science 480: 2642, 2013
(with F. Montagna). PDF
 Formal approaches to rulebased systems in medicine: the case of CADIAG2, Journal of Approximate Reasoning 54(1): 132148, 2013
(with D. Picado, T. Vetterlein and M. ElZekey). PDF
 Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability, Logical Methods for Computer Science 8(1), 2012
(with M. Baaz and C.G. Fermüller). PDF
 Algebraic proof theory for substructural logics: cutelimination and completions, Annals of Pure and Applied Logic, 163(3): 266290, 2012
(with N. Galatos and K. Terui). PDF
 Firstorder satisfiability in Gödel logics: an NPcomplete fragment, Theoretical Computer Science, 412: 66126623, 2011
(with M. Baaz and N. Preining). PDF
 MacNeille Completions of FLalgebras, Algebra Universalis 66(4): 405420, 2011
(with N. Galatos and K. Terui). PDF
 On the (fuzzy) logical content of CADIAG2, Fuzzy Sets and Systems, 161(14): 19411958, 2010
(with T. Vetterlein). PDF
 Algebraic and prooftheoretic characterizations of truth stressers for MTL and its extensions, Fuzzy Sets and Systems, 161(3): 369389, 2010
(with G. Metcalfe and F. Montagna). PDF
 Density Elimination, Theoretical Computer Science 403(23): 328346, 2008
(with G. Metcalfe). PDF
 Towards an Algorithmic Construction of CutElimination Procedures, Mathematical Structures in Computer Science 18(1): 81105, 2008
(with A. Leitsch). PDF
 Towards a semantic characterization of cutelimination, Studia logica 82(1): 95119, 2006
(with K. Terui). PDF (Addenda)
 A Prooftheoretical Investigation of Global Intuitionistic (Fuzzy) Logic,
Archive of Mathematical Logic 44: 435457, 2005. PDF
 Analytic Calculi for Monoidal Tnorm Based Logic, Fundamenta Informaticae, Vol. 59, N. 4, 315332, 2004,
(with M. Baaz and F. Montagna). PS
 Hypersequent Calculi for Gödel Logics  a Survey, Journal of Logic and Computation 13: 835861, 2003
(with M. Baaz and C.G. Fermüller). PDF
 Tnorm based logics with ncontraction, Neural Network World 12(5): 441452, 2002
(with F. Esteva and L. Godo). PS
 Hypersequent Calculi for some Intermediate Logics with Bounded Kripke Models, Journal of Logic and Computation 11(2): 283294, 2001
(with M. Ferrari). PDF (Corrigenda)
 Finiteness of infinitevalued Lukasiewicz logic, Journal of Logic, Language and Information 9: 529, 2000
(with S. Aguzzoli). PS
 Sequent calculi for finitevalued Lukasiewicz logics via boolean decompositions, Journal of Logic and Computation 10(2): 213222, 2000
(with S. Aguzzoli and A. Di Nola).
 Cut free proof systems for logics of weak excluded middle, Soft Computing 2(4): 147156, 1998
(with D.M. Gabbay and N. Olivetti).
 A Sufficient Condition for Completability of Partial Combinatory Algebras, Journal of Symbolic Logic 62(4): 12091214, 1997
(with A. Asperti).
International Conferences
 From Display to Labelled Proofs for Tense Logics. Proceedings of LFCS 2018, (with T. Lyon and R. Ramanayake).
PDF
 Goedel Logic: From Natural Deduction to Parallel Computation.
Proceedings of LICS 2017, (with F. Aschieri and F. Genco).
PDF
 Bunched Hypersequent Calculi for Distributive Substructural Logics.
Proceedings of LPAR 2017, (with R. Ramanayake).
PDF
 Standard completeness for extensions of IMTL. Proceedings of FUZZIEEE 2017:
International Conference on Fuzzy Systems, (with P. Baldi and F. Gulisano)
PDF
 Embedding formalisms: hypersequents and twolevel systems of rules. Proceedings of AIML 2016 , (with F. Genco)
PDF
 Mimamsa Deontic Logic: Proof Theory and Applications. Proceedings of TABLEAUX 2015, (with E. Freschi, F. Genco and B. Lellmann)
PDF
 Standard completeness for uninormbased logics. Proceedings of the IEEE International Symposium on MultipleValued Logic
(ISMVL 2015), Waterloo (Canada),
(with P. Baldi) PDF.
 Tools for the investigation of substructural and paraconsistent logics. Proceedings of JELIA 2014 ,
(with L. Spendier) PDF 
Software
 Hypersequent and Labelled Calculi for Intermediate Logics, Proceedings of TABLEAUX 2013 ,
(with P. Maffezioli and L. Spendier) PDF

Structural extensions of display calculi: a general recipe, Proceedings of WOLLIC 2013 ,
(with R. Ramanayake). PDF
 Automated Support for the Investigation of Paraconsistent and Other Logics, Proceedings of the Symposium on Logical Foundations in Computer Science 2013,
LFCS 2013, S. Artemov and A. Nerode (Eds.), LNCS (with O. Lahav, L. Spendier and A. Zamansky). PDF
 Software
 Standard completeness for extensions of MTL: an automated approach, Proceedings of the Workshop on Logic, Language, Information and Computation, WOLLIC 2012,
L. Ong and R. de Queiroz (Eds.), LNCS 7456, 154167, Springer, Heidelberg, 2012 (with P. Baldi and L. Spendier). PDF
 Basic Constructive Connectives, Determinism and Matrixbased Semantics, Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods,
LNCS 6793, 119133, Tableaux 2011 (with O. Lahav and A. Zamansky). PDF
 On the classical content of Gödel logic with strong negation and its application to a fuzzy medical expert system, Proceedings of Knowledge Representation
and Reasoning KR2010, IEEE (with P. Rusnok).
PDF
 Expanding the realm of systematic proof theory, Proceedings of Computer Science Logic, CSL 2009, LNCS
(with L. Strassburger and K. Terui). PDF
 SAT in Monadic Gödel Logics: a borderline between decidability and undecidability, Proceedings of
Workshop on Logic, Language, Information and Computation, WOLLIC 2009, LNAI
(with M. Baaz and N. Preining). PDF
 A formal logical framework for CADIAG2, Proceedings of Medical Informatics Europe, MIE 2009, Sarajevo, Studies in Health Technology and Informatics series, IOS Press
(with T. Vetterlein and KP. Adlassnig)
 Canonical Calculi: Invertibility, AxiomExpansion and (Non)determinism, Proceedings of Computer Science Symposium in Russia (CSR2009), LNCS
(with A. Avron and A. Zamansky). PDF
 Cut elimination for first order Gödel logic by hyperclause resolution, Proceedings of Logic for Programming and Automated Reasoning (LPAR 2008), LNCS 5330, 451466
(with M. Baaz and C.G. Fermüller). PDF
 From axioms to analytic rules in nonclassical logics, Proceedings of the IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE, 229240, 2008
(with N. Galatos and K. Terui). PDF  Software
 Monadic Fragments of Gödel Logics: Decidability and Undecidability Results, Proceedings of Logic for Programming and Automated Reasoning (LPAR 2007),
LNAI 4790, 7791, 2007
(with M. Baaz and C.G. Fermüller). PDF
 Density Elimination and Rational Completeness for FirstOrder Logics, Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2007), LNCS 4514, 132146, 2007
(with G. Metcalfe). PDF
 Modular CutElimination: Finding Proofs or Counterexamples, Proceedings of Logic for Programming and Automated Reasoning (LPAR 2006), LNAI 4246, 135149, 2006
(with K. Terui). PDF
 Uniform Rules and Dialogue Games for Fuzzy Logics, Proceedings of Logic for Programming and Automated Reasoning (LPAR 2005), LNAI 3452, 496510, 2004
(with C. Fermüller and G. Metcalfe). PDF
 Automated Generation of Analytic Calculi for Logics with Linearity, Proceedings of Computer Science Logic (CSL 2004), LNCS 3210, 505517.
PDF
 Bounded Lukasiewicz Logics, Proceedings of
Automated Reasoning with Analytic Tableaux and Related Methods
(Tableaux 2003), LNAI 2796, 3247, 2003 (with G. Metcalfe). PS
 From Intuitionistic Logic to GödelDummett Logic via Parallel Dialogue Games, Proceedings of IEEE International Symposium on MultipleValued Logic (ISMVL 2003), Tokyo, (Japan),
May 2003, 188193 (with C.G. Fermüller). PDF
 A SchütteTait style cutelimination proof for firstorder Gödel logic,
Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2002), Copenhagen
(Denmark), August 2002, LNAI 2381, 2438 (with M. Baaz). PDF
 Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving,
Proceedings of Logic for Programming and Automated Reasoning (LPAR 2001), Cuba, December 2001, LNAI 2250, 201216 (with M. Baaz and C.G. Fermüller).
PDF
 Hypersequents as a uniform framework for Urquhart's C, MTL and related logics, Proceedings of IEEE International Symposium on MultipleValued Logic
(ISMVL 2001), Warsaw (Poland),
May 2001, IEEE Computer Society Press, 227232 (with C.G. Fermüller).
 CutElimination in a SequentsofRelations Calculus for Gödel Logic, Proceedings of the
IEEE International Symposium on MultipleValued Logic (ISMVL 2001), Warsaw (Poland), May 2001,
IEEE Computer Society Press, 181186 (with M. Baaz and C.G. Fermüller).PDF
 Quantified Propositional Gödel Logic, Proceedings of Logic for Programming and Automated Reasoning (LPAR 2000), Reunion Island, November 2000, LNAI 1955, 240257,
(with M. Baaz and R. Zach). PS
 Hypertableau and PathHypertableau Calculi for some families of intermediate logics, Proceedings of
Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2000),
St. Andrews (Scotland), July 2000, LNAI 1847, 160175 (with M. Ferrari).
PDF
 On Urquhart's C logic, Proceedings of the IEEE International Symposium on MultipleValued Logic (ISMVL 2000), Portland (USA), May 2000, IEEE Computer Society Press, 113118.
PS
 On the Undecidability of Some Subclassical FirstOrder Logics, Proceedings of
Foundations of Software Technology and Theoretical Computer Science (FST&TCS 1999), Chennai, December 1999,
LNCS 1738, 258268 (with M. Baaz , C.G. Fermüller and H. Veith). PS
 Bounded contraction in systems with linearity, Proceedings of
Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 1999), Saratoga (NY), June 1999, LNAI 1617, 113128.
 Proof Theory of Fuzzy Logics: Urquhart's C and related logics,
Proceedings of Mathematical Foundations of Computer Science (MFCS'98), Brno, August 1998, LNCS 1450, 203212
(with M. Baaz, C.G. Fermüller and H. Veith).
 Two connections between Linear Logic and Lukasiewicz Logic, Proceedings of
Computational Logic and Proof Theory  Kurt Gödel Colloquium (KGC 1997), Vienna, August 1997, LNCS 1289, 128139
(with D. Luchi).
 Effective Applicative Structures, Proceedings of
Category Theory in Computer Science (CTCS 1995) Cambridge (UK), August 1995, LNCS 953, 8195,
(with A. Asperti). PDF
National Conferences
 On Completability of Partial Combinatory Algebras, Fifth Italian Conference on Theoretical Computer Science (ICTCS 1995), Ravello, Italy. November 1995.
A. De Santis ed., World Scientific, 162175 (with A. Asperti). PDF
Book Chapters
 Towards an interpretation of the medical expert system CADIAG2.
Fuzziness and Medicine: Philosophical Reflections and Application Systems in Health Care ,
Studies in Fuzziness and Soft Computing, R. Seising and M. Tabacchi eds. Volume 302, 2013, pp 323338
(with D. Picado and T. Vetterlein).
 Sequent of Relations Calculi: a Framework for Analytic Deduction in ManyValued Logics, Beyond two: Theory and applications of MultipleValued Logics, M. Fitting and E. Orlowska eds.,
PhysicaVerlag, 157180, 2003 (with M. Baaz and C.G. Fermüller). PDF
 A Natural Deduction System for Intuitionistic Fuzzy Logic, Lectures on Soft Computing and Fuzzy Logic, A. Di Nola, G. Gerla eds., PhysicaVerlag, 118, 2000
(with M. Baaz and C.G. Fermüller). PS
International Workshops
 Service QoS Composition at the Level of Part Names, Proceedings of WSFM 2006, LNCS 4184, 2437, 2006
(with M. Aiello, F. Rosenberg, C. Platzer and S. Dunstdar).
 A Guide to Quantified Propositional Gödel Logic, Proceedings of the IJCAR Workshop on Theory and Applications of Quantified Boolean Formulas (QBF 2001), Siena (Italy),
June 2001 (with M. Baaz , N. Preining and H. Veith).