Publications

[1]

M. Ferrari, C. Fiorentini. Goal-oriented proof-search in natural deduction for Intuitionistic Propositional Logic. Journal of Automated Reasoning, 62(1):127-165, 2019.

Abstract. We address the problem of proof-search in the natural deduction calculus for Intuitionistic propositional logic. Our aim is to improve the usual proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Nbu, a variant of the usual natural deduction calculus for Intuitionistic Propositional Logic, and we show that it can be used as a base for a goal-oriented proof-search procedure. We also show that the implementation of our proof-search procedure is competitive with those based on sequent or tableaux calculi.

[DOI]

[2]M. Ferrari and C. Fiorentini and G. Fiorino. A Sequent Based On-the-fly Procedure to Get Hilbert Proofs in Classical Propositional Logic. In IARIA, editor, COMPUTATION TOOLS 2019, pages 10–15, 2019.
[3]

C. Fiorentini and M. Ferrari. A Forward Unprovability Calculus for Intuitionistic Propositional Logic. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017, LNCS, vol. 10501, pages 114–130. Springer International Publishing, 2017.

Abstract. The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. This method has been successfully applied to a variety of logics. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability. From a derivation of G in FRJ(G) we can extract a Kripke countermodel for G. Since in forward methods sequents are not duplicated, the generated countermodels do not contain redundant worlds and are in general very concise.

[DOI]

[4]

M. Ferrari, C. Fiorentini, and G. Fiorino. Proof-search in Hilbert calculi. In D. Della Monica and A. Murano and S. Rubin and L. Sauro, editors, CILC 2017 Italian Conference on Computational Logic, volume 1949 of CEUR Proceedings, ISBN/ISSN: 1613-0073, pages 301-305, 2017.

[pdf]

[5]

M. Ferrari, C. Fiorentini and G. Fiorino. JTabWb: a Java framework for implementing terminating sequent and tableau calculi. Fundamenta Informaticae, 150(1):119-142, 2017.

Abstract. JTabWb is a Java framework for developing provers based on sequent or tableau calculi. It provides a generic engine which searches for proof of a given goal driven by a user-defined prover. The user is required to define the components of a prover by implementing suitable Java interfaces. In this paper we describe the structure of the framework and the role of its components through a running example. To show the generality of the framework we review some of the provers implemented in JTabWb. Finally, to corroborate the fact that the framework can be used to generate efficient provers, we compare the performances of one of the implemented provers with the state-of-the-art provers for Intuitionistic Propositional Logic.

[DOI]

[6]

M. Ferrari and C. Fiorentini. Proof-search in natural deduction calculus for classical propositional logic. In H. De Nivelle, editor, TABLEAUX 2015, LNCS, vol. 9323, pages 237–252. Springer International Publishing, 2015

Abstract. We address the problem of proof-search in the natural deduction calculus for Classical propositional logic. Our aim is to improve the usual naïve proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Ncr, a variant of the usual natural deduction calculus for Classical propositional logic, and we show that it can be used as a base for a proof-search procedure which does not require backtracking nor loop-checking.

[DOI]

[7]

M. Ferrari, C. Fiorentini, and G. Fiorino. An Evaluation-Driven Decision Procedure for G3i. ACM Transactions on Computational Logic (TOCL), 6(1):8:1–8:37, 2015.

Abstract. It is well-known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the näive goal-oriented proof-search strategy, consisting in applying the rules of the calculus bottom-up until possible, can generate branches of infinite length. The usual solution to this problem is to support the proof-search procedure with a loop-checking mechanism which prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development. In this paper we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism which, analyzing only the current goal of the proof-search, allows one to drive the application of rules so to guarantee termination and to avoid useless backtracking. We describe an evaluation-driven proof-search procedure that given a sequent \(\sigma\) returns either a G3i-derivation of \(\sigma\) or a counter-model for \(\sigma\). We prove that such a procedure is terminating and correct and that the depth of the G3i-trees generated during proof-search is quadratic in the size of \(\sigma\). Finally, we discuss the overhead time introduced by evaluation functions in the proof-search procedure.

[DOI]

[8]M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Quarta edizione. Pearson Italia, 2015.
[9]M. Ferrari, C. Fiorentini, and G. Fiorino. A new refutation calculus with logical optimizations for PLTL. In IARIA, editor, COMPUTATION TOOLS 2015, pages 39–41, 2015.
[10]

M. Ferrari, C. Fiorentini, and G. Fiorino. JTabWb: a Java framework for implementing terminating sequent and tableau calculi. In L. Giordano, V. Gliozzi and G.L. Pozzato, editors, CILC 2014 Italian Conference on Computational Logic, volume 1195 of CEUR Proceedings, ISBN/ISSN: 1613-0073, pages 46-530, 2014.

Abstract. JTabWb is a Java framework for developing provers based on terminating sequent or tableau calculi. It provides a generic engine which performs proof-search driven by a user-defined specification. The user is required to define the components of a prover by implementing suitable Java interfaces. The implemented provers can be used as standalone applications or embedded in other Java applications. The framework also supports proof-trace generation, LaTeX rendering of proofs and counter-model generation.

[pdf]

[11]

M. Ferrari, C. Fiorentini, and G. Fiorino. A terminating evaluation-driven variant of G3i. In D. Galmiche and D. Larchey-Wendling, editors, TABLEAUX 2013, LNCS, volume 8123, pages 104-118. Springer-Verlag, 2013.

Abstract. We present Gbu, a terminating variant of the sequent calculus G3i for intuitionistic propositional logic. Gbu modifies G3i by annotating the sequents so to distinguish rule applications into two phases: an unblocked phase where any rule can be backward applied, and a blocked phase where only right rules can be used. Derivations of Gbu have a trivial translation into G3i. Rules for right implication exploit an evaluation relation, defined on sequents; this is the key tool to avoid the generation of branches of infinite length in proof-search. To prove the completeness of Gbu, we introduce a refutation calculus Rbu for unprovability dual to Gbu. We provide a proof-search procedure that, given a sequent as input, returns either a Rbu-derivation or a Gbu-derivation of it.

[DOI]

[12]

M. Ferrari, C. Fiorentini, and 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, 51(2):129-149, 2013.

Abstract. In this paper we present LSJ, a contraction-free sequent calculus for Intuitionistic propositional logic whose proofs are linearly bounded in the length of the formula to be proved and satisfy the subformula property. We also introduce a sequent calculus RJ for intuitionistic unprovability with the same properties of LSJ. We show that from a refutation of RJ of a sequent \(\sigma\) we can extract a Kripke counter-model for \(\sigma\). Finally, we provide a procedure that given a sequent \(\sigma\) returns either a proof of σ in LSJ or a refutation in RJ such that the extracted counter-model is of minimal depth.

[DOI]

[13]

M. Ferrari, C. Fiorentini, and G. Fiorino. Simplification Rules for Intuitionistic Propositional Tableaux. ACM Transactions on Computational Logic (TOCL), 13(2), 2012.

Abstract. The implementation of a logic requires, besides the definition of a calculus and a decision procedure, the development of techniques to reduce the search space. In this paper we introduce some simplification rules for Intuitionistic propositional logic that try to replace a formula with an equi-satisfiable simpler one with the aim to reduce the search space. Our results are proved via semantical techniques based on Kripke models. We also provide an empirical evaluation of their impact on implementations.

[DOI]

[14]

M. Ferrari, C. Fiorentini, and G. Fiorino. BCDL: Basic Constructive Description Logic. Journal of Automated Reasoning, 44(4):371-399, 2010.

Abstract. In this paper we present BCDL, a description logic based on information terms semantics, which allows a constructive interpretation of ALC formulas. In the paper we describe the information terms semantics, we define a natural deduction calculus for BCDL and we show it is sound and complete. As a first application of proof-theoretical properties of the calculus, we show how it fulfils the proofs-as-programs paradigm. Finally, we discuss the role of generators, the main element distinguishing our formalisation from the usual ones.

[DOI]

[15]

M. Ferrari, C. Fiorentini, and G. Fiorino. FCube: An Efficient Prover for Intuitionistic Propositional Logic. In C. G. Fermuller and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17, volume 6397, pages 294-301. Springer, 2010.

Abstract. In this system description we provide FCube, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. The main novelty of FCube is that it implements several optimization techniques that allow to prune the search space acting on different aspects of the proof-search. We tested the efficiency of our techniques by comparing FCube with other theorem provers. We found that our prover outperforms the other provers on several interesting families of formulas.

[DOI]

[16]

L.Bozzato, M. Ferrari, C. Fiorentini, and G. Fiorino. A decidable constructive description logic. In T. Janhunen and I. Niemela, editors, Logics in Artificial Intelligence, JELIA 2010, volume 6341, pages 51-63. Springer, 2010.

Abstract. Recently, there has been a growing interest in constructive reinterpretations of description logics. This has been motivated by the need to model in the DLs setting problems that have a consolidate tradition in constructive logics. In this paper we introduce a constructive description logic for the language of ALC based on the Kripke semantics for Intuitionistic Logic. Moreover we give a tableau calculus and we show that it is sound, complete and terminating.

[DOI]

[17]

L.Bozzato and M. Ferrari. A Note on Semantic Web Services Specification and Composition in Constructive Description Logics. arXiv:1007.2364, CoRR, pages 15, 2010.

Abstract. The idea of the Semantic Web is to annotate Web content and services with computer interpretable descriptions with the aim to automatize many tasks currently performed by human users. In the context of Web services, one of the most interesting tasks is their composition. In this paper we formalize this problem in the framework of a constructive description logic. In particular we propose a declarative service specification language and a calculus for service composition. We show by means of an example how this calculus can be used to define composed Web services and we discuss the problem of automatic service synthesis.

[arXiv]

[18]

L.Bozzato and M. Ferrari. Composition of Semantic Web Services in a Constructive Description Logic, In P. Hitzler and T. Lukasiewicz, editors, Web Reasoning and Rule Systems, RR 2010, volume 6333 of Lecture Notes in Computer Science, pages 223-226. Springer, 2010.

Abstract. We formalize the problem of service composition in the framework of a constructive description logic. We propose a declarative service specification language and a calculus for service composition.

[DOI]

[19]

L. Bozzato, M. Ferrari and P. Villa. Actions over a constructive semantics for description logics. Fundamenta Informaticae, 96, 1-17, 2009.

Abstract. Following the approaches given in recent works about action languages over description logics, we propose an action formalism based on a constructive information terms semantics for ALC. We discuss how a notion of state can be naturally encoded by this semantics. We address the problems of determining executability of an action, building the state obtained by an action applicaztion and checking its consistency: we present an algorithm to solve the latter two problems.

[DOI]

[20]

M. Ferrari, C. Fiorentini, and G. Fiorino. A Tableau Calculus for Propositional Intuitionistic Logic with a Refined Treatment of Nested Implications. Journal of Applied Non-Classical Logics, 19(2):144-166, 2009.

Abstract. Since 1993, when Hudelmaier developed an \(O(n\log n)\)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind \(T((A\to B)\to C)\) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and the width of proofs with respect to Hudelmaier’s one. These improvements have a significant influence on the performances of the implementation.

[DOI]

[21]

M. Ferrari, C. Fiorentini, and G. Fiorino. Towards the use of Simplification Rules in Intuitionistic Tableaux. Proceedings of CILC09, 24-esimo Convegno Italiano di Logica Computazionale. 2009.

Abstract. By replacement it is meant the substitution of one or more occurrences of a formula with an equivalent one. In automated deduction this can be useful to reduce the search space. In tableau calculi for classical and modal logics this technique is known as simplification and consists in replacing a formula with a logical constant (true or false). Recently, this idea has been applied to Intuitionistic Logic. This work in progress investigates further conditions on the applicability of Simplification in Intuitionistic Logic.

[pdf]

[22]

L. Bozzato, M. Ferrari and P. Villa. A note on constructive semantics for description logics. Proceedings of CILC09, 24-esimo Convegno Italiano di Logica Computazionale. 2009.

Abstract. Following the approaches and motivations given in recent works about constructive interpretation of description logics, we introduce the constructive description logic IALC. This logic is based on a Kripke-style semantics inspired by the Kripke semantics for Intuitionistic first order logic. In the paper we present the main features of our semantics and we study its relations with other approaches. Moreover, we present a tableau calculus which turns out to be sound and complete for IALC.

[pdf]

[23]

M. Ferrari, C. Fiorentini, A. Momilgiano and M. Ornaghi. Snapshot generation in a constructive object-oriented modeling language. In A. King, editor Logic Based Program Synthesis and Transformation, LOPSTR 2007, Selected Papers, volume 4915 of Lecture Notes in Computer Science, pages 169-184. Springer-Verlag, 2008.

Abstract. CooML is an object-oriented modeling language where specifications are theories in a constructive logic designed to handle incomplete information. In this logic we view snapshots as a formal counterpart of object populations, which are associated with specifications via the constructive interpretation of logical connectives. In this paper, we introduce the snapshot semantics of CooML and we describe a snapshot generation (SG) algorithm, which can be applied to validate specifications in the spirit of OCL-like constraints over UML models. Differently from the latter and from the standard BHK semantics, the logic allows us to exploit a notion of partial validation that is appropriate to encodings characterised by incomplete information. SG is akin to model generation in answer set programming. We show that the algorithm is sound and complete so that its successful termination implies consistency of the system.

[DOI]

[24]

L. Bozzato, M. Ferrari, and A. Trombetta. Building a domain ontology from glossaries: a general methodology. In A. Gangemi and J. Keizer and V. Presutti and H. Stoermer, editors Proceedins of 2008 Semantic Web Applications and Perspectives, SWAP 2008, volume 426 of CEUR Proceedings, ISBN/ISSN: 1613-0073, pages 1-10, 2008.

Abstract. We propose a general methodology to build up a domain ontology from one or more domain glossaries. The particular feature of this methodology is in the parallel construction of a domain ontology and a complete domain terminology. In this paper we fully describe the methodology phases and we apply them to a real-world example from the medical domain.

[pdf]

[25]

L. Bozzato, M. Ferrari and P. Villa. Actions over a constructive semantics for ALC. In F. Baader and C. Lutz and B. Motik, editors Proceedins of 2008 International Workshop on Description Logics, volume 353 of CEUR Proceedings, ISBN/ISSN: 1613-0073, 2008.

Abstract. Following the approaches and motivations given in recent works about action languages over description logics, we propose an action formalism based on a constructive semantics for ALC.

[pdf]

[26]M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Terza edizione. Pearson Addison-Wesley, 2008.
[27]

L. Bozzato, M. Ferrari, C. Fiorentini and G. Fiorino. A constructive semantics for ALC. In D. Calvanese and E. Franconi and V. Haarslev and D. Lembo and B. Motik and A.-Y. Turhan and S. Tessaris, editors Proceedins of 2007 International Workshop on Description Logics, volume 250 of CEUR Proceedings, ISBN/ISSN: 1613-0073, pages 219-226, 2007.

Abstract. One of the main concerns of constructive semantics is to provide a computational interpretation for the proofs of a given logic. In this paper we introduce a constructive semantics for the basic description logic ALC in the spirit of the BHK interpretation. We prove that such a semantics provides an interpretation of ALC formulas consistent with the classical one and we show how, according to such a semantics, proofs of a suitable natural deduction calculus for ALC support a proofs-as-programs paradigm.

[pdf]

[28]

M. Ornaghi, M.Benini, M. Ferrari, C. Fiorentini, and A. Momigliano. A Constructive Modeling Language for Object Oriented Information Systems. Proceedings of Constructive Logic for Automated Software Engineering, volume 153(1):55-75 of Electronic Notes in Theoretical Computer Science, 2006.

Abstract. The central aspect in an Information System is the meaning of data in the external world and the information carried by them. We propose a Modeling Language for Object Oriented Information Systems based on a constructive logic of the pieces of information, where the focus is on the meaning of data and on the correct way of storing, exchanging and elaborating information. Although the research work presented in this paper is still preliminary, we believe that its potential applications are of interest for the community.

[DOI]

[29]

A.Avellone, M. Ferrari, C. Fiorentini, G.Fiorino and U.Moscato. ESBC: an application for computing stabilization bounds. Proceedings of Constructive Logic for Automated Software Engineering, volume 153(1):23-33 of Electronic Notes in Theoretical Computer Science, 2006.

Abstract. We describe the application ESBC to perform the timing analysis of a combinatorial circuit. The circuit is described by formulas of Classical Logic and the delays of propagation of the signals in a gate are represented by a kind of valuation form semantics. ESBC computes the exact stabilization times at which the output signals stabilize.

[DOI]

[30]

M. Ferrari, C. Fiorentini, and G. Fiorino. On the complexity of the disjunction property in intuitionistic and modal logics. ACM, TOCL, 6(3):519-538, 2005.

Abstract. In this paper we study the complexity of disjunction property for Intuitionistic Logic, the modal logics S4, S4.1, Grzegorczyk Logic, Gödel-Löb Logic and the intuitionistic counterpart of the modal logic K. For S4 we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require to prove structural properties of the calculi in hand, such as the Cut-elimination Theorem or the Normalization Theorem. This is a key-point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known.

[DOI]

[31]M. Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Seconda edizione. Pearson Education Italia, 2005.
[32]

M. Ferrari, C. Fiorentini, and G. Fiorino. A secondary semantics for second order intuitionistic propositional logic. Mathematical Logic Quarterly, 50(2):202-210, 2004.

Abstract. In this paper we propose a Kripke-style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics.

[DOI]

[33]

M. Ferrari and C.Fiorentini. A proof-theoretical analysis of semiconstructive intermediate theories. Studia Logica, 73(1):21-49, 2003.

Abstract. In the 80’s Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of large subsystems of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that provide computational procedures only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility.

[DOI]

[34]

M. Ferrari, P. Miglioli, and M. Ornaghi. On uniformly constructive and semiconstructive formal systems. Logic Journal of the IGPL, 11(1):1-49, 2003.

Abstract. We propose a formalization of two notions of uniformly constructive formal system, we call uniform e-constructivity and uniform r-constructivity. On an intuitive ground, the first (extended) notion concerns formal systems characterized by calculi with the following properties: any proof of a formula such as \(A\lor B\) (of a formula such as \(\exists xA(x)\)) contains sufficient information to build up a proof of \(A\) or a proof of \(B\) (respectively, a proof of \(A(t)\) for some term \(t\)). On the other hand, the second (restricted) notion takes into account the same properties only for \(A\lor B\), \(\exists xA(x)\) and \(t\) closed. Our treatment allows us to analyze both weak systems (containing only purely logical principles or, at most, weak mathematical axioms) and powerful ones (comparable with Intuitionistic Arithmetic or extensions of its), and exceeds the class of intuitionistic systems, as well as the class of systems for which normalization or cut-elimination theorems can be stated; moreover, it allows us to tackle systems to which the variants of recursive realizability interpretation most known in literature are not applicable. We also introduce a weaker notion of uniformly semiconstructive formal system, requiring classical logic to complete the constructive content involved in its proofs. We give examples of uniformly constructive and uniformly semiconstructive systems. Finally, we provide an example of a system which is not uniformly constructive (more than this, not uniformly semiconstructive), yet satisfying the disjunction property and the explicit definability property.

[DOI]

[35]M.Ferrari and G. Pighizzini. Dai fondamenti agli oggetti. Corso di programmazione Java. Pearson Education Italia, ISBN 88 7192 205 0, 2003.
[36]

M. Ferrari, C. Fiorentini, and 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, number 2514 in Lecture Notes in Artificial Intelligence, pages 175-189. Springer-Verlag, 2002.

Abstract. In this paper we provide a uniform framework, based on extraction calculi, where to study the complexity of the problem to decide the disjunction and the explicit definability properties for Intuitionistic Logic and some Superintuitionistic Logics. Unlike the previous approaches, our framework is independent of structural properties of the proof systems and it can be applied to Natural Deduction systems, Hilbert style systems and Gentzen sequent systems.

[DOI]

[37]

M. Ferrari, C. Fiorentini, and M. Ornaghi. Extracting exact time bounds from logical proofs. In A. Petterossi, editor, Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Selected Papers, volume 2372 of Lecture Notes in Computer Science, pages 245-265. Springer-Verlag, 2002.

Abstract. Accurate evaluation of delays of combinatorial circuits is crucial in circuit verification and design. In this paper we present a logical approach to timing analysis which allows us to compute exact stabilization bounds while proving the correctness of the boolean behavior.

[DOI]

[38]

M. Ferrari, C. Fiorentini, and G. Fiorino. Tableau calculi for the logics of finite k-ary trees. In TABLEAUX 2002, Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of Lecture Notes in Artificial Intelligence, pages 115-129. Springer-Verlag, 2002.

Abstract. We present tableau calculi for the logics \(D_k\) (\(k\geq 2\)) semantically characterized by the classes of Kripke models built on finite k-ary trees. Our tableau calculi use the signs T and F, some tableau rules for Intuitionistic Logic and two rules formulated in a hypertableau fashion. We prove the Soundness and Completeness Theorems for our calculi. Finalgly, we use them to prove the main properties of the logics \(D_k\), in particular their constructivity and their decidability.

[DOI]

[39]

A. Ciabattoni and M. Ferrari. Hypersequent calculi for some intermediate logics with bounded Kripke models. Journal of Logic and Computation, 11(2):283-294, 2001.

Abstract. In this paper we define cut-free hypersequent calculi for some intermediate logics semantically characterized by bounded Kripke models. In particular we consider the logics characterized by Kripke models of bounded width \(Bw_k\), by Kripke models of bounded cardinality \(Bc_k\) and by linearly ordered Kripke models of bounded cardinality \(Dum_k\). The latter family of logics coincides with finite-valued Gödel logics. Our calculi turn out to be very simple and natural. Indeed, for each family of logics (respectively, \(Bw_k\), \(Bc_k\) and \(Dum_k\)), they are defined by adding just one structural rule to a common system, namely the hypersequent calculus for Intuitionistic Logic. This structural rule reflects in a natural way the characteristic semantical features of the corresponding logic.

[DOI]

[40]

A. Avellone, M. Ferrari, and C. Fiorentini. A formal framework for synthesis and verification of logic programs. In K. K. Lau, editor, Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000, Selected Papers, volume 2042 of Lecture Notes in Computer Science, pages 1-17. Springer-Verlag, 2001.

Abstract. In this paper we present a formal framework, based on the notion of extraction calculus, which has been applied to define procedures for extracting information from constructive proofs. Here we apply such a mechanism to give a proof-theoretic account of SLD-derivations. We show how proofs of suitable constructive systems can be used in the context of deductive synthesis of logic programs, and we state a link between constructive and deductive program synthesis.

[DOI]

[41]

M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate semiconstructive HA-systems. Mathematical Structures in Computer Science, 11:589-696, 2001.

Abstract. In this paper we describe research in progress on the problem of extracting information from proofs. Here we concentrate our attention on semiconstructive calculi, which is a kind of calculus which is of interest in the framework of program synthesis and formal verification. We discuss the notion of uniformly semiconstructive calculus, introduce our information extraction mechanism and apply it to two calculi extending Intuitionistic Arithmetic.

[DOI]

[42]

A. Ciabattoni and M. Ferrari. Hypertableau and path-hypertableau calculi for some families of intermediate logics. In R. Dyckhoff, editor, TABLEAUX 2000, Automated Reasoning with Analytic Tableaux and Related Methods, volume 1947 of LNAI, pages 160-174. Springer-Verlag, 2000.

Abstract. In this paper we investigate the tableau systems corresponding to hypersequent calculi. We call these systems hypertableau calculi. We define hypertableau calculi for some propositional intermediate logics. We then introduce path-hypertableau calculi which are simply defined by imposing additional structure on hypertableaux. Using path-hypertableaux we define analytic calculi for the intermediate logics \(Bd_k\), with \(k \geq 1\), which are semantically characterized by Kripke models of depth \(\leq k\). These calculi are obtained by adding one more structural rule to the path-hypertableau calculus for Intuitionistic Logic.

[DOI]

[43]

M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate T-systems. Technical Report 252-00, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.

Abstract. In this paper we will study the problem of uniformly extracting information from constructive and semiconstructive calculi. We will define an information extraction mechanism and will explain several examples of systems to which such a mechanism can be applied. In particular, we will give as examples some families of effective subsystems of a wide class of very large intermediate theories, we call T-systems. These large T-systems, even if ineffective and semantically defined, provide a uniform and fruitful framework where to analyze the possible combinations in a uniformly constructive context of mathematical and super-intuitionistic logical principles.

Presented at IMLA99: Intuitionistic Modal Logics and Application, Trento, July 6, 1999

[pdf]

[44]

M. Ferrari, C. Fiorentini, and P. Miglioli. Extracting information from intermediate semiconstructive HA-systems. Technical Report 253-00, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.

Abstract. In this paper we will study the problem of uniformly extracting information from proofs in semiconstructive calculi, a kind of calculi which is of interest in the framework of program synthesis. Here we will discuss the notion of uniformly constructive calculus, we introduce our information extraction mechanism and we apply it to two calculi extending Intuitionistic Arithmetic.

[pdf]

[45]

M. Ferrari, C. Fiorentini, and P. Miglioli. Goal oriented information extraction in uniformly constructive calculi. In Argentinian Workshop on Theoretical Computer Science (WAIT 99), pages 51-63. Sociedad Argentina de Informàtica e Investigaciòn Operativa, 1999.

Abstract. In this paper we describe a method to extract information from constructive proofs of suitable systems using an extractive calculus. This method relies on the definition of uniformly constructive calculus, and allows to extend the family of systems for which a good information extraction procedure can be defined to include superintuitionistic systems for which a Normalization Theorem or a Cut-elimination Theorem does not hold. However, in the general setting we can only assure that the extraction calculus contains proofs of bounded logical complexity. In this paper we study systems for which the extraction calculus can be characterized in a goal-oriented manner. We will show that such a goal-oriented procedure can be defined for proofs in an Intuitionistic calculus of appropriate sequents. Finally we will prove that this result can be extended to the intuitionistic calculus enriched by the Grzegorczyk Principle and the Descending Chain Principle.

[pdf]

[46]

A. Avellone, M. Ferrari, and P. Miglioli. Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics. Logic Journal of the IGPL, 7(4):447-480, 1999.

Abstract. We get cut-free sequent calculi for the interpolable propositional intermediate logics by translating suitable duplication-free tableau calculi developed within a semantical framework. From this point of view, the paper also provides semantical proofs of the admissibility of the cut-rule for appropriate cut-free sequent calculi.

[DOI]

[47]

A. Avellone, M. Ferrari, and P. Miglioli. Synthesis of programs in abstract data types. In 8th International Workshop on Logic-based Program Synthesis and Transformation, volume 1559 of Lecture Notes in Computer Science, pages 81-100. Springer-Verlag, 1999.

Abstract. In this paper we propose a method for program synthesis from constructive proofs based on a particular proof strategy, we call dischargeable set construction. This proof-strategy allows to build proofs in which active patterns (sequences of application of rules with proper computational content) can be distinguished from correctness patterns (concerning correctness properties of the algorithm implicitly contained in the proof). The synthesis method associates with every active pattern of the proof a program schema (in an imperative language) translating only the computational content of the proof. One of the main features of our method is that it can be applied to a variety of theories formalizing ADT’s and classes of ADT’s. Here we will discuss the method and the computational content of some principles of particular interest in the context of some classes of ADT’s.

[DOI]

[48]

A. Avellone, M. Ferrari, P. Miglioli, and U. Moscato. A tableau calculus for Dummett predicate logic. In Walter A. Carnielli and Itala M. D’Ottaviano, editors, Advances in Contemporary Logic and Computer Science, volume 235 of Contemporary Mathematics, pages 135-151. American Mathematical Society, 1999.

Abstract. In this paper we present a tableau calculus and a cut-free sequent calculus for Dummett predicate logic. A special care is devoted to reduce as much as possible the duplications.
[49]

M. Ferrari. Cut-free tableau calculi for some intuitionistic modal logics. Studia Logica, 59(3):303-330, 1997.

Abstract. In this paper we provide cut-free tableau calculi for the intuitionistic modal logics IK, ID, IT, i.e. the intuitionistic analogues of the classical modal systems K, D and T. Further, we analyse the necessity of duplicating formulas to which rules are applied. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Specifically, we enlarge the language with the new signs Fc and CR near to the usual signs T and F. In this work we establish the soundness and completeness theorems for these calculi with respect to the Kripke semantics propose by Fischer Servi.

[DOI]

[50]

M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1997.

Abstract. We propose a formalization of a notion of strongly constructived formal system, intuitively intended as a formal system characterized by a calculus with the following properties: any proof of a closed formula such as \(A\lor B\) (of a closed formula such as \(\exists xA(x)\)) contains sufficient information to build up a proof of \(A\) or a proof of \(B\) (respectively, a proof of \(A(t)\) for some closed term \(t\)). Our treatment far exceeds the class of intuitionistic systems and the class of system for which normalization or cut-elimination theorems can be stated. In the thesis we exhibith several superintuitionistic formal systems which turns out to be strongly constructive. Finally, we provide an example of a system which is not strongly constructive (more than this, not strongly semiconstructive), yet satisfying the disjunction property and the explicit definability property.

[pdf]

[51]

A. Avellone, M. Ferrari and P. Miglioli. Duplication-free tableau calculi together with cut-free and contraction-free sequent calculi for the interpolable propositional intermediate logics, Technical Report 210-97, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 2000.

Abstract. We get cut-free and contraction-free sequent calculi for the interpolable propositional intermediate logics by translating suitable duplication-free tableau calculi developed within a semantical framework. From this point of view, the paper aims also to outline a general semantical method to get cut-free sequent calculi for appropriate intermediate logics.

[pdf]

[52]

A. Avellone and M. Ferrari. Almost duplication-free tableaux calculi for propositional Lax logics. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings of the 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of LNAI, pages 48-64. Springer-Verlag, 1996.

Abstract. In this paper we provide tableau calculi for the intuitionistic modal logics LAX and LAX1, where the calculus for LAX1 is duplication-free while among the rules for LAX there is just one rule that allows duplication of formulas. These logics have been investigated by Fairtlough and Mendler in relation to the problem of Formal Hardware Verification. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Namely, we enlarge the language containing the usual sings T and F with the new sign Fc. LAX and LAX1 logics are characterized by a Kripke-semantics which is a weak version of the semantics for ordinary intuitionistic modal logics. In this paper we establish the soundness and completeness theorems for these calculi.

[DOI]

[53]

M. Ferrari and P. Miglioli. A method to single out maximal propositional logics with the disjunction property II. Annals of Pure and Applied Logic, 76:117-168, 1995.

Abstract. This is the second part of a paper devoted to the study of the maximal intermediate propositional logics with the disjunction property (we will simply call maximal constructive logics), whose firs part, indicated as [5] in the references, has appeared in this journal with the title “A method to single out maximal propositional logics with the disjunction property I”. In [5] we have explained the general results upon which a method to single out maximal constructive logics is based and have illustrated such a method by exhibiting the Kripke semantics of maximal constructive logics extending the logic ST of Scott, for which, in turn, a semantical characterization in terms of Kripke frames has been given. In the present part we complete the illustration of the method of [5], having in mind some aspects which might be interesting for a classiffication of the maximal constructive logics, and an application of the heuristic content of the method to detect the non-maximality of apparently maximal constructive logics. Thus, on the one hand we introduce the logic AST (“anti” ST), which is compared with ST and is seen as a logic “alternative” (or even “opposite”) to it, in a sense which will be precisely explained. We provide a Kripke semantics for AST and (without exhibiting them) show that (near the ones including ST and the ones including AST) there are maximal constrctive logics which neither are extensions of ST nor are extensions of AST. Finally, we give a further application of the results of [5] by exhibiting the Kripke semantics of a maximal constructive logic extending AST. On the other hand, we compare the maximal constructive logics presented in both parts of the paper with a consructive logic introduced by L. L. Maksimova in [13], which has been conjectured to be maximal by Chagrov and Zacharyashchev in [3]; from this comparison a disproof of the conjecture arises.

[DOI]

[54]

M. Ferrari and P. Miglioli. A method to single out maximal propositional logics with the disjunction property I. Annals of Pure and Applied Logic, 76:1-46, 1995.

Abstract. This is the first part of a paper concerning intermediate propositional logics with the disjunction property which cannot be properly extended into logics of the same kind, and are therefore called maximal. To deal with these logics, we use a method based on the search of suitable nonstandard logics, which has an heuristic content and has allowed us to discover a wide family of logics, as well as to get their maximality proofs in a uniform way. The present part illustrates infinitely many maximal logics with the disjunction property extending the well-known logic of Scott, and aims to provide a first picture of the method, sufficient for the reader who wish to achieve an overall understanding of it without entering into the further aspects developed in the second part. From this point of view, the latter will not be self-contained, but will be seen as a prosecution and a complement of the former, with the aim that the material presented in the whole paper can be used as a starting point for a classification of the subject.

[DOI]

[55]

M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. Journal of Symbolic Logic, 58(4):1365-1401, 1993.

A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjuntion property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise “constructively incompatible constructive logics”. We use a notion of semiconstructive logic, and define wide sets of constructive logics by representing the “constructive” logics as “limits” of decreasing sequences of “semiconstructive” logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, filtrations over rank formulas are used to show that any two different logics belonging to a suitable uncountable set of “constructive” logics are “constructively incompatible”.

[DOI]

[56]M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. AILA Preprint n. 11 - gennaio/giugno, 1992.
[57]M. Ferrari. Logiche intermedie costruttive massimali. Master’s thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1990.