Agata Ciabattoni

To Autonomous Agents (Deontic and Temporal Logics)

• Combining MORL with Restraining Bolts to Learn Normative Behaviour. IJCAI 2025 (with E. Neufeld and R. Tulcan)
• From Explicit Allowances to Defeasible Deontic Operators: A Modal View. PRIMA 2025.
  (with J. Dik, E. Lorini, D. Pichler and D. Rozplokhas) PDF
• Tackling Temporal Deontic Challenges with Equilibrium Logic. AAMAS 2025 (with D Solda, P. Cabalar and E. Neufeld)
• Norm Compliance in Reinforcement Learning Agents via Restraining Bolts. JURIX 2024 (with E. Neufeld, and R. Tulcan)
• Deontic Equilibrium Logic with eXplicit negation. JELIA 2023 (with P. Cabalar, and L. van der Torre)
  
• Deontic Paradoxes in ASP with Weak Constraints. Technical Communication at ICLP 2023 (with C. Hatschka and T. Eiter)
  
• On Normative Reinforcement Learning via Safe Reinforcement Learning. PRIMA 2022. (with E. Neufeld and E. Bartocci).
  
• Enforcing Ethical Goals over Reinforcement Learning Policies. J. of Ethics and Information Technology. 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 Legal Reasoning

• The Result Model under Inconsistent Knowledge: Theory and Experiments. JURIX2025.
  (with Y. Morello and M. Gray)
• From Legal Texts to Defeasible Deontic Logic via LLMs: A Study in Automated Semantic Analysis. ASAIL 2025
  (with E. Horner, C. Mateis and G. Governatori)
• A Bayesian View of the Result Model. DIGHUM-25. (with Y.Morello)
• Deontic Explanations in Aqvist's Systems. DEON 2025 (with B. Istenic Urh and X. Parent) PDF
• Tackling Temporal Deontic Challenges with Equilibrium Logic. AAMAS 2025 (with D Solda, P. Cabalar and E. Neufeld)
• Deontic Equilibrium Logic with eXplicit negation. JELIA 2023 (with P. Cabalar, and L. van der Torre)
  
• Permissions in a Kelsenian perspective. Proc. of the 36th International Conference on Legal Knowledge Representation and Information Systems JURIX 2023 , IOS Press. (with X. Parent and G. Sartor)
  
• 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)
  

To Concurrency Theory and Foundations of Functional Programming Languages (Intermediate Logics)

• A typed parallel lambda calculus via 1-depth 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 (Many-valued Logics)

• Bilattice CADIAG-II: Theory and Experimental Results. International Conference on Artificial Intelligence and Computational Intelligence (AICI 2021). (with. P. Baldi and K-P. 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 CADIAG-2, Fuzzy Sets and Systems, 161(14): 1941-1958, 2010 (with T. Vetterlein). PDF
• Formal approaches to rule-based systems in medicine: the case of CADIAG2, Journal of Approximate Reasoning 54(1): 132-148, 2013 (with D. Picado, T. Vetterlein and M. El-Zekey).
• 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 CADIAG-2, Medical Informatics Europe, MIE 2009, Sarajevo, Studies in Health Technology and Informatics series, IOS Press (with T. Vetterlein and K-P. Adlassnig)

To Universal Algebra (Substructural Logics)

• Algebraic proof theory: hypersequents and hypercompletions, Annals of Pure and Applied Logic, 693-737, 2017 (with N. Galatos and K. Terui). PDF
• MacNeille Completions of FL-algebras, Algebra Universalis 66(4): 405-420, 2011 (with N. Galatos and K. Terui). PDF
• Algebraic proof theory for substructural logics: cut-elimination and completions, Annals of Pure and Applied Logic, 163(3): 266-290, 2012 (with N. Galatos and K. Terui). PDF
• Uniform proofs of standard completeness for extensions of first-order MTL. Theoretical Computer Science vol. 603: 43-57 (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, 154-167, Springer, Heidelberg, 2012 (with P. Baldi and L. Spendier). PDF
• Density Elimination, Theoretical Computer Science 403(2-3): 328-346, 2008 (with G. Metcalfe). PDF
• Density Elimination and Rational Completeness for First-Order Logics, Symposium on Logical Foundations of Computer Science (LFCS'07), LNCS 4514, 132-146, 2007 (with G. Metcalfe). PDF
• Standard completeness for uninorm-based logics, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2015), Waterloo (Canada), (with P. Baldi).

To Computational Trust (Conditional Logics)

• Support + Belief = Decision Trust. SIROCCO 2025 (with A. Aldini, D. Pichler and Mirko Tagliaferri)

Normative Reasoning

• From Explicit Allowances to Defeasible Deontic Operators: A Modal View. PRIMA 2025.
  (with J. Dik, E. Lorini, D. Pichler and D. Rozplokhas) PDF
• GL-based calculi for PCL and its deontic cousin. JELIA 2025 (with D.Rozplokhas and M. Tesi)
• Combining MORL with Restraining Bolts to Learn Normative Behaviour. IJCAI 2025 (with E. Neufeld and R. Tulcan)
• Deontic Explanations in Aqvist's Systems. DEON 2025 (with B. Istenic Urh and X. Parent) PDF
• Tackling Temporal Deontic Challenges with Equilibrium Logic. AAMAS 2025 (with D. Solda, P. Cabalar and E. Neufeld)
• Mimamsa on better not permissions. J. of Philosophical Logic. 2025. (with J. Dik, and E. Freschi)
• Norm Compliance in Reinforcement Learning Agents via Restraining Bolts. JURIX 2024 (with E. Neufeld, and R. Tulcan)
• Streamlining Input/Output Logics with Sequent Calculi (Extended Abstract). IJCAI 2024 Sister Conferences Best Paper Track. (with D. Rozplokhas)
• Sequents vs hypersequents for Aqvist systems IJCAR 2024 (with M. Tesi)
• Deontic Equilibrium Logic with eXplicit negation. JELIA 2023 (with P. Cabalar, and L. van der Torre)
• Streamlining Input/Output Logics with Sequent Calculi. KR 2023 (with D. Rozplokhas)
• Disambiguating permissions: A contribution from Mimamsa, DEON 2023 , (with J. Dik and E. Freschi)
• Deontic Paradoxes in ASP with Weak Constraints. Technical Communication at ICLP 2023 (with C. Hatschka and T. Eiter)
• Analytic proof theory for Aqvist’s system F, DEON 2023 , (with N. Olivetti, X. Parent, R. Ramanayake and D. Rozplokhas)
• 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): 351-394. 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 sequent-based 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

Automated Support for the Investigation of non-classical 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, 154-167, 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, 229-240, 2008 (with N. Galatos and K. Terui). PDF | Software

(Systematic and) Automated Introduction of Analytic Calculi for non-classical logics

• Bunched Hypersequent Calculi for Distributive Substructural Logics. Proceedings of LPAR 2017, (with R. Ramanayake). PDF
• Embedding formalisms: hypersequents and two-level 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 Co-NP Completeness for Many-Valued 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 many-valued logics: semi-projective logics. Theoretical Computer Science 480: 26-42 (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: cut-elimination and completions, Annals of Pure and Applied Logic, 163(3): 266-290, 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, 229-240, 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, 505-517. PDF
• Sequent of Relations Calculi: a Framework for Analytic Deduction in Many-Valued Logics, Beyond two: Theory and applications of Multiple-Valued Logics, M. Fitting and E. Orlowska eds., Physica-Verlag, 157-180, 2003 (with M. Baaz and C.G. Fermüller). PDF

Algebraic Proof Theory

• Algebraic proof theory: hypersequents and hypercompletions, Annals of Pure and Applied Logic, 693-737, 2017 (with N. Galatos and K. Terui). PDF
• MacNeille Completions of FL-algebras, Algebra Universalis 66(4): 405-420, 2011 (with N. Galatos and K. Terui). PDF
• Algebraic proof theory for substructural logics: cut-elimination and completions, Annals of Pure and Applied Logic, 163(3): 266-290, 2012 (with N. Galatos and K. Terui). PDF
• Standard completeness for extensions of IMTL. Proceedings of FUZZ-IEEE 2017: International Conference on Fuzzy Systems, (with P. Baldi and F. Gulisano) PDF
• Uniform proofs of standard completeness for extensions of first-order MTL. Theoretical Computer Science vol. 603: 43-57 (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, 154-167, Springer, Heidelberg, 2012 (with P. Baldi and L. Spendier). PDF
• Density Elimination, Theoretical Computer Science 403(2-3): 328-346, 2008 (with G. Metcalfe). PDF
• Density Elimination and Rational Completeness for First-Order Logics, Symposium on Logical Foundations of Computer Science (LFCS'07), LNCS 4514, 132-146, 2007 (with G. Metcalfe). PDF
• Standard completeness for uninorm-based logics, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2015), Waterloo (Canada), (with P. Baldi).
• Towards a semantic characterization of cut-elimination, Studia logica 82(1): 95-119, 2006 (with K. Terui). PDF (Addenda)

Automated Deduction

• Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. KR 2024 (with C. Eisenhofer, and D. Rozplokhas)
• Sequents vs hypersequents for Aqvist systems IJCAR 2024 (with M. Tesi)
• Streamlining Input/Output Logics with Sequent Calculi. Accepted to KR 2023 (with D. Rozplokhas)
• Analytic proof theory for Aqvist’s system F, DEON 2023 , (with N. Olivetti, X. Parent, R. Ramanayake and D. Rozplokhas)
• Dyadic Obligations: Proofs and Countermodels via Hypersequents. PRIMA 2022. (with N.Olivetti and X. Parent)
• A Normative Supervisor for Reinforcement Learning Agents. CADE 2021. (with E. Neufeld, Ezio Bartocci and Guido Governatori).
• From cut-free 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, 201-216 (with M. Baaz and C.G. Fermüller). PDF

Structural Proof Theory

• Analytic Proofs for Tense Logic. TABLEAUX 2025 (with T. Lang and R.Ramanayake) PDF
• GL-based calculi for PCL and its deontic cousin. JELIA 2025 (with D.Rozplokhas and M. Tesi)
• Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. KR 2024 (with C. Eisenhofer, and D. Rozplokhas)
• Streamlining Input/Output Logics with Sequent Calculi (Extended Abstract). IJCAI 2024 Sister Conferences Best Paper Track. (with D. Rozplokhas)
• Sequents vs hypersequents for Aqvist systems IJCAR 2024 (with M. Tesi)
• Streamlining Input/Output Logics with Sequent Calculi. KR 2023 (with D. Rozplokhas)
• Cut-restrictions: from cuts to analytic cuts, LICS 2023 , (with T. Lang and R. Ramanayake) PDF
• Analytic proof theory for Aqvist’s system F, DEON 2023 , (with N. Olivetti, X. Parent, R. Ramanayake and D. Rozplokhas)
• 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 . 2021. PDF (with T. Lang and R. Ramanayake).
• Display to Labeled Proofs and Back Again for Tense Logics. ACM TOCL . 2021. (with T. Lyon, R. Ramanayake and A. Tiu).
• Bounded sequent calculi for non-classical 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): 1-27, 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): 1245-1294 (2014)
  (with R. Ramanayake and H. Wansing)
• Embedding formalisms: hypersequents and two-level systems of rules. Proceedings of AIML 2016 , (with F. Genco) PDF
• Proof theory of witnessed Goedel logic: a negative result. 26(1): 51-64 (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 proof-theoretic characterizations of truth stressers for MTL and its extensions, Fuzzy Sets and Systems, 161(3): 369-389, 2010 (with G. Metcalfe and F. Montagna). PDF
• Density Elimination, Theoretical Computer Science 403(2-3): 328-346, 2008 (with G. Metcalfe). PDF
• Towards an Algorithmic Construction of Cut-Elimination Procedures, Mathematical Structures in Computer Science 18(1): 81-105, 2008 (with A. Leitsch). PDF
• Towards a semantic characterization of cut-elimination, Studia logica 82(1): 95-119, 2006 (with K. Terui). PDF (Addenda)
• A Proof-theoretical Investigation of Global Intuitionistic (Fuzzy) Logic, Archive of Mathematical Logic 44: 435-457, 2005. PDF
• Analytic Calculi for Monoidal T-norm Based Logic, Fundamenta Informaticae, Vol. 59, N. 4, 315-332, 2004, (with M. Baaz and F. Montagna). PS
• Hypersequent Calculi for Gödel Logics - a Survey, Journal of Logic and Computation 13: 835-861, 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): 283-294, 2001 (with M. Ferrari). PDF (Corrigenda)
• Finiteness of infinite-valued Lukasiewicz logic, Journal of Logic, Language and Information 9: 5-29, 2000 (with S. Aguzzoli). PS
• Sequent calculi for finite-valued Lukasiewicz logics via boolean decompositions, Journal of Logic and Computation 10(2): 213-222, 2000 (with S. Aguzzoli and A. Di Nola).
• Cut free proof systems for logics of weak excluded middle, Soft Computing 2(4): 147-156, 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 Matrix-based Semantics, Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods, LNCS 6793, 119-133, Tableaux 2011 (with O. Lahav and A. Zamansky). PDF
• Canonical Calculi: Invertibility, Axiom-Expansion 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, 451-466 (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, 229-240, 2008 (with N. Galatos and K. Terui). PDF | Software
• Density Elimination and Rational Completeness for First-Order Logics, Symposium on Logical Foundations of Computer Science (LFCS 2007), LNCS 4514, 132-146, 2007 (with G. Metcalfe). PDF
• Modular Cut-Elimination: Finding Proofs or Counterexamples, Logic for Programming and Automated Reasoning (LPAR 2006), LNAI 4246, 135-149, 2006 (with K. Terui). PDF
• Uniform Rules and Dialogue Games for Fuzzy Logics, Logic for Programming and Automated Reasoning (LPAR 2005), LNAI 3452, 496-510, 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, 505-517. PDF
• Bounded Lukasiewicz Logics, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2003), LNAI 2796, 32-47, 2003 (with G. Metcalfe). PS
• From Intuitionistic Logic to Gödel-Dummett Logic via Parallel Dialogue Games, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2003), Tokyo, (Japan), May 2003, 188-193 (with C.G. Fermüller). PDF
• A Schütte-Tait style cut-elimination proof for first-order Gödel logic, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2002), Copenhagen (Denmark), August 2002, LNAI 2381, 24-38 (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, 201-216 (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 Multiple-Valued Logic (ISMVL 2001), Warsaw (Poland), May 2001, IEEE Computer Society Press, 227-232 (with C.G. Fermüller).
• Cut-Elimination in a Sequents-of-Relations Calculus for Gödel Logic, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2001), Warsaw (Poland), May 2001, IEEE Computer Society Press, 181-186 (with M. Baaz and C.G. Fermüller).PDF
• Hypertableau and Path-Hypertableau Calculi for some families of intermediate logics, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2000), St. Andrews (Scotland), July 2000, LNAI 1847, 160-175 (with M. Ferrari). PS
• On Urquhart's C logic, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2000), Portland (USA), May 2000, IEEE Computer Society Press, 113-118. PS
• Bounded contraction in systems with linearity, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 1999), Saratoga (NY), June 1999, LNAI 1617, 113-128.
• Proof Theory of Fuzzy Logics: Urquhart's C and related logics, Mathematical Foundations of Computer Science (MFCS'98), Brno, August 1998, LNCS 1450, 203-212 (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, 128-139 (with D. Luchi).
• Sequent of Relations Calculi: a Framework for Analytic Deduction in Many-Valued Logics, Beyond two: Theory and applications of Multiple-Valued Logics, M. Fitting and E. Orlowska eds., Physica-Verlag, 157-180, 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., Physica-Verlag, 1-18, 2000 (with M. Baaz and C.G. Fermüller). PS

(Un)Decidability and Complexity

• Proof Search and Co-NP Completeness for Many-Valued Logics. Fuzzy Sets and Systems 292: 130-149 (2016)
  (with M. Bongini and F. Montagna).
• First-order satisfiability in Gödel logics: an NP-complete fragment, Theoretical Computer Science, 412: 6612-6623, 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, 77-91, 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, 240-257, (with M. Baaz and R. Zach). PS
• On the Undecidability of Some Sub-classical First-Order Logics, Foundations of Software Technology and Theoretical Computer Science (FST&TCS 1999), Chennai, December 1999, LNCS 1738, 258-268 (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): 1209-1214, 1997 (with A. Asperti).
• Effective Applicative Structures, Category Theory in Computer Science (CTCS 1995) Cambridge (UK), August 1995, LNCS 953, 81-95, (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, 162-175 (with A. Asperti). PDF

Non-deterministic 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 Matrix-based Semantics, Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods, LNCS 6793, 119-133, Tableaux 2011 (with O. Lahav and A. Zamansky). PDF
• Canonical Calculi: Invertibility, Axiom-Expansion and (Non)-determinism, Computer Science Symposium in Russia (CSR 2009), LNCS (with A. Avron and A. Zamansky). PDF

Specific Logics and Families of Logics

Conditional Logics

• GL-based calculi for PCL and its deontic cousin. JELIA 2025 (with D.Rozplokhas and M. Tesi)
• Support + Belief = Decision Trust. SIROCCO 2025 (with A. Aldini, D. Pichler and Mirko Tagliaferri)
• Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. KR 2024 (with C. Eisenhofer, and D. Rozplokhas)
• Streamlining Input/Output Logics with Sequent Calculi (Extended Abstract). IJCAI 2024 Sister Conferences Best Paper Track. (with D. Rozplokhas)
• Sequents vs hypersequents for Aqvist systems IJCAR 2024 (with M. Tesi)
• Streamlining Input/Output Logics with Sequent Calculi. KR 2023 (with D. Rozplokhas)
• Analytic proof theory for Aqvist’s system F, DEON 2023 , (with N. Olivetti, X. Parent, R. Ramanayake and D. Rozplokhas)
• Dyadic Obligations: Proofs and Countermodels via Hypersequents. PRIMA 2022. (with N.Olivetti and X. Parent)

T-norm based logics

• Standard completeness for extensions of IMTL. Proceedings of FUZZ-IEEE 2017: International Conference on Fuzzy Systems, (with P. Baldi and F. Gulisano) PDF
• Uniform proofs of standard completeness for extensions of first-order MTL. Theoretical Computer Science vol. 603: 43-57 (2015) (with P. Baldi)
• Standard completeness for uninorm-based logics, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2015), Waterloo (Canada), (with P. Baldi).
• Proof Search and Co-NP Completeness for Many-Valued Logics. Fuzzy Sets and Systems
  (with M. Bongini and F. Montagna).
• Proof theory for locally finite many-valued logics: semi-projective logics. Theoretical Computer Science 480: 26-42 (2013) (with F. Montagna).
• Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions, Fuzzy Sets and Systems, 161(3): 369-389, 2010 (with G. Metcalfe and F. Montagna). PDF
• Density Elimination, Theoretical Computer Science 403(2-3): 328-346, 2008 (with G. Metcalfe). PDF
• Analytic Calculi for Monoidal T-norm Based Logic, Fundamenta Informaticae, Vol. 59, N. 4, 315-332, 2004, (with M. Baaz and F. Montagna). PS
• T-norm based logics with n-contraction, Neural Network World 12(5): 441-452, 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 Multiple-Valued Logic (ISMVL 2001), Warsaw (Poland), May 2001, IEEE Computer Society Press, 227-232 (with C.G. Fermüller).
• Sequent of Relations Calculi: a Framework for Analytic Deduction in Many-Valued Logics, Beyond two: Theory and applications of Multiple-Valued Logics, M. Fitting and E. Orlowska eds., Physica-Verlag, 157-180, 2003 (with M. Baaz and C.G. Fermüller). PDF

Lukasiewicz Logic

• Finiteness of infinite-valued Lukasiewicz logic, Journal of Logic, Language and Information 9: 5-29, 2000 (with S. Aguzzoli). PS
• Sequent calculi for finite-valued Lukasiewicz logics via boolean decompositions, Journal of Logic and Computation 10(2): 213-222, 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, 496-510, 2004 (with C. Fermüller and G. Metcalfe). PDF
• Bounded Lukasiewicz Logics, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2003), LNAI 2796, 32-47, 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, 128-139 (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. 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
• First-order satisfiability in Gödel logics: an NP-complete fragment, Theoretical Computer Science, 412: 6612-6623, 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, 77-91, 2007 (with M. Baaz and C.G. Fermüller). PDF
• Hypersequent Calculi for Gödel Logics - a Survey, Journal of Logic and Computation 13: 835-861, 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, 451-466 (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, 496-510, 2004 (with C. Fermüller and G. Metcalfe). PDF
• From Intuitionistic Logic to Gödel-Dummett Logic via Parallel Dialogue Games, IEEE International Symposium on Multiple-Valued Logic (ISMVL 2003), Tokyo, (Japan), May 2003, 188-193 (with C.G. Fermüller). PDF
• A Schütte-Tait style cut-elimination proof for first-order Gödel logic, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2002), Copenhagen (Denmark), August 2002, LNAI 2381, 24-38 (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, 201-216 (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, 240-257, (with M. Baaz and R. Zach). PS
• Sequent of Relations Calculi: a Framework for Analytic Deduction in Many-Valued Logics, Beyond two: Theory and applications of Multiple-Valued Logics, M. Fitting and E. Orlowska eds., Physica-Verlag, 157-180, 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., Physica-Verlag, 1-18, 2000 (with M. Baaz and C.G. Fermüller). PS

Web Services

• Service QoS Composition at the Level of Part Names, Proceedings of WS-FM 2006, LNCS 4184, 24-37, 2006 (with M. Aiello, F. Rosenberg, C. Platzer and S. Dunstdar).