Camillo Fiorentini

61 papers A* 1A 2B 10C 3Journal 23Unranked 21
YearRankTypeTitle / Venue / Authors
2025 B conf
A Gödel Modal Logic over Witnessed Crisp Models.
TABLEAUX
Mauro Ferrari, Camillo Fiorentini, Ricardo Oscar Rodríguez
2025 — conf
Proof Search and Countermodel Construction for iCK4.
CILC
Mauro Ferrari, Camillo Fiorentini, Paolo Giardini
2024 — conf
A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property.
IJCAR (2)
Camillo Fiorentini, Mauro Ferrari
2024 J jnl
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic.
J. Autom. Reason.
Camillo Fiorentini, Mauro Ferrari
2023 — conf
A New Approach to Clausification for Intuitionistic Propositional Logic.
CILC
Camillo Fiorentini, Mauro Ferrari
2022 — conf
Forward refutation for Gödel-Dummett Logics.
CILC
Camillo Fiorentini, Mauro Ferrari
2022 A conf
SAT-Based Proof Search in Intermediate Propositional Logics.
IJCAR
Camillo Fiorentini, Mauro Ferrari
2021 J jnl
A forward internal calculus for model generation in S4.
J. Log. Comput.
Camillo Fiorentini, Mauro Ferrari
2021 A conf
Efficient SAT-based Proof Search in Intuitionistic Propositional Logic.
CADE
Camillo Fiorentini
2020 — conf
A Natural Deduction Calculus for Gödel-Dummett Logic Internalizing Proof-search Control Mechanisms.
CILC
Camillo Fiorentini, Mauro Ferrari
2020 — conf
Connections Between Answer Set Semantics and Information Terms Semantics in Constructive EL_bot (Extended Abstract).
Description Logics
Loris Bozzato, Camillo Fiorentini
2020 J jnl
Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic.
ACM Trans. Comput. Log.
Camillo Fiorentini, Mauro Ferrari
2020 — conf
Forward proof-search and Countermodel Construction in Intuitionistic Propositional Logic.
ICTCS
Camillo Fiorentini, Mauro Ferrari
2020 — conf
Reasoning on Information Term Semantics with ASP for Constructive ELꓕ.
CILC
Loris Bozzato, Camillo Fiorentini
2019 B conf
A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic.
TABLEAUX
Camillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand
2019 A* conf
An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic.
IJCAI
Camillo Fiorentini
2019 J jnl
Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic.
J. Autom. Reason.
Mauro Ferrari, Camillo Fiorentini
2018 J jnl
Duality between unprovability and provability in forward proof-search for Intuitionistic Propositional Logic.
CoRR
Camillo Fiorentini, Mauro Ferrari
2018 — conf
Forward Countermodel Construction in Modal Logic K.
CILC
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2018 J jnl
From Constructivism to Logic Programming: an Homage to Mario Ornaghi.
Fundam. Informaticae
Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano
2018 J jnl
Preface.
Fundam. Informaticae
Camillo Fiorentini, Alberto Momigliano, Alberto Pettorossi
2017 B conf
A Forward Unprovability Calculus for Intuitionistic Propositional Logic.
TABLEAUX
Camillo Fiorentini, Mauro Ferrari
2017 J jnl
JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi.
Fundam. Informaticae
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2017 — conf
LOGI: A Didactic Tool for a Beginners' Course in Logic (System Description).
ICTCS/CILC
Mario Ornaghi, Camillo Fiorentini, Alberto Momigliano
2017 — conf
Proof-Search in Hilbert Calculi.
ICTCS/CILC
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2016 — ed.
Proceedings of the 31st Italian Conference on Computational Logic, Milano, Italy, June 20-22, 2016.
CILC
Camillo Fiorentini, Alberto Momigliano
2015 J jnl
A Semantical Analysis of Focusing and Contraction in Intuitionistic Logic.
Fundam. Informaticae
Alessandro Avellone, Camillo Fiorentini, Alberto Momigliano
2015 J jnl
An Evaluation-Driven Decision Procedure for G3i.
ACM Trans. Comput. Log.
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2015 B conf
Proof-Search in Natural Deduction Calculus for Classical Propositional Logic.
TABLEAUX
Mauro Ferrari, Camillo Fiorentini
2015 J jnl
Terminating sequent calculi for proving and refuting formulas in S4.
J. Log. Comput.
Camillo Fiorentini
2015 — conf
Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations.
CILC
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2014 — conf
JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi.
CILC
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2013 B conf
A Terminating Evaluation-Driven Variant of G3i.
TABLEAUX
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2013 J jnl
Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models.
J. Autom. Reason.
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2013 — conf
Focusing on Contraction.
CILC
Alessandro Avellone, Camillo Fiorentini, Alberto Momigliano
2012 J jnl
Simplification Rules for Intuitionistic Propositional Tableaux.
ACM Trans. Comput. Log.
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2010 — conf
A Constructive Approach to Testing Model Transformations.
ICMT@TOOLS
Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi, Iman Poernomo
2010 B conf
A Decidable Constructive Description Logic.
JELIA
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2010 — conf
fCube: An Efficient Prover for Intuitionistic Propositional Logic.
LPAR (Yogyakarta)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2009 J jnl
A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications.
J. Appl. Non Class. Logics
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2009 B conf
Applying ASP to UML Model Validation.
LPNMR
Mario Ornaghi, Camillo Fiorentini, Alberto Momigliano, Francesco Pagano
2008 — conf
Towards a Type Discipline for Answer Set Programming.
TYPES
Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi
2007 — conf
A Constructive Semantics for ALC.
Description Logics
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2007 C conf
Snapshot Generation in a Constructive Object-Oriented Modeling Language.
LOPSTR
Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi
2005 — conf
A Constructive Object Oriented Modeling Language for Information Systems.
CLASE
Mario Ornaghi, Marco Benini, Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano
2005 — conf
ESBC: an application for computing stabilization bounds.
CLASE
Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino, Ugo Moscato
2005 J jnl
On the complexity of the disjunction property in intuitionistic and modal logics.
ACM Trans. Comput. Log.
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2004 B conf
A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation.
CSL
Alessandro Avellone, Camillo Fiorentini, Guido Fiorino, Ugo Moscato
2004 J jnl
A secondary semantics for Second Order Intuitionistic Propositional Logic.
Math. Log. Q.
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2003 J jnl
A Proof-theoretical Analysis of Semiconstructive Intermediate Theories.
Stud Logica
Mauro Ferrari, Camillo Fiorentini
2003 J jnl
Combining word problems through rewriting in categories with products.
Theor. Comput. Sci.
Camillo Fiorentini, Silvio Ghilardi
2002 B conf
On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics.
LPAR
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2002 B conf
Tableau Calculi for the Logics of Finite k-Ary Trees.
TABLEAUX
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2001 C conf
Extracting Exact Time Bounds from Logical Proofs.
LOPSTR
Mauro Ferrari, Camillo Fiorentini, Mario Ornaghi
2001 J jnl
Extracting information from intermediate semiconstructive HA-systems - extended abstract.
Math. Struct. Comput. Sci.
Mauro Ferrari, Camillo Fiorentini, Pierangelo Miglioli
2001 J jnl
Hypercanonicity, Extensive Canonicity, Canonicity and Strong Completeness of Intermediate Propositional Logics.
Reports Math. Log.
Camillo Fiorentini
2000 — conf
A Formal Framework for Synthesis and Verification of Logic Programs.
LOPSTR (LNCS 2042: Selected Papers)
Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini
2000 C conf
A formal framework for synthesis and verification of logic programs.
LOPSTR
Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini
2000 J jnl
All Intermediate Logics with Extra Axions in One Variable, Except Eight, Are Not Strongly omega-Complete.
J. Symb. Log.
Camillo Fiorentini
1999 J jnl
A Cut-free Sequent Calculus for the Logic of Constant Domains with a Limited Amount of Duplications.
Log. J. IGPL
Camillo Fiorentini, Pierangelo Miglioli
1996 J jnl
On maximal intermediate predicate constructive logics.
Stud Logica
Alessandro Avellone, Camillo Fiorentini, Paolo Mantovani, Pierangelo Miglioli