Applications of nonclassical logics
To Sanskrit Philosophy
Deontic paradoxes in Mimamsa logics: there and back again.
J. of Logic, Language and Information. 2022.
(with K. van Berkel. E. Freschi, F. Gulisano and M. Olszewski)
The Gentle Murder
Paradox in Sanskrit Philosophy. DEON 2020/2021.
PDF
(with K. van Berkel. E. Freschi, F. Gulisano and M. Olszewski)
Mimamsa Deontic Reasoning using Specificity: A Proof Theoretic Approach.
Artificial Intelligence and Law , 29(3): 351394. 2021.
(with F. Gulisano and B. Lellmann). PDF
Evaluating Networks of Arguments: A Case Study in Mimamsa
Dialectics, Proceedings of LORI 2019 ,
(with K. van Berkel, E. Freschi and S. Modgil)
PDF
Sequent Rules
for Reasoning and Conflict Resolution in Conditional Norms, Proceedings of DEON 2020/2021 ,
PDF
(with B. Lellmann)
Resolving conflicting obligations in Mimamsa: a sequentbased approach. Proceedings of DEON 2018,
(with F. Gulisano and B. Lellmann)
PDF
Understanding Prescriptive Texts: Rules and Logic as elaborated by the Mimamsa school.
Confluence: Online Journal of World Philosophies ,
2(1), pp.4766, 2017. (with E. Freschi, F. Genco and B. Lellmann).
PDF
Mimamsa Deontic Logic: Proof Theory and Applications. Proceedings of TABLEAUX 2015, (with E. Freschi, F. Genco and B. Lellmann)
PDF
To Autonomous Agents and Legal Reasoning
On Normative Reinforcement Learning via Safe Reinforcement Learning.
PRIMA 2022.
(with E. Neufeld and E. Bartocci).
A Kelsenian deontic logic. Proc. of the 34th International Conference on Legal
Knowledge Representation and Information Systems JURIX 2021 , IOS Press.
(with X. Parent and G. Sartor)
Enforcing Ethical Goals over Reinforcement Learning Policies.
J. of Ethics and Information Technology. Accepted 2021.
(with E. Neufeld, E. Bartocci and G. Governatori).
A Normative Supervisor for Reinforcement Learning Agents.
CADE 2021 .
(with E. Neufeld, E. Bartocci and G. Governatori).
To Concurrency Theory and Foundations of Functional Programming Languages

A typed parallel lambda calculus via 1depth intermediate proofs,
Proceedings of LPAR 2020 ,
(with F. Aschieri and F. Genco)
PDF
 On the Concurrent Computational
Content of Intermediate Logics.
Theoretical Computer science, 2020 . (with F. Aschieri and F. Genco). PDF
 Classical Proofs as parallel programs.
Proceedings of Gandalf 2018, (with F. Aschieri and F. Genco).
PDF
 Goedel Logic: From Natural Deduction to Parallel Computation.
Proceedings of LICS 2017, (with F. Aschieri and F. Genco).
PDF
To Medical Expert Systems

Bilattice CADIAGII: Theory and Experimental Results.
International Conference on Artificial Intelligence and Computational Intelligence (AICI 2021). (with. P. Baldi and KP. Adlassnig)
 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
 On the (fuzzy) logical content of CADIAG2, Fuzzy Sets and Systems, 161(14): 19411958, 2010
(with T. Vetterlein). 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).
 Towards an interpretation of the medical expert system CADIAG2. Fuzziness and Medicine: Philosophy and Application Systems, R. Seising and M. Tabacchi eds.
(with D. Picado and T. Vetterlein).
 A formal logical framework for CADIAG2, Medical Informatics Europe, MIE 2009, Sarajevo, Studies in Health Technology and Informatics series, IOS Press
(with T. Vetterlein and KP. Adlassnig)
To Universal Algebra
Algebraic proof theory: hypersequents and hypercompletions, Annals of Pure and Applied Logic,
693737, 2017 (with N. Galatos and K. Terui).
PDF
MacNeille Completions of FLalgebras, Algebra Universalis 66(4): 405420, 2011
(with N. Galatos and K. Terui). 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
Uniform proofs of standard completeness for extensions of firstorder MTL.
Theoretical Computer Science vol. 603: 4357 (2015)
(with P. Baldi)
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
Density Elimination, Theoretical Computer Science 403(23): 328346, 2008
(with G. Metcalfe). PDF
Density Elimination and Rational Completeness for FirstOrder Logics, Symposium on Logical Foundations of Computer Science (LFCS'07), LNCS 4514, 132146, 2007
(with G. Metcalfe). PDF
Standard completeness for uninormbased logics, IEEE International Symposium on MultipleValued Logic (ISMVL 2015), Waterloo (Canada),
(with P. Baldi).
Automated Support for the Investigation of nonclassical logics
 Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. TOCL 16(1): 5 (2014)
(with O. Lahav, L. Spendier and A. Zamansky),
 Software
 Tools for the investigation of substructural and paraconsistent logics. JELIA 2014,
(with L. Spendier) PDF
 Software
 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
 Hypersequent and Labelled Calculi for Intermediate Logics, Proceedings of TABLEAUX 2013,
(with P. Maffezioli and L. Spendier) 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
 Software
 Expanding the realm of systematic proof theory, Computer Science Logic, CSL 2009, LNCS
(with L. Strassburger and K. Terui). PDF  Software
 From axioms to analytic rules in nonclassical logics, IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE, 229240, 2008
(with N. Galatos and K. Terui). PDF  Software
(Systematic and) Automated Introduction of Analytic Calculi for nonclassical logics
 Bunched Hypersequent Calculi for Distributive Substructural Logics.
Proceedings of LPAR 2017, (with R. Ramanayake).
PDF
 Embedding formalisms: hypersequents and twolevel systems of rules. Proceedings of AIML 2016 , (with F. Genco)
PDF
 Power and limits of structural display rules. ACM TOCL 17(3), 2016
(with R. Ramanayake). PDF
 Proof Search and CoNP Completeness for ManyValued Logics. Fuzzy Sets and Systems
(with M. Bongini and F. Montagna).
 Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. TOCL 16(1): 5 (2014)
(with O. Lahav, L. Spendier and A. Zamansky)
 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
 Proof theory for locally finite manyvalued logics: semiprojective logics. Theoretical Computer Science
480: 2642 (2013)
(with F. Montagna).
 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
 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
 Expanding the realm of systematic proof theory, Computer Science Logic, CSL 2009, LNCS
(with L. Strassburger and K. Terui). PDF
 From axioms to analytic rules in nonclassical logics, IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE, 229240, 2008
(with N. Galatos and K. Terui). PDF  Software
 Automated Generation of Analytic Calculi for Logics with Linearity, Computer Science Logic (CSL 2004), LNCS 3210, 505517.
PDF
 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
Normative Reasoning
Dyadic Obligations: Proofs and Countermodels via Hypersequents.
PRIMA 2022. (with N.Olivetti and X. Parent)
A Kelsenian deontic logic. Accepted for publication at JURIX 2021.
(with X. Parent and G. Sartor)
Deontic paradoxes in Mimamsa logics: there and back again.
J. of Logic, Language and Information. 2022.
(with K. van Berkel. E. Freschi, F. Gulisano and M. Olszewski)
The Gentle Murder
Paradox in Sanskrit Philosophy. DEON 2020/2021.
(with K. van Berkel. E. Freschi, F. Gulisano and M. Olszewski)
Mimamsa Deontic Reasoning using Specificity: A Proof Theoretic Approach.
Artificial Intelligence and Law , 29(3): 351394. 2021
(with F. Gulisano and B. Lellmann).
Sequent Rules for Reasoning and Conflict Resolution in Conditional Norms, Proceedings of DEON 2020/2021 ,
PDF
(with B. Lellmann)
Resolving conflicting obligations in Mimamsa: a sequentbased approach. Proceedings of DEON 2018,
(with F. Gulisano and B. Lellmann)
PDF
Mimamsa Deontic Logic: Proof Theory and Applications. Proceedings of TABLEAUX 2015, (with E. Freschi, F. Genco and B. Lellmann)
PDF
Algebraic Proof Theory
 Algebraic proof theory: hypersequents and hypercompletions, Annals of Pure and Applied Logic,
693737, 2017 (with N. Galatos and K. Terui).
PDF
 MacNeille Completions of FLalgebras, Algebra Universalis 66(4): 405420, 2011
(with N. Galatos and K. Terui). 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
 Standard completeness for extensions of IMTL. Proceedings of FUZZIEEE 2017:
International Conference on Fuzzy Systems, (with P. Baldi and F. Gulisano)
PDF
 Uniform proofs of standard completeness for extensions of firstorder MTL.
Theoretical Computer Science vol. 603: 4357 (2015)
(with P. Baldi)
 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
 Density Elimination, Theoretical Computer Science 403(23): 328346, 2008
(with G. Metcalfe). PDF
 Density Elimination and Rational Completeness for FirstOrder Logics, Symposium on Logical Foundations of Computer Science (LFCS'07), LNCS 4514, 132146, 2007
(with G. Metcalfe). PDF
 Standard completeness for uninormbased logics, IEEE International Symposium on MultipleValued Logic (ISMVL 2015), Waterloo (Canada),
(with P. Baldi).
 Towards a semantic characterization of cutelimination, Studia logica 82(1): 95119, 2006
(with K. Terui). PDF (Addenda)
Automated Deduction

A Normative Supervisor for Reinforcement Learning Agents.
CADE 2021. (with E. Neufeld, Ezio Bartocci and Guido Governatori).
 From cutfree calculi to automated deduction: the case of bounded contraction,
ENTCS, 2017 (with B, Lellmann, C. Olarte and E. Pimentel).
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
 Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving,
Logic for Programming and Automated Reasoning (LPAR 2001), Cuba, December 2001, LNAI 2250, 201216 (with M. Baaz and C.G. Fermüller).
PDF
Structural Proof Theory

Taming Bounded Depth with Nested Sequents.
AIML 2022. (with L. Strassburger and M. Tesi)

Dyadic Obligations: Proofs and Countermodels via Hypersequents.
PRIMA 2022. (with N.Olivetti and X. Parent)
 Bounded sequent calculi and restricted
embeddings: hypersequent logics.
J. of Symbolic Logic . Accepted 2021.
PDF
(with T. Lang and R. Ramanayake).
 Display to Labeled Proofs and Back Again for Tense Logics.
ACM TOCL . Accepted, 2021. (with T. Lyon, R. Ramanayake and A. Tiu).
 Bounded sequent calculi for nonclassical logics via hypersequents , Proceedings of TABLEAUX 2019 ,
(with T. Lang and R. Ramanayake)
PDF
 Hypersequents and Systems of Rules: Embeddings and Applications. ACM TOCL 19(2): 127, 2018.
(with F. Genco).
PDF
 From Display to Labelled Proofs for Tense Logics. Proceedings of LFCS 2018, (with T. Lyon and R. Ramanayake).
PDF
 Power and limits of structural display rules. ACM TOCL 17(3), 2016
(with R. Ramanayake). PDF
 Hypersequent and display calculi  a unified perspective. Studia Logica 102(6): 12451294 (2014)
(with R. Ramanayake and H. Wansing)
 Embedding formalisms: hypersequents and twolevel systems of rules. Proceedings of AIML 2016 , (with F. Genco)
PDF
 Proof theory of witnessed Goedel logic: a negative result.
26(1): 5164 (2016) Journal of Logic and Computation
(with M. Baaz)
 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
 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
 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).
 Expanding the realm of systematic proof theory, Computer Science Logic, CSL 2009, LNCS
(with L. Strassburger and K. Terui). 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
 Canonical Calculi: Invertibility, AxiomExpansion and (Non)determinism, Computer Science Symposium in Russia (CSR 2009), LNCS
(with A. Avron and A. Zamansky). PDF
 Cut elimination for first order Gödel logic by hyperclause resolution, 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, IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE, 229240, 2008
(with N. Galatos and K. Terui). PDF  Software
 Density Elimination and Rational Completeness for FirstOrder Logics, Symposium on Logical Foundations of Computer Science (LFCS 2007), LNCS 4514, 132146, 2007
(with G. Metcalfe). PDF
 Modular CutElimination: Finding Proofs or Counterexamples, Logic for Programming and Automated Reasoning (LPAR 2006), LNAI 4246, 135149, 2006
(with K. Terui). PDF
 Uniform Rules and Dialogue Games for Fuzzy Logics, 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, Computer Science Logic (CSL 2004), LNCS 3210, 505517.
PDF
 Bounded Lukasiewicz Logics, 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, 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, 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,
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, 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, 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
 Hypertableau and PathHypertableau Calculi for some families of intermediate logics, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2000),
St. Andrews (Scotland), July 2000, LNAI 1847, 160175 (with M. Ferrari). PS
 On Urquhart's C logic, IEEE International Symposium on MultipleValued Logic (ISMVL 2000), Portland (USA), May 2000, IEEE Computer Society Press, 113118.
PS
 Bounded contraction in systems with linearity, 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, 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, Computational Logic and Proof Theory  Kurt Gödel Colloquium (KGC 1997), Vienna, August 1997, LNCS 1289, 128139
(with D. Luchi).
 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
(Un)Decidability and Complexity
 Proof Search and CoNP Completeness for ManyValued Logics.
Fuzzy Sets and Systems 292: 130149 (2016)
(with M. Bongini and F. Montagna).
 Firstorder satisfiability in Gödel logics: an NPcomplete fragment, Theoretical Computer Science, 412: 66126623, 2011
(with M. Baaz and N. Preining). PDF
 SAT in Monadic Gödel Logics: a borderline between decidability and undecidability, Workshop on Logic, Language, Information and Computation, WOLLIC 2009, LNAI
(with M. Baaz and N. Preining). PDF
 Monadic Fragments of Gödel Logics: Decidability and Undecidability Results, Logic for Programming and Automated Reasoning (LPAR 2007), LNAI 4790, 7791, 2007
(with M. Baaz and C.G. Fermüller). PDF
 Quantified Propositional Gödel Logic, Logic for Programming and Automated Reasoning (LPAR'2000), Reunion Island, November 2000, LNAI 1955, 240257,
(with M. Baaz and R. Zach). PS
 On the Undecidability of Some Subclassical FirstOrder Logics, 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
Computability Theory and Partial Combinatory Algebras
 A Sufficient Condition for Completability of Partial Combinatory Algebras, Journal of Symbolic Logic 62(4): 12091214, 1997
(with A. Asperti).
 Effective Applicative Structures, Category Theory in Computer Science (CTCS 1995) Cambridge (UK), August 1995, LNCS 953, 8195,
(with A. Asperti). PDF
 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
Nondeterministic Matrices
 Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. TOCL 16(1): 5 (2014)
(with O. Lahav, L. Spendier and A. Zamansky)
 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
 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
 Canonical Calculi: Invertibility, AxiomExpansion and (Non)determinism, Computer Science Symposium in Russia (CSR 2009), LNCS
(with A. Avron and A. Zamansky). PDF
Specific Logics and Families of Logics
Tnorm based logics
 Standard completeness for extensions of IMTL. Proceedings of FUZZIEEE 2017:
International Conference on Fuzzy Systems, (with P. Baldi and F. Gulisano)
PDF
 Uniform proofs of standard completeness for extensions of firstorder MTL.
Theoretical Computer Science vol. 603: 4357 (2015)
(with P. Baldi)
 Standard completeness for uninormbased logics, IEEE International Symposium on MultipleValued Logic (ISMVL 2015), Waterloo (Canada),
(with P. Baldi).
 Proof Search and CoNP Completeness for ManyValued Logics. Accepted for Publication in Fuzzy Sets and Systems
(with M. Bongini and F. Montagna).
 Proof theory for locally finite manyvalued logics: semiprojective logics. Theoretical Computer
Science 480: 2642 (2013)
(with F. Montagna).
 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
 Analytic Calculi for Monoidal Tnorm Based Logic, Fundamenta Informaticae, Vol. 59, N. 4, 315332, 2004,
(with M. Baaz and F. Montagna). PS
 Tnorm based logics with ncontraction, Neural Network World 12(5): 441452, 2002
(with F. Esteva and L. Godo). PS
 Hypersequents as a uniform framework for Urquhart's C, MTL and related logics, IEEE International Symposium on MultipleValued Logic (ISMVL 2001), Warsaw (Poland),
May 2001, IEEE Computer Society Press, 227232 (with C.G. Fermüller).
 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
Lukasiewicz Logic
 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).
 Uniform Rules and Dialogue Games for Fuzzy Logics, Logic for Programming and Automated Reasoning (LPAR 2005), LNAI 3452, 496510, 2004
(with C. Fermüller and G. Metcalfe). PDF
 Bounded Lukasiewicz Logics, Automated Reasoning with Analytic Tableaux and Related Methods
(Tableaux 2003), LNAI 2796, 3247, 2003 (with G. Metcalfe). PS
 Two connections between Linear Logic and Lukasiewicz Logic, Computational Logic and Proof Theory  Kurt Gödel Colloquium (KGC'97), Vienna, August 1997, LNCS 1289, 128139
(with D. Luchi).
Gödel Logics
 Goedel Logic: From Natural Deduction to Parallel Computation.
Proceedings of LICS 2017, (with F. Aschieri and F. Genco).
PDF
 Proof theory of witnessed Goedel logic: a negative result. Accepted for Publication in Journal of Logic and Computation
(with M. Baaz)
 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
 Firstorder satisfiability in Gödel logics: an NPcomplete fragment, Theoretical Computer Science, 412: 66126623, 2011
(with M. Baaz and N. Preining). PDF
 SAT in Monadic Gödel Logics: a borderline between decidability and undecidability, Workshop on Logic, Language, Information and Computation, WOLLIC 2009, LNAI
(with M. Baaz and N. Preining). PDF
 Monadic Fragments of Gödel Logics: Decidability and Undecidability Results, Logic for Programming and Automated Reasoning (LPAR 2007), LNAI 4790, 7791, 2007
(with M. Baaz and C.G. Fermüller). PDF
 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
 Cut elimination for first order Gödel logic by hyperclause resolution, Logic for Programming and Automated Reasoning (LPAR 2008), LNCS 5330, 451466
(with M. Baaz and C.G. Fermüller). PDF
 Uniform Rules and Dialogue Games for Fuzzy Logics, Logic for Programming and Automated Reasoning (LPAR 2005), LNAI 3452, 496510, 2004
(with C. Fermüller and G. Metcalfe). PDF
 From Intuitionistic Logic to GödelDummett Logic via Parallel Dialogue Games, 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, 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,
Logic for Programming and Automated Reasoning (LPAR 2001), Cuba, December 2001, LNAI 2250, 201216 (with M. Baaz and C.G. Fermüller).
PDF
 Quantified Propositional Gödel Logic, Logic for Programming and Automated Reasoning (LPAR'2000), Reunion Island, November 2000, LNAI 1955, 240257,
(with M. Baaz and R. Zach). PS
 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
Web Services