Camillo Fiorentini

Publications

Home page

Journal papers

  1. M. Ferrari and C. Fiorentini. Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic. Journal of Automated Reasoning, vol. 62(1), pp. 127-67, 2019.
  2. M. Ferrari, C. Fiorentini, and G. Fiorino. JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi. Fundamenta Informaticae, vol. 150(1), pp. 119-142, 2017.
  3. A. Avellone, C. Fiorentini, A. Momigliano. A Semantical Analysis of Focusing and Contraction in Intuitionistic Logic. Fundamenta Informaticae, vol. 140(3-4), pp. 247-262, 2015.
  4. M. Ferrari, C. Fiorentini, G. Fiorino. An Evaluation-Driven Decision Procedure for G3i. ACM Transactions on Computational Logic (TOCL), vol. 16(1), pp. 8:1-8:37, 2015.
  5. C. Fiorentini. Terminating sequent calculi for proving and refuting formulas in S4. Journal of Logic and Computation, vol 25(1), pp. 179-205, 2015.
  6. M. Ferrari, C. Fiorentini, 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, vol. 51(2), pp. 129-149, 2013.
  7. M. Ferrari, C. Fiorentini, G.Fiorino. Simplification Rules for Intuitionistic Propositional Tableaux. ACM Transactions on Computational Logic (TOCL), vol. 13(2), pp. 14:1-14:23, 2012.
  8. M. Ferrari, C. Fiorentini, G. Fiorino. BCDL: Basic Constructive Description Logic. Journal of Automated Reasoning, vol. 44(4), pp. 503-524, 2010.
  9. M. Ferrari, C. Fiorentini, G. Fiorino. A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of implication. Journal of Applied Non-classical Logics, vol. 19(2), pp. 149-166, 2009.
  10. M. Ferrari, C. Fiorentini, G. Fiorino. On the complexity of the disjunction property in intuitionistic and modal logics. ACM Transactions on Computational Logic (TOCL), vol. 6(3), pp. 519-538, 2005.
  11. M. Ferrari, C. Fiorentini, G. Fiorino. A secondary semantics for second order intuitionistic propositional logic. Mathematical Logic Quarterly, vol. 50(2), pp. 202-210, 2004.
  12. M. Ferrari, C. Fiorentini. A proof-theoretical analysis of semiconstructive intermediate theories. Studia Logica, vol. 73(1), pp. 21-49, 2003.
  13. C. Fiorentini, S. Ghilardi. Combining word problems through rewriting in categories with products. Theoretical Computer Science, vol., pp. 294:103-149, 2003.
  14. C. Fiorentini. Hypercanonicity, extensive canonicity, canonicity and strong completeness of intermediate propositional logics. Reports on Mathematical Logic, vol. 35, pp. 3-46, 2001.
  15. C. Fiorentini. All intermediate logics with extra axioms in one variable, except eight, are not strongly ω-complete. The Journal of Symbolic Logic, vol. 65, pp. 1575-1604, 2000.
  16. C. Fiorentini, P. Miglioli. A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications. Logic Journal of the IGPL, vol. 7(6), pp. 733-753, 1999.
  17. A. Avellone, C. Fiorentini, P. Mantovani, P. Miglioli. On maximal intermediate predicate constructive logics. Studia Logica, vol. 57, pp. 373 - 408, 1996.

Conference/Workshop papers

  1. C. Fiorentini, R. Gorè and S. Graham-Lengrand. A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic. TABLEAUX 2019, to appear.
  2. C. Fiorentini. An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic. IJCAI 2019, to appear.
  3. C. Fiorentini and M. Ferrari. A Forward Unprovability Calculus for Intuitionistic Propositional Logic. TABLEAUX 2017, LNAI, vol. 10501, pp. 114-130, Springer, 2017. Appendix (pdf). Slides (pdf)
  4. M. Ferrari and C. Fiorentini. Proof-search in Natural Deduction calculus for classical propositional logic. TABLEAUX 2015, LNCS, vol. 9323, pp. 237-252, Springer-Verlag, 2015. Slides (pdf)
  5. M. Ferrari, C. Fiorentini, and G. Fiorino. A terminating evaluation-driven variant of G3i. In TABLEAUX 2013, LNCS, vol. 8123, pp. 104-118. Springer-Verlag, 2013. Slides (pdf)
  6. M. Ferrari, C. Fiorentini, G. Fiorino. fCube: An Efficient Prover for Intuitionistic Propositional Logic. System Description, In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, 2010. Proceedings, LNCS, vol. 6397/2010, pp. 294-301, 2010.
  7. L. Bozzato, M. Ferrari, C. Fiorentini, G. Fiorino. A Decidable Constructive Description Logic. In Logics in Artificial Intelligence - 12th European Conference, JELIA 2010. Proceedings, LNCS, vol. 6341/2010, pp. 51-63, 2010.
  8. C. Fiorentini, A. Momigliano, M. Ornaghi, I. Poernomo. A constructive approach to testing model transformations. In Theory and Practice of Model Transformations. Third International Conference, ICMT 2010. Proceedings, LNCS, vol. 6142/2010, pp. 77-92,2010.
  9. M. Ornaghi, C. Fiorentini, A. Momigliano, F. Pagano. Applying ASP to UML Model Validation. In Logic Programming and Nonmonotonic Reasoning, LPNMR 2009, LNCS, vol. 5753, pp. 457-463, 2009.
  10. C. Fiorentini, A. Momigliano, M. Ornaghi. Towards a Type Discipline for Answer Set Programming. In Types for Proofs and Programs, International Conference, TYPES 2008. Revised Selected Papers, LNCS, vol. 5497, pp. 117-135, 2009
  11. M. Ferrari, C. Fiorentini, A. Momigliano, M. Ornaghi. Snapshot Generation in a Constructive Object-oriented Modeling Language. In Logic Based Program Synthesis and Transformation, LOPSTR'07. Revised Selected Papers, LNCS, vol. 4914, pp. 169-184, 2008.
  12. C. Fiorentini, M. Ornaghi. Model Validation through CooML Snapshot Generation. In Tests and Proofs: Papers Presented at the Second International Conference TAP 2008, Prato, Italy, April 2008, Reports of the Faculty of Informatics, University of Koblenz-Landau, N. 5/2008, pp 17-32, 2008.
  13. C. Fiorentini, M. Ornaghi. Answer Set Semantics vs. Information Term Semantics. In Proceedings of the 4th Workshop on Answer Set Programming: Advances in Theory and Implementation, S. Costantini, R. Watson Eds., pp 241-254, 2007.
  14. L. Bozzato, M. Ferrari, C. Fiorentini, G. Fiorino. A Constructive Semantics for ALC. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), Brixen-Bressanone, near Bozen-Bolzano, Italy, 8-10 June, 2007, CEUR Workshop Proceedings, vol. 250, pp. 219-226.
  15. M. Ornaghi, M. Benini, M. Ferrari, C. Fiorentini, A. Momigliano. A Constructive Object Oriented Modeling Language for Information Systems. In Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005), ENTCS, 153(1): 55-75, 2006.
  16. A. Avellone, M. Ferrari, C. Fiorentini, G. Fiorino, U. Moscato. ESBC: an application for computing stabilization bounds. In Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005), ENTCS, 153(1): 23-33, 2006.
  17. A. Avellone, C. Fiorentini, G. Fiorino, U. Moscato. A space efficient implementation of a tableau calculus for a logic with a constructive negation. Computer Science Logic. 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, LNCS, vol.3210. pp. 488-502, 2004.
  18. M. Ferrari, C. Fiorentini, M. Ornaghi. Extracting exact time bounds from logical proofs. In Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Selected Papers, LNCS, vol. 2372 pp. 245-265, 2002.
  19. M. Ferrari, C. Fiorentini, G. Fiorino. Tableau calculi for the logics of finite k-ary trees. In TABLEAUX 2002, Automated Reasoning with Analytic Tableaux and Related Methods, LNAI, vol. 2381, pp. 115-129, 2002.
  20. M. Ferrari, C. Fiorentini, 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, LNAI, vol. 2514, pp. 175-189, 2002.
  21. A. Avellone, M. Ferrari, C. Fiorentini. A formal framework for synthesis and verification of logic programs. In Logic Based Program Synthesis and Transformation. 10th International Workshop, LOPSTR 2000, London, UK, July 24-28, 2000. Selected Papers. LNCS, vol. 1559, pp. 1-17, 2001.
  22. M. Ferrari, C. Fiorentini, P. Miglioli. Goal oriented information extraction in uniformly constructive calculi. In Proceedings of WAIT'99: Workshop Argentino de Informàtica Teòrica, pp. 51-63, 1999.

Technical Reports, Presentations, Abstracts

  1. M. Ferrari, C. Fiorentini. Evaluation Driven Proof-Search in Natural Deduction Calculi for Intuitionistic Propositional Logic. SYSMICS 2016. Slides (pdf)
  2. M. Ferrari, C. Fiorentini, P. Miglioli. Extracting information from intermediate semiconstructive HA-systems (extended abstract). Mathematical Structures in Computer Science, 11, 2001.
  3. C. Fiorentini, S. Ghilardi. Path rewriting and combined word problems. Technical Report 250-00, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 2000. pdf