Camillo Fiorentini

Publications

Home page

Journal papers

  1. C. Fiorentini and M. Ferrari. General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic. Journal of Automated Reasoning, vol. 68(3):13, 2024. See the github page intuitRGC.
  2. C. Fiorentini and M. Ferrari. A forward internal calculus for model generation in S4. Journal of Logic and Computation, 2021.
  3. C. Fiorentini and M. Ferrari. Duality between unprovability and provability in forward refutation-search for Intuitionistic Propositional Logic. ACM Transactions on Computational Logic (TOCL), vol. 21(3), pp. 22:1-44, 2020. See the github page jtabwb_provers (prover ipl_frj).
  4. 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. See the github page jtabwb_provers (prover ipl_nbu).
  5. 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.
  6. 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.
  7. 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-7, 2015.
  8. C. Fiorentini. Terminating sequent calculi for proving and refuting formulas in S4. Journal of Logic and Computation, vol 25(1), pp. 179-205, 2015.
  9. 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.
  10. 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.
  11. M. Ferrari, C. Fiorentini, G. Fiorino. BCDL: Basic Constructive Description Logic. Journal of Automated Reasoning, vol. 44(4), pp. 503-524, 2010.
  12. 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.
  13. 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.
  14. 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.
  15. M. Ferrari, C. Fiorentini. A proof-theoretical analysis of semiconstructive intermediate theories. Studia Logica, vol. 73(1), pp. 21-49, 2003.
  16. C. Fiorentini, S. Ghilardi. Combining word problems through rewriting in categories with products. Theoretical Computer Science, vol., pp. 294:103-149, 2003.
  17. C. Fiorentini. Hypercanonicity, extensive canonicity, canonicity and strong completeness of intermediate propositional logics. Reports on Mathematical Logic, vol. 35, pp. 3-46, 2001.
  18. 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.
  19. 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.
  20. 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 and M. Ferrari. A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property. IJCAR 2024, vol.14740 of LNAI, pp. 24–42, 2022. See the github page isl_gbuS.
  2. C. Fiorentini and M. Ferrari. SAT-based Proof Search in Intermediate Propositional Logics. IJCAR 2022, vol.13385 of LNAI, pp. 57–74, 2022. See the github page intuitRIL.
  3. C. Fiorentini. Efficient SAT-based Proof Search in Intuitionistic Propositional Logic. CADE 2021,LNAI, vol.12699, pp. 217-133, Springer, 2021. See the github page intuitR.
  4. C. Fiorentini, R. Gorè and S. Graham-Lengrand. A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic. TABLEAUX 2019,LNCS, vol.11714, pp. 111-129, Springer, 2019.
  5. C. Fiorentini. An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic. IJCAI 2019, pp. 1675-1681, 2019. Slides (pdf)
  6. 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)
  7. 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)
  8. 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)
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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