Algebraic Proof Theory

• MacNeille Completions of FL-algebras. Submitted.
  (with N. Galatos and K. Terui ) Abstract

• Algebraic proof theory for substructural logics: cut-elimination and completions. Submitted.
  (with N. Galatos and K. Terui ) Abstract

• Density Elimination. Theoretical Computer Science 403(2-3), pp. 328--346. 2008.
  (with G. Metcalfe ) PDF.

• Towards a semantic characterization of cut-elimination . Studia logica . Vol. 82(1). pp. 95 - 119. 2006.
  (with K. Terui ). PDF. ( Addenda )

• Density Elimination and Rational Completeness for First-Order Logics. Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS'07) . LNCS 4514. pp. 132-146. 2007.
  (with G. Metcalfe ) PDF.

Structural Proof Theory

• Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions. Fuzzy Sets and Systems. Accepted for publication 2009.
  (with G. Metcalfe and F. Montagna ) PDF.

• Density Elimination. Theoretical Computer Science 403(2-3), pp. 328--346. 2008.
  (with G. Metcalfe ) PDF.

• Towards an Algorithmic Construction of Cut-Elimination Procedures . Mathematical Structures in Computer Science 18(1), pp. 81--105. 2008.
  (with A. Leitsch )

• Towards a semantic characterization of cut-elimination . Studia logica . Vol. 82(1). pp. 95 - 119. 2006.
  (with K. Terui ). PDF. ( Addenda )

• A Proof-theoretical Investigation of Global Intuitionistic (Fuzzy) Logic . Archive of Mathematical Logic . vol. 44. pp. 435-457. 2005. PDF.

• Analytic Calculi for Monoidal T-norm Based Logic. Fundamenta Informaticae . vol. 59, Number 4, pp. 315-332. 2004.
  (with M. Baaz and F. Montagna ). PDF.

• Hypersequent Calculi for Gödel Logics --- a Survey. Journal of Logic and Computation . vol. 13. pp. 835 - 861. 2003.
  (with M. Baaz and C.G. Fermüller ). PDF.

• T-norm based logics with n-contraction. Neural Network World . vol. 12. n. 5. pp. 441-452. 2002.
  (with F. Esteva and L. Godo ) PS.

• Hypersequent Calculi for some Intermediate Logics with Bounded Kripke Models. Journal of Logic and Computation, vol. 11. n. 2. pp. 283-294. 2001.
  (with M. Ferrari ) PDF. ( Corrigenda )

• Finiteness of infinite-valued Lukasiewicz logic. Journal of Logic, Language and Information , vol. 9, pp. 5-29, 2000.
  (with S. Aguzzoli ). PS.

• Sequent calculi for finite-valued Lukasiewicz logics via boolean decompositions, Journal of Logic and Computation , vol. 10. n. 2. pp. 213-222, 2000.
  (with S. Aguzzoli and A. Di Nola )

• Cut free proof systems for logics of weak excluded middle , Soft Computing , vol. 2. n. 4. pp. 147-156, 1998.
  (with D.M. Gabbay and N. Olivetti )

• Expanding the realm of systematic proof theory. Proceedings of Computer Science Logic CSL 2009 . LNCS.
  (with L. Strassburger and K. Terui ) PDF.

• Canonical Calculi: Invertibility, Axiom-Expansion and (Non)-determinism. Proceedings of the 4th Computer Science Symposium in Russia (CSR2009) Novosibirsk, Russia, 2009.
  (with A. Avron and A. Zamansky ) PDF.

• Cut elimination for first order Goedel logic by hyperclause resolution. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2008), LNCS 5330, pp. 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'08) , IEEE pp. 229-240, 2008.
  (with N. Galatos and K. Terui ) PDF.

• Density Elimination and Rational Completeness for First-Order Logics. Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS'07) . LNCS 4514. pp. 132-146. 2007.
  (with G. Metcalfe ) PDF.

• Modular Cut-Elimination: Finding Proofs or Counterexamples. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2006), LNAI 4246. pp. 135-149. 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. pp. 496-510. 2004.
  (with C. Fermüller and G. Metcalfe ) PS and PDF.

• Automated Generation of Analytic Calculi for Logics with Linearity. Proceedings of Computer Science Logic. (CSL04) . LNCS 3210 pp. 505-517. Karpacz, Poland. September 2004. PS and PDF

• Bounded Lukasiewicz Logics . Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods. (Tableaux 2003), Roma, Italy, September 2003. LNAI 2796. pp. 32-47. 2003.
  (with G. Metcalfe ) PS.

• From Intuitionistic Logic to Gödel-Dummett Logic via Parallel Dialogue Games. Proceedings of the 33th IEEE International Symposium on Multiple-Valued Logic (ISMVL'2003) , Tokyo, (Japan), May 2003. pp. 188-193.
  (with C.G. Fermüller ) PDF.

• A Schütte-Tait style cut-elimination proof for first-order Gödel logic. Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods. (Tableaux 2002), Copenhagen, Denmark, August 2002. LNAI 2381. pp. 24-38.
  (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. pp. 201-216.
  (with M. Baaz and C.G. Fermüller ) PDF.

• Hypersequents as a uniform framework for Urquhart's C, MTL and related logics. Proceedings of the 31th IEEE International Symposium on Multiple-Valued Logic (ISMVL'2001) , Warsaw (Poland), May 2001. IEEE Computer Society Press. pp. 227-232.
  (with C.G. Fermüller )

• Cut-Elimination in a Sequents-of-Relations Calculus for Gödel Logic. Proceedings of the 31th IEEE International Symposium on Multiple-Valued Logic (ISMVL'2001) , Warsaw (Poland), May 2001. IEEE Computer Society Press. pp. 181-186.
  (with M. Baaz and C.G. Fermüller ). PS.

• Hypertableau and Path-Hypertableau 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. pp. 160-175.
  (with M. Ferrari ). PS.

• On Urquhart's C logic, Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL'2000) , Portland (USA), May 2000. IEEE Computer Society Press. pp. 113-118. PS.

• Bounded contraction in systems with linearity, Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'99) Saratoga (NY), June 1999. LNAI 1617. pp. 113-128.

• 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. pp. 203-212.
  (with M. Baaz , C.G. Fermüller and H. Veith )

• Two connections between Linear Logic and Lukasiewicz Logic, Proceedings of the biennal conference Computational Logic and Proof Theory -- Kurt Gödel Colloquium (KGC'97), Vienna, August 1997. LNCS 1289, pp. 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. pp. 157-180. 2003.
  (with M. Baaz and C.G. Fermüller ). PS.

• A Natural Deduction System for Intuitionistic Fuzzy Logic, Lectures on Soft Computing and Fuzzy Logic , A. Di Nola, G. Gerla eds., Physica-Verlag. 2000, pp. 1-18.
  (with M. Baaz and C.G. Fermüller ) PS.

(Un)Decidability Results

• SAT in Monadic Goedel Logics: a borderline between decidability and undecidability. Proceedings of WOLLIC 2009 . LNAI.
  (with M. Baaz and N. Preining ) PDF.

• Monadic Fragments of Gödel Logics: Decidability and Undecidability Results. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2007), LNAI 4790. pp. 77-91. 2007.
  (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. pp. 240-257.
  (with M. Baaz and R. Zach ). PS.

• On the Undecidability of Some Sub-classical First-Order Logics, Proceedings of Foundations of Software Technology and Theoretical Computer Science (FST&TCS'99) , Chennai, December 1999. LNCS 1738. pp. 258-268.
  (with M. Baaz , C.G. Fermüller and H. Veith ). PS.

Web Services

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

Recursion Theory and Partial Combinatory Algebras

• A Sufficient Condition for Completability of Partial Combinatory Algebras, Journal of Symbolic Logic , vol. 62. n. 4. pp. 1209-1214, 1997.
  (with A. Asperti )

• Effective Applicative Structures , Proceedings of the biennal conference Category Theory in Computer Science (CTCS'95) Cambridge (UK), August 1995. LNCS 953, pp. 81-95.
  (with A. Asperti ) PDF.

• On Completability of Partial Combinatory Algebras, Proceedings of the fifth Italian Conference on Theoretical Computer Science (ICTCS'95) , Ravello, Italy. November 1995. A. De Santis ed., World Scientific, pp. 162-175.
  (with A. Asperti )

Rule-Based Systems

• On the classical content of Goedel logic with strong negation and its application to a fuzzy medical expert system. Forthcoming in the Proceedings of Knowledge Representation and Reasoning KR2010 . IEEE.
  (with P. Rusnok ) PDF.

• On the (fuzzy) logical content of CADIAG-2. Fuzzy Sets and Systems. Accepted for publication. 2009.
  (with T. Vetterlein ) PDF.

• A formal logical framework for CADIAG-2. Proceedings of Medical Informatics Europe MIE 2009 . Sarajevo. Studies in Health Technology and Informatics series. IOS Press.
  (with T. Vetterlein and K-P. Adlassnig )

Non-deterministic Matrices

• Canonical Calculi: Invertibility, Axiom-Expansion and (Non)-determinism. Proceedings of the 4th Computer Science Symposium in Russia (CSR2009) Novosibirsk, Russia, 2009.
  (with A. Avron and A. Zamansky ) PDF.

Automated Generation of Analytic Calculi

• Algebraic proof theory for substructural logics: cut-elimination and completions. Submitted.
  (with N. Galatos and K. Terui ) Abstract

• Expanding the realm of systematic proof theory. Proceedings of 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'08) , IEEE pp. 229-240, 2008.
  (with N. Galatos and K. Terui ) PDF.

• Automated Generation of Analytic Calculi for Logics with Linearity. Proceedings of Computer Science Logic. (CSL04) . LNCS 3210 pp. 505-517. Karpacz, Poland. September 2004. PS and 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. pp. 157-180. 2003.
  (with M. Baaz and C.G. Fermüller ). PS.

T-norm based logics

• Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions. Fuzzy Sets and Systems. Accepted for publication 2009.
  (with G. Metcalfe and F. Montagna ) PDF.

• Density Elimination. Theoretical Computer Science 403(2-3), pp. 328--346. 2008.
  (with G. Metcalfe ) PDF.

• Analytic Calculi for Monoidal T-norm Based Logic. Fundamenta Informaticae . vol. 59, Number 4, pp. 315-332. 2004.
  (with M. Baaz and F. Montagna ). PDF.

• T-norm based logics with n-contraction. Neural Network World . vol. 12. n. 5. pp. 441-452. 2002.
  (with F. Esteva and L. Godo ) PS.

• Hypersequents as a uniform framework for Urquhart's C, MTL and related logics. Proceedings of the 31th IEEE International Symposium on Multiple-Valued Logic (ISMVL'2001) , Warsaw (Poland), May 2001. IEEE Computer Society Press. pp. 227-232.

• 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. pp. 157-180. 2003.
  (with M. Baaz and C.G. Fermüller ). PS.

Lukasiewicz Logic

• Finiteness of infinite-valued Lukasiewicz logic. Journal of Logic, Language and Information , vol. 9, pp. 5-29, 2000.
  (with S. Aguzzoli ). PS.

• Sequent calculi for finite-valued Lukasiewicz logics via boolean decompositions, Journal of Logic and Computation , vol. 10. n. 2. pp. 213-222, 2000.
  (with S. Aguzzoli and A. Di Nola )

• Uniform Rules and Dialogue Games for Fuzzy Logics. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2005), LNAI 3452. pp. 496-510. 2004.
  (with C. Fermüller and G. Metcalfe ) PS and PDF.

• Bounded Lukasiewicz Logics . Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods. (Tableaux 2003), Roma, Italy, September 2003. LNAI 2796. pp. 32-47. 2003.
  (with G. Metcalfe ) PS.

• Two connections between Linear Logic and Lukasiewicz Logic, Proceedings of the biennal conference Computational Logic and Proof Theory -- Kurt Gödel Colloquium (KGC'97), Vienna, August 1997. LNCS 1289, pp. 128-139.
  (with D. Luchi )

Goedel Logics

• SAT in Monadic Goedel Logics: a borderline between decidability and undecidability. Proceedings of WOLLIC 2009 . LNAI.
  (with M. Baaz and N. Preining ) PDF.

• Monadic Fragments of Gödel Logics: Decidability and Undecidability Results. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2007), LNAI 4790. pp. 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 . vol. 13. pp. 835 - 861. 2003.
  (with M. Baaz and C.G. Fermüller ). PDF.

• Cut elimination for first order Goedel logic by hyperclause resolution. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2008), LNCS 5330, pp. 451-466
  (with M. Baaz and C.G. Fermüller ) PDF.

• Uniform Rules and Dialogue Games for Fuzzy Logics. Proceedings of Logic for Programming and Automated Reasoning (LPAR'2005), LNAI 3452. pp. 496-510. 2004.
  (with C. Fermüller and G. Metcalfe ) PS and PDF.

• From Intuitionistic Logic to Gödel-Dummett Logic via Parallel Dialogue Games. Proceedings of the 33th IEEE International Symposium on Multiple-Valued Logic (ISMVL'2003) , Tokyo, (Japan), May 2003. pp. 188-193.
  (with C.G. Fermüller ) PDF.

• A Schütte-Tait style cut-elimination proof for first-order Gödel logic. Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods. (Tableaux 2002), Copenhagen, Denmark, August 2002. LNAI 2381. pp. 24-38.
  (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. pp. 201-216.
  (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. pp. 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. pp. 157-180. 2003.
  (with M. Baaz and C.G. Fermüller ). PS.

• A Natural Deduction System for Intuitionistic Fuzzy Logic, Lectures on Soft Computing and Fuzzy Logic , A. Di Nola, G. Gerla eds., Physica-Verlag. 2000, pp. 1-18.
  (with M. Baaz and C.G. Fermüller ) PS.