Mauro Ferrari

Publication Activity (10 Years)

Years Active: 1993-2024
Publications (10 Years): 16

Top Topics

Propositional Logic

Top Venues

Fundam. Informaticae

ACM Trans. Comput. Log.

J. Autom. Reason.

Publications

Camillo Fiorentini, Mauro Ferrari
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic. J. Autom. Reason. 68 (3) (2024)
Camillo Fiorentini, Mauro Ferrari
A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property. IJCAR (2) (2024)
Camillo Fiorentini, Mauro Ferrari
A New Approach to Clausification for Intuitionistic Propositional Logic. CILC (2023)
Camillo Fiorentini, Mauro Ferrari
Forward refutation for Gödel-Dummett Logics. CILC (2022)
Camillo Fiorentini, Mauro Ferrari
SAT-Based Proof Search in Intermediate Propositional Logics. IJCAR (2022)
Camillo Fiorentini, Mauro Ferrari
A forward internal calculus for model generation in S4. J. Log. Comput. 31 (3) (2021)
Camillo Fiorentini, Mauro Ferrari
Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic. ACM Trans. Comput. Log. 21 (3) (2020)
Camillo Fiorentini, Mauro Ferrari
Forward proof-search and Countermodel Construction in Intuitionistic Propositional Logic. ICTCS (2020)
Camillo Fiorentini, Mauro Ferrari
A Natural Deduction Calculus for Gödel-Dummett Logic Internalizing Proof-search Control Mechanisms. CILC (2020)
Mauro Ferrari, Camillo Fiorentini
Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic. J. Autom. Reason. 62 (1) (2019)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Forward Countermodel Construction in Modal Logic K. CILC (2018)
Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano
From Constructivism to Logic Programming: an Homage to Mario Ornaghi. Fundam. Informaticae 161 (1-2) (2018)
Camillo Fiorentini, Mauro Ferrari
Duality between unprovability and provability in forward proof-search for Intuitionistic Propositional Logic. CoRR (2018)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi. Fundam. Informaticae 150 (1) (2017)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Proof-Search in Hilbert Calculi. ICTCS/CILC (2017)
Camillo Fiorentini, Mauro Ferrari
A Forward Unprovability Calculus for Intuitionistic Propositional Logic. TABLEAUX (2017)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations. CILC (2015)
Mauro Ferrari, Camillo Fiorentini
Proof-Search in Natural Deduction Calculus for Classical Propositional Logic. TABLEAUX (2015)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
An Evaluation-Driven Decision Procedure for G3i. ACM Trans. Comput. Log. 16 (1) (2015)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi. CILC (2014)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models. J. Autom. Reason. 51 (2) (2013)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
A Terminating Evaluation-Driven Variant of G3i. TABLEAUX (2013)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Simplification Rules for Intuitionistic Propositional Tableaux. ACM Trans. Comput. Log. 13 (2) (2012)
Loris Bozzato, Mauro Ferrari
A Note on Semantic Web Services Specification and Composition in Constructive Description Logics CoRR (2010)
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
A Decidable Constructive Description Logic. JELIA (2010)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
fCube: An Efficient Prover for Intuitionistic Propositional Logic. LPAR (Yogyakarta) (2010)
Loris Bozzato, Mauro Ferrari
Composition of Semantic Web Services in a Constructive Description Logic. RR (2010)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
\boldsymbol {\cal BC\!D\!L}: Basic Constructive Description Logic. J. Autom. Reason. 44 (4) (2010)
Loris Bozzato, Mauro Ferrari, Paola Villa
Actions Over a Constructive Semantics for Description Logics. Fundam. Informaticae 96 (3) (2009)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications. J. Appl. Non Class. Logics 19 (2) (2009)
Loris Bozzato, Mauro Ferrari, Alberto Trombetta
Building a Domain Ontology from Glossaries: A General Methodology. SWAP (2008)
Loris Bozzato, Mauro Ferrari, Paola Villa
Actions over a Constructive Semantics for ALC. Description Logics (2008)
Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi
Snapshot Generation in a Constructive Object-Oriented Modeling Language. LOPSTR (2007)
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
A Constructive Semantics for ALC. Description Logics (2007)
Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino, Ugo Moscato
ESBC: an application for computing stabilization bounds. Electron. Notes Theor. Comput. Sci. 153 (1) (2006)
Mario Ornaghi, Marco Benini, Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano
A Constructive Object Oriented Modeling Language for Information Systems. Electron. Notes Theor. Comput. Sci. 153 (1) (2006)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
On the complexity of the disjunction property in intuitionistic and modal logics. ACM Trans. Comput. Log. 6 (3) (2005)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
A secondary semantics for Second Order Intuitionistic Propositional Logic. Math. Log. Q. 50 (2) (2004)
Mauro Ferrari, Camillo Fiorentini
A Proof-theoretical Analysis of Semiconstructive Intermediate Theories. Stud Logica 73 (1) (2003)
Mauro Ferrari, Pierangelo Miglioli, Mario Ornaghi
On Uniformly Constructive and Semiconstructive Formal Systems. Log. J. IGPL 11 (1) (2003)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Tableau Calculi for the Logics of Finite k-Ary Trees. TABLEAUX (2002)
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics. LPAR (2002)
Mauro Ferrari, Camillo Fiorentini, Pierangelo Miglioli
Extracting information from intermediate semiconstructive HA-systems - extended abstract. Math. Struct. Comput. Sci. 11 (4) (2001)
Mauro Ferrari, Camillo Fiorentini, Mario Ornaghi
Extracting Exact Time Bounds from Logical Proofs. LOPSTR (2001)
Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini
A Formal Framework for Synthesis and Verification of Logic Programs. LOPSTR (LNCS 2042: Selected Papers) (2000)
Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini
A formal framework for synthesis and verification of logic programs. LOPSTR (2000)
Agata Ciabattoni, Mauro Ferrari
Hypertableau and Path-Hypertableau Calculi for Some Families of Intermediate Logics. TABLEAUX (2000)
Alessandro Avellone, Mauro Ferrari, Pierangelo Miglioli
Duplication-Free Tableau Calculi and Related Cut-Free Sequent Calculi for the Interpolable Propositional Intermediate Logics. Log. J. IGPL 7 (4) (1999)
Alessandro Avellone, Mauro Ferrari, Pierangelo Miglioli
Synthesis of Programs in Abstract Data Types. LOPSTR (1998)
Mauro Ferrari
Cut-Free Tableau Calculi for some Intuitionistic Modal Logics. Stud Logica 59 (3) (1997)
Alessandro Avellone, Mauro Ferrari
Almost Duplication-Free Tableau Calculi for Propositional Lax Logics. TABLEAUX (1996)
Mauro Ferrari, Pierangelo Miglioli
A Method to Single out Maximal Propositional Logics with the Disjunction Property II. Ann. Pure Appl. Log. 76 (2) (1995)
Mauro Ferrari, Pierangelo Miglioli
A Method to Single out Maximal Propositional Logics with the Disjunction Property I. Ann. Pure Appl. Log. 76 (1) (1995)
Mauro Ferrari, Pierangelo Miglioli
Counting the Maximal Intermediate Constructive Logics. J. Symb. Log. 58 (4) (1993)