Publications¶
[1] | M. Ferrari, C. Fiorentini. Goal-oriented proof-search in natural deduction for Intuitionistic Propositional Logic. Journal of Automated Reasoning, 62(1):127-165, 2019.
|
[2] | M. Ferrari and C. Fiorentini and G. Fiorino. A Sequent Based On-the-fly Procedure to Get Hilbert Proofs in Classical Propositional Logic. In IARIA, editor, COMPUTATION TOOLS 2019, pages 10–15, 2019. |
[3] | C. Fiorentini and M. Ferrari. A Forward Unprovability Calculus for Intuitionistic Propositional Logic. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017, LNCS, vol. 10501, pages 114–130. Springer International Publishing, 2017.
|
[4] | M. Ferrari, C. Fiorentini, and G. Fiorino. Proof-search in Hilbert calculi. In D. Della Monica and A. Murano and S. Rubin and L. Sauro, editors, CILC 2017 Italian Conference on Computational Logic, volume 1949 of CEUR Proceedings, ISBN/ISSN: 1613-0073, pages 301-305, 2017. |
[5] | M. Ferrari, C. Fiorentini and G. Fiorino. JTabWb: a Java framework for implementing terminating sequent and tableau calculi. Fundamenta Informaticae, 150(1):119-142, 2017.
|
[6] | M. Ferrari and C. Fiorentini. Proof-search 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
|
[7] | M. Ferrari, C. Fiorentini, and G. Fiorino. An Evaluation-Driven Decision Procedure for G3i. ACM Transactions on Computational Logic (TOCL), 6(1):8:1–8:37, 2015.
|
[8] | M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Quarta edizione. Pearson Italia, 2015. |
[9] | 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. |
[10] | 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: 1613-0073, pages 46-530, 2014.
|
[11] | M. Ferrari, C. Fiorentini, and G. Fiorino. A terminating evaluation-driven variant of G3i. In D. Galmiche and D. Larchey-Wendling, editors, TABLEAUX 2013, LNCS, volume 8123, pages 104-118. Springer-Verlag, 2013.
|
[12] | M. Ferrari, C. Fiorentini, and G. Fiorino. Contraction-free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models. Journal of Automated Reasoning, 51(2):129-149, 2013.
|
[13] | M. Ferrari, C. Fiorentini, and G. Fiorino. Simplification Rules for Intuitionistic Propositional Tableaux. ACM Transactions on Computational Logic (TOCL), 13(2), 2012.
|
[14] | M. Ferrari, C. Fiorentini, and G. Fiorino. BCDL: Basic Constructive Description Logic. Journal of Automated Reasoning, 44(4):371-399, 2010.
|
[15] | 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, LPAR-17, volume 6397, pages 294-301. Springer, 2010.
|
[16] | 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 51-63. Springer, 2010.
|
[17] | 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.
|
[18] | 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 223-226. Springer, 2010.
|
[19] | L. Bozzato, M. Ferrari and P. Villa. Actions over a constructive semantics for description logics. Fundamenta Informaticae, 96, 1-17, 2009.
|
[20] | M. Ferrari, C. Fiorentini, and G. Fiorino. A Tableau Calculus for Propositional Intuitionistic Logic with a Refined Treatment of Nested Implications. Journal of Applied Non-Classical Logics, 19(2):144-166, 2009.
|
[21] | M. Ferrari, C. Fiorentini, and G. Fiorino. Towards the use of Simplification Rules in Intuitionistic Tableaux. Proceedings of CILC09, 24-esimo Convegno Italiano di Logica Computazionale. 2009.
|
[22] | L. Bozzato, M. Ferrari and P. Villa. A note on constructive semantics for description logics. Proceedings of CILC09, 24-esimo Convegno Italiano di Logica Computazionale. 2009.
|
[23] | M. Ferrari, C. Fiorentini, A. Momilgiano and M. Ornaghi. Snapshot generation in a constructive object-oriented 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 169-184. Springer-Verlag, 2008.
|
[24] | 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: 1613-0073, pages 1-10, 2008.
|
[25] | 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: 1613-0073, 2008.
|
[26] | M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Terza edizione. Pearson Addison-Wesley, 2008. |
[27] | 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: 1613-0073, pages 219-226, 2007.
|
[28] | 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):55-75 of Electronic Notes in Theoretical Computer Science, 2006.
|
[29] | 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):23-33 of Electronic Notes in Theoretical Computer Science, 2006.
|
[30] | M. Ferrari, C. Fiorentini, and G. Fiorino. On the complexity of the disjunction property in intuitionistic and modal logics. ACM, TOCL, 6(3):519-538, 2005.
|
[31] | M. Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Seconda edizione. Pearson Education Italia, 2005. |
[32] | M. Ferrari, C. Fiorentini, and G. Fiorino. A secondary semantics for second order intuitionistic propositional logic. Mathematical Logic Quarterly, 50(2):202-210, 2004.
|
[33] | M. Ferrari and C.Fiorentini. A proof-theoretical analysis of semiconstructive intermediate theories. Studia Logica, 73(1):21-49, 2003.
|
[34] | M. Ferrari, P. Miglioli, and M. Ornaghi. On uniformly constructive and semiconstructive formal systems. Logic Journal of the IGPL, 11(1):1-49, 2003.
|
[35] | M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Pearson Education Italia, ISBN 88 7192 205 0, 2003. |
[36] | 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 175-189. Springer-Verlag, 2002.
|
[37] | 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 245-265. Springer-Verlag, 2002.
|
[38] | M. Ferrari, C. Fiorentini, and G. Fiorino. Tableau calculi for the logics of finite k-ary trees. In TABLEAUX 2002, Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of Lecture Notes in Artificial Intelligence, pages 115-129. Springer-Verlag, 2002.
|
[39] | A. Ciabattoni and M. Ferrari. Hypersequent calculi for some intermediate logics with bounded Kripke models. Journal of Logic and Computation, 11(2):283-294, 2001.
|
[40] | 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 1-17. Springer-Verlag, 2001.
|
[41] | M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate semiconstructive HA-systems. Mathematical Structures in Computer Science, 11:589-696, 2001.
|
[42] | A. Ciabattoni and M. Ferrari. Hypertableau and path-hypertableau 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 160-174. Springer-Verlag, 2000.
|
[43] | M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate T-systems. Technical Report 252-00, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.
|
[44] | M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate semiconstructive HA-systems. Technical Report 253-00, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.
|
[45] | 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 51-63. Sociedad Argentina de Informàtica e Investigaciòn Operativa, 1999.
|
[46] | A. Avellone, M. Ferrari, and P. Miglioli. Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics. Logic Journal of the IGPL, 7(4):447-480, 1999.
|
[47] | A. Avellone, M. Ferrari, and P. Miglioli. Synthesis of programs in abstract data types. In 8th International Workshop on Logic-based Program Synthesis and Transformation, volume 1559 of Lecture Notes in Computer Science, pages 81-100. Springer-Verlag, 1999.
|
[48] | 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 135-151. American Mathematical Society, 1999.
|
[49] | M. Ferrari. Cut-free tableau calculi for some intuitionistic modal logics. Studia Logica, 59(3):303-330, 1997.
|
[50] | M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1997.
|
[51] | A. Avellone, M. Ferrari and P. Miglioli. Duplication-free tableau calculi together with cut-free and contraction-free sequent calculi for the interpolable propositional intermediate logics, Technical Report 210-97, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.
|
[52] | A. Avellone and M. Ferrari. Almost duplication-free 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 48-64. Springer-Verlag, 1996.
|
[53] | 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:117-168, 1995.
|
[54] | 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:1-46, 1995.
|
[55] | M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. Journal of Symbolic Logic, 58(4):1365-1401, 1993.
|
[56] | M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. AILA Preprint n. 11 - gennaio/giugno, 1992. |
[57] | M. Ferrari. Logiche intermedie costruttive massimali. Master’s thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1990. |