Publications¶
[1]  M. Ferrari, C. Fiorentini. Goaloriented proofsearch in natural deduction for Intuitionistic Propositional Logic. Journal of Automated Reasoning, to appear.

[2]  M. Ferrari and C. Fiorentini. A Forward Unprovability Calculus for Intuitionistic Propositional Logic. TABLEAUX 2017, to appear.

[3]  M. Ferrari, C. Fiorentini, and G. Fiorino. Proofsearch in Hilbert calculi. CILC 2017 Italian Conference on Computational Logic, to appear. 
[4]  M. Ferrari, C. Fiorentini and G. Fiorino. JTabWb: a Java framework for implementing terminating sequent and tableau calculi. Fundamenta Informaticae, 150(1):119142, 2017.

[5]  M. Ferrari and C. Fiorentini. Proofsearch in natural deduction calculus for classical propositional logic. In H. De Nivelle, editor, TABLEAUX 2015, LNCS, vol. 9323, pages 237–252. Springer International Publishing, 2015

[6]  M. Ferrari, C. Fiorentini, and G. Fiorino. An EvaluationDriven Decision Procedure for G3i. ACM Transactions on Computational Logic (TOCL), 6(1):8:1–8:37, 2015.

[7]  M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Quarta edizione. Pearson Italia, 2015. 
[8]  M. Ferrari, C. Fiorentini, and G. Fiorino. A new refutation calculus with logical optimizations for PLTL. In IARIA, editor, COMPUTATION TOOLS 2015, pages 39–41, 2015. 
[9]  M. Ferrari, C. Fiorentini, and G. Fiorino. JTabWb: a Java framework for implementing terminating sequent and tableau calculi. In L. Giordano, V. Gliozzi and G.L. Pozzato, editors, CILC 2014 Italian Conference on Computational Logic, volume 1195 of CEUR Proceedings, ISBN/ISSN: 16130073, pages 46530, 2014.

[10]  M. Ferrari, C. Fiorentini, and G. Fiorino. A terminating evaluationdriven variant of G3i. In D. Galmiche and D. LarcheyWendling, editors, TABLEAUX 2013, LNCS, volume 8123, pages 104118. SpringerVerlag, 2013.

[11]  M. Ferrari, C. Fiorentini, and G. Fiorino. Contractionfree Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth CounterModels. Journal of Automated Reasoning, 51(2):129149, 2013.

[12]  M. Ferrari, C. Fiorentini, and G. Fiorino. Simplification Rules for Intuitionistic Propositional Tableaux. ACM Transactions on Computational Logic (TOCL), 13(2), 2012.

[13]  M. Ferrari, C. Fiorentini, and G. Fiorino. BCDL: Basic Constructive Description Logic. Journal of Automated Reasoning, 44(4):371399, 2010.

[14]  M. Ferrari, C. Fiorentini, and G. Fiorino. FCube: An Efficient Prover for Intuitionistic Propositional Logic. In C. G. Fermuller and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR17, volume 6397, pages 294301. Springer, 2010.

[15]  L.Bozzato, M. Ferrari, C. Fiorentini, and G. Fiorino. A decidable constructive description logic. In T. Janhunen and I. Niemela, editors, Logics in Artificial Intelligence, JELIA 2010, volume 6341, pages 5163. Springer, 2010.

[16]  L.Bozzato and M. Ferrari. A Note on Semantic Web Services Specification and Composition in Constructive Description Logics. arXiv:1007.2364, CoRR, pages 15, 2010.

[17]  L.Bozzato and M. Ferrari. Composition of Semantic Web Services in a Constructive Description Logic, In P. Hitzler and T. Lukasiewicz, editors, Web Reasoning and Rule Systems, RR 2010, volume 6333 of Lecture Notes in Computer Science, pages 223226. Springer, 2010.

[18]  L. Bozzato, M. Ferrari and P. Villa. Actions over a constructive semantics for description logics. Fundamenta Informaticae, 96, 117, 2009.

[19]  M. Ferrari, C. Fiorentini, and G. Fiorino. A Tableau Calculus for Propositional Intuitionistic Logic with a Refined Treatment of Nested Implications. Journal of Applied NonClassical Logics, 19(2):144166, 2009.

[20]  M. Ferrari, C. Fiorentini, and G. Fiorino. Towards the use of Simplification Rules in Intuitionistic Tableaux. Proceedings of CILC09, 24esimo Convegno Italiano di Logica Computazionale. 2009.

[21]  L. Bozzato, M. Ferrari and P. Villa. A note on constructive semantics for description logics. Proceedings of CILC09, 24esimo Convegno Italiano di Logica Computazionale. 2009.

[22]  M. Ferrari, C. Fiorentini, A. Momilgiano and M. Ornaghi. Snapshot generation in a constructive objectoriented modeling language. In A. King, editor Logic Based Program Synthesis and Transformation, LOPSTR 2007, Selected Papers, volume 4915 of Lecture Notes in Computer Science, pages 169184. SpringerVerlag, 2008.

[23]  L. Bozzato, M. Ferrari, and A. Trombetta. Building a domain ontology from glossaries: a general methodology. In A. Gangemi and J. Keizer and V. Presutti and H. Stoermer, editors Proceedins of 2008 Semantic Web Applications and Perspectives, SWAP 2008, volume 426 of CEUR Proceedings, ISBN/ISSN: 16130073, pages 110, 2008.

[24]  L. Bozzato, M. Ferrari and P. Villa. Actions over a constructive semantics for ALC. In F. Baader and C. Lutz and B. Motik, editors Proceedins of 2008 International Workshop on Description Logics, volume 353 of CEUR Proceedings, ISBN/ISSN: 16130073, 2008.

[25]  M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Terza edizione. Pearson AddisonWesley, 2008. 
[26]  L. Bozzato, M. Ferrari, C. Fiorentini and G. Fiorino. A constructive semantics for ALC. In D. Calvanese and E. Franconi and V. Haarslev and D. Lembo and B. Motik and A.Y. Turhan and S. Tessaris, editors Proceedins of 2007 International Workshop on Description Logics, volume 250 of CEUR Proceedings, ISBN/ISSN: 16130073, pages 219226, 2007.

[27]  M. Ornaghi, M.Benini, M. Ferrari, C. Fiorentini, and A. Momigliano. A Constructive Modeling Language for Object Oriented Information Systems. Proceedings of Constructive Logic for Automated Software Engineering, volume 153(1):5575 of Electronic Notes in Theoretical Computer Science, 2006.

[28]  A.Avellone, M. Ferrari, C. Fiorentini, G.Fiorino and U.Moscato. ESBC: an application for computing stabilization bounds. Proceedings of Constructive Logic for Automated Software Engineering, volume 153(1):2333 of Electronic Notes in Theoretical Computer Science, 2006.

[29]  M. Ferrari, C. Fiorentini, and G. Fiorino. On the complexity of the disjunction property in intuitionistic and modal logics. ACM, TOCL, 6(3):519538, 2005.

[30]  M. Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Seconda edizione. Pearson Education Italia, 2005. 
[31]  M. Ferrari, C. Fiorentini, and G. Fiorino. A secondary semantics for second order intuitionistic propositional logic. Mathematical Logic Quarterly, 50(2):202210, 2004.

[32]  M. Ferrari and C.Fiorentini. A prooftheoretical analysis of semiconstructive intermediate theories. Studia Logica, 73(1):2149, 2003.

[33]  M. Ferrari, P. Miglioli, and M. Ornaghi. On uniformly constructive and semiconstructive formal systems. Logic Journal of the IGPL, 11(1):149, 2003.

[34]  M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Pearson Education Italia, ISBN 88 7192 205 0, 2003. 
[35]  M. Ferrari, C. Fiorentini, and G.Fiorino. On the complexity of disjunction and explicit definability properties in some intermediate logics. In LPAR 2002: Logic for Programming Artificial Intelligence and Reasoning, number 2514 in Lecture Notes in Artificial Intelligence, pages 175189. SpringerVerlag, 2002.

[36]  M. Ferrari, C. Fiorentini, and M. Ornaghi. Extracting exact time bounds from logical proofs. In A. Petterossi, editor, Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Selected Papers, volume 2372 of Lecture Notes in Computer Science, pages 245265. SpringerVerlag, 2002.

[37]  M. Ferrari, C. Fiorentini, and G. Fiorino. Tableau calculi for the logics of finite kary trees. In TABLEAUX 2002, Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of Lecture Notes in Artificial Intelligence, pages 115129. SpringerVerlag, 2002.

[38]  A. Ciabattoni and M. Ferrari. Hypersequent calculi for some intermediate logics with bounded Kripke models. Journal of Logic and Computation, 11(2):283294, 2001.

[39]  A. Avellone, M. Ferrari, and C. Fiorentini. A formal framework for synthesis and verification of logic programs. In K. K. Lau, editor, Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000, Selected Papers, volume 2042 of Lecture Notes in Computer Science, pages 117. SpringerVerlag, 2001.

[40]  M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate semiconstructive HAsystems. Mathematical Structures in Computer Science, 11:589696, 2001.

[41]  A. Ciabattoni and M. Ferrari. Hypertableau and pathhypertableau calculi for some families of intermediate logics. In R. Dyckhoff, editor, TABLEAUX 2000, Automated Reasoning with Analytic Tableaux and Related Methods, volume 1947 of LNAI, pages 160174. SpringerVerlag, 2000.

[42]  M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate Tsystems. Technical Report 25200, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.

[43]  M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate semiconstructive HAsystems. Technical Report 25300, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.

[44]  M. Ferrari, C. Fiorentini, and P. Miglioli. Goal oriented information extraction in uniformly constructive calculi. In Argentinian Workshop on Theoretical Computer Science (WAIT 99), pages 5163. Sociedad Argentina de Informàtica e Investigaciòn Operativa, 1999.

[45]  A. Avellone, M. Ferrari, and P. Miglioli. Duplicationfree tableau calculi and related cutfree sequent calculi for the interpolable propositional intermediate logics. Logic Journal of the IGPL, 7(4):447480, 1999.

[46]  A. Avellone, M. Ferrari, and P. Miglioli. Synthesis of programs in abstract data types. In 8th International Workshop on Logicbased Program Synthesis and Transformation, volume 1559 of Lecture Notes in Computer Science, pages 81100. SpringerVerlag, 1999.

[47]  A. Avellone, M. Ferrari, P. Miglioli, and U. Moscato. A tableau calculus for Dummett predicate logic. In Walter A. Carnielli and Itala M. D’Ottaviano, editors, Advances in Contemporary Logic and Computer Science, volume 235 of Contemporary Mathematics, pages 135151. American Mathematical Society, 1999.

[48]  M. Ferrari. Cutfree tableau calculi for some intuitionistic modal logics. Studia Logica, 59(3):303330, 1997.

[49]  M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1997.

[50]  A. Avellone, M. Ferrari and P. Miglioli. Duplicationfree tableau calculi together with cutfree and contractionfree sequent calculi for the interpolable propositional intermediate logics, Technical Report 21097, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.

[51]  A. Avellone and M. Ferrari. Almost duplicationfree tableaux calculi for propositional Lax logics. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings of the 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of LNAI, pages 4864. SpringerVerlag, 1996.

[52]  M. Ferrari and P. Miglioli. A method to single out maximal propositional logics with the disjunction property II. Annals of Pure and Applied Logic, 76:117168, 1995.

[53]  M. Ferrari and P. Miglioli. A method to single out maximal propositional logics with the disjunction property I. Annals of Pure and Applied Logic, 76:146, 1995.

[54]  M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. Journal of Symbolic Logic, 58(4):13651401, 1993.

[55]  M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. AILA Preprint n. 11  gennaio/giugno, 1992. 
[56]  M. Ferrari. Logiche intermedie costruttive massimali. Master’s thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1990. 