| |
Representative
publications |
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.
M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di
programmazione Java (seconda edizione). Pearson Education Italia,
2005.
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,
to appear.
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, to appear.
M. Ferrari, C. Fiorentini, and G. Fiorino. A secondary semantics for
second order intuitionistic propositional logic. Mathematical Logic Quarterly,
50(2):202-210, 2004.
M. Ferrari and C.Fiorentini. A proof-theoretical analysis of semiconstructive
intermediate theories. Studia Logica, 73(1):21-49, 2003.
M. Ferrari, P. Miglioli, and M. Ornaghi. On uniformly constructive
and semiconstructive formal systems. Logic Journal of the IGPL, 11(1):1-49,
2003.
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.
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.
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.
M. Ferrari, C. Fiorentini, and M. Ornaghi. Extracting exact time bounds
from logical proofs. In A. Pettorossi, editor, Pre-Proceedings of
LOPSTR'01: Logic-Based Program Synthesis and Transformation, pages
132-140, 2001.
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.
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.
M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information
from intermediate semiconstructive HA-systems (extended abstract).
Mathematical Structures in Computer Science, 11:589-696, 2001.
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.
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.
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.
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.
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.
A. Avellone, M. Ferrari, and P. Miglioli. Synthesis of programs in
abstract data types (extended abstract). In Pre-Proceedings of LOPSTR'98.
Depart. of Computer Science, University of Manchester, UMCS-98-6-1,
1998.
A. Avellone, M. Ferrari, P. Miglioli, and U. Moscato. A tableau calculus
and a cut-free sequent calculus for Dummett predicate logic. In H.C.M.
de Swart, editor, Position Papers, pages 1-18. International Conference
TABLEAUX'98, Analytic Tableaux and Related Methods, Katholieke Universiteit
Brabant, 1998.
M. Ferrari. Cut-free tableau calculi for some intuitionistic modal
logics. Studia Logica, 59(3):303-330, 1997.
M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento
di Scienze dell'Informazione, Università degli Studi di Milano,
Italy, 1997.
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.
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.
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.
M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive
logics. Journal of Symbolic Logic, 58(4):1365-1401, 1993.
|
