Mauro Ferrari

55 papers A 1B 9C 4Journal 23Unranked 18
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
2020 — conf
A Natural Deduction Calculus for Gödel-Dummett Logic Internalizing Proof-search Control Mechanisms.
CILC
Camillo Fiorentini, Mauro Ferrari
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
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
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
Proof-Search in Hilbert Calculi.
ICTCS/CILC
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
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 — 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
2012 J jnl
Simplification Rules for Intuitionistic Propositional Tableaux.
ACM Trans. Comput. Log.
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2010 B conf
A Decidable Constructive Description Logic.
JELIA
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
2010 J jnl
A Note on Semantic Web Services Specification and Composition in Constructive Description Logics
CoRR
Loris Bozzato, Mauro Ferrari
2010 — conf
Composition of Semantic Web Services in a Constructive Description Logic.
RR
Loris Bozzato, Mauro Ferrari
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 J jnl
Actions Over a Constructive Semantics for Description Logics.
Fundam. Informaticae
Loris Bozzato, Mauro Ferrari, Paola Villa
2008 — conf
Actions over a Constructive Semantics for ALC.
Description Logics
Loris Bozzato, Mauro Ferrari, Paola Villa
2008 — conf
Building a Domain Ontology from Glossaries: A General Methodology.
SWAP
Loris Bozzato, Mauro Ferrari, Alberto Trombetta
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 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
On Uniformly Constructive and Semiconstructive Formal Systems.
Log. J. IGPL
Mauro Ferrari, Pierangelo Miglioli, Mario Ornaghi
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
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 B conf
Hypertableau and Path-Hypertableau Calculi for Some Families of Intermediate Logics.
TABLEAUX
Agata Ciabattoni, Mauro Ferrari
1999 J jnl
Duplication-Free Tableau Calculi and Related Cut-Free Sequent Calculi for the Interpolable Propositional Intermediate Logics.
Log. J. IGPL
Alessandro Avellone, Mauro Ferrari, Pierangelo Miglioli
1998 C conf
Synthesis of Programs in Abstract Data Types.
LOPSTR
Alessandro Avellone, Mauro Ferrari, Pierangelo Miglioli
1997 J jnl
Cut-Free Tableau Calculi for some Intuitionistic Modal Logics.
Stud Logica
Mauro Ferrari
1996 B conf
Almost Duplication-Free Tableau Calculi for Propositional Lax Logics.
TABLEAUX
Alessandro Avellone, Mauro Ferrari
1995 J jnl
A Method to Single out Maximal Propositional Logics with the Disjunction Property I.
Ann. Pure Appl. Log.
Mauro Ferrari, Pierangelo Miglioli
1995 J jnl
A Method to Single out Maximal Propositional Logics with the Disjunction Property II.
Ann. Pure Appl. Log.
Mauro Ferrari, Pierangelo Miglioli
1993 J jnl
Counting the Maximal Intermediate Constructive Logics.
J. Symb. Log.
Mauro Ferrari, Pierangelo Miglioli