Pierangelo Miglioli

List of Publications (by type)


Journal Papers

    G. Degli Antoni, P. Miglioli, and M. Ornaghi. Procedure per la sintesi di programmi. Rivista di Informatica, VII(Supplemento al numero 3):53-83, 1977.
    P. Miglioli and M. Ornaghi. A calculus to build up correct programs. Mathematical Foundations of Computer Science, 53:398-409, 1977.
    A. Bertoni, G. Mauri, P. Miglioli, and M. Wirsing. On different approaches to abstract data types and the existence of recursive models. EATCS bulletin, 9:47-57, 1979.
    P. Miglioli and M. Ornaghi. La teoria delle prove nella sintesi dei programmi: alcune note. Rivista di Informatica, Supplemento al vol XI(3):49-91, November 1981.
    P. Miglioli and M. Ornaghi. A logically justified model of computation I. Fundamenta Informaticae, IV(1):151-172, 1981.
    Abstract
    The aim of this paper is to provide a general explanation of the "algorithmic content" of proofs, according to a point of view adequate to computer science. Differently from the more usual attitude of program synthesis, where the "algorithmic content" is captured by translating proofs into standard algorithmic languages, here we propose a "direct" interpretation of "proofs as programs". To do this, a clear explanation is needed of what is to be meant by "proof-execution", a concept which must generalize the usual "program-execution". In the first part of the paper we discuss the general conditions to be satisfied by the execution of proofs and consider, as a first example of proof-execution, Prawitz's normalization. According to our analysis, simple normalization is not fully adequate to the goals of the theory of programs: so, in the second section we present an execution procedure based on ideas more oriented to computer science than Prawitz's. We provide a soundness theorem which states that our executions satisfy an appropriate adequacy condition, and discuss the sense according to which our "proof-algorithms" inherently involve parallelism and non determinism. The properties of our computational model are analyzed and also a completeness theorem involving a notion of "uniform evaluation" of open formulas is stated. Finally, an "algorithmic completeness" theorem is given, which essentially states that every flow-chart program proved to be totally correct can be simulated by an appropriate "purely logical proof".

    P. Miglioli and M. Ornaghi. A logically justified model of computation II. Fundamenta Informaticae, IV(2):277-341, 1981.
    P. Miglioli and M. Ornaghi. Constructive proofs and logical computations. Pocitace umela inteligencia, 1(5):369-388, 1982.
    Abstract
    In this paper two different approaches are compared, both using first order logic as a tool to define and solve problems: the first one is the typical Artificial Intelligence approach, where a set of clauses defines a problem and implicitly outlines a solution algorithm whose computations are to be carried out by an automatic theorem prover; the second one is in the frame of constructive Proof Theory, where general solution algorithms can be codifies in the form of appropriate general proofs which do not require theorem provers. The main goal of the paper is to show how the second attitude can help in answering a typical question involved in the first, i.e., whether a given set of clauses is complete with respect to the possibility of solving a given problem.

    A. Bertoni, G. Mauri, and P. Miglioli. On the power of model theory to specify abstract data types and to capture their recursiveness. Fundamenta Informaticae, IV.2:129-170, 1983.
    Abstract
    In this paper a comparative analysis of some algebraic and model-theoretic tools to specify abstract data types is presented: our aim is to show that, in order to capture a quite relevant feature such as recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze various notions such as "initiality", "finality", "monoinitiality", "epifinality", "weak monoinitiality" and "weak epifinality", both from the point of view of "abstractness" and of "cardinality", in a general model theoretic frame. For the second aspect, it is shown that only "initiality", "monoinitiality", "epifinality" and "weak epifinality" allow us to select countable models (for theories with a countable language), a necessary condition to get recursive data types, while this is not the case for "finality" and "weak monoinitiality". An extensive analysis is then devoted to the problem of recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapse, nor it is incompatible with the "abstractness" requirements. We also show that none of the above quoted categorical notions captures recursiveness. Finally, we consider our own definition of "abstract data type" based on typically model-theoretic notions, and illustrate the sense according to which it captures recursiveness.

    P. Miglioli and G. Usberti. Una logica del conoscere. Teoria, 2:111-132, 1984.
    P. Miglioli, U. Moscato, M. Ornaghi, and G. Usberti. A constructivism based on classical truth. Notre Dame Journal of Formal Logic, 30(1):67-90, 1989.
    P. Miglioli, U. Moscato, M. Ornaghi, S. Quazza, and G. Usberti. Some results on intermediate constructive logics. Notre Dame Journal of Formal Logic, 30(4):543-562, 1989.
    Abstract
    Some techniques for the study of intermediate constructive logics are illustrated. In particular a general characterization is given of maximal constructive logics from which a new proof of the maximality of MV (Medvedev's logic of finite problems) can be obtained. Some semantical notions are also introduced, allowing a new characterization of MV, from which a new proof of a conjecture of Fridman's and a new family of principles valid in MV can be extracted.

    M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. AILA Preprint n. 11- gennaio/giugno, 1992.
    Abstract
    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''.

    P. Miglioli. An infinite class of maximal intermediate propositional logics with the disjunction property. Archive for Mathematical Logic, 31:415-432, 1992.
    Abstract
    Infinitely many intermediate propositional logics with the disjunction property are defined, each logic being characterized both in terms of finite axiomatization and in terms of a Kripke semantics with the finite model property. The completeness theorems are used to prove that any two logics are constructively incompatible. As a consequence, one deduces that there exists infinitely many maximal intermediate propositional logics with the disjunction property.

    M. Ferrari and P. Miglioli. Counting the maximal intermediate constructive logics. The Journal of Symbolic Logic, 58(4):1365-14001, 1993.
    Abstract
    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''.

    P. Miglioli, U. Moscato, and M. Ornaghi. An improved refutation system for intuitionistic predicate logic. Journal of Automated Reasoning, 13:361-373, 1994.
    Abstract
    In this paper a refutation calculus for intuitionistic predicate logic is presented where the necessity of duplicating formulas to which rules are applied is analyzed. In line with the semantics of intuitionistic logic in terms of Kripke models a new sign $F_c$ besides the signs $T$ and $F$ is added which reduces the size of the proofs and the involved nondeterminism. The resulting calculus is proved to be correct and complete. An extension of it for Kuroda logic is given.

    P. Miglioli, U. Moscato, and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. The Journal of Symbolic Computation, 18:41-81, 1994.
    Abstract
    We introduce a methodology to treat abstract data types (ADT), abstract parametric classes (APC) and subclasses, together with appropriate inheritance properties, by means of first order theories. The notion of a first order theory axiomatizing an ADT is based on the notion of isoinitial model and has been proposed by the authors in previous papers (Bertoni et al. (1979), Bertoni et al.(1983), Bertoni et al. (1984)). A theory formalizing an APC is seen, in this paper, as a theory $T$ incompletely axiomatizing an ADT. Given a class $\cal C$ of ADT's, the class formalized by $T$ can be seen (under suitable soundness conditions on $T$) as the class of the instances of $T$ over $\cal C$. An instantiation of $T$ by an ADT $\,I$ of $\cal C$ completes $T$ into a $T'$ formalizing an ADT $I'$, which extends $I$ and inherits the properties of the APC $T$. We use both classical and constructive methods in the following sense: on the one hand, the semantics is based on classical model theory; on the other hand, the soundness of a consistent axiomatization can be analyzed by purely syntactical methods, in terms of provability within suitable constructive systems. A theory $T$ formalizing an APC (or an ADT) is not given by a list of axioms, but by a suitable ``APC-expression", which explicitly or implicitly (but effectively) defines the axioms of $T$. We have APC-expressions to define APC's, to extend already defined APC's and to instantiate APC's (into ADT's or subclasses). We allow also ``recurrence APC-expressions". At the end of the paper we give some examples showing how the proposed methodology works.

    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 ther efore 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.

    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.

    A. Avellone, C. Fiorentini, P. Mantovani, and P. Miglioli. On maximal intermediate predicate constructive logics. Studia Logica, 57:373-408, 1996.
    Abstract
    We extend to the predicate frame a previous characterization of the maximal intermediate propositional constructive logics. This provides a technique to get maximal intermediate predicate constructive logics starting from suitable sets of classically valid predicate formulae we call maximal nonstandard predicate constructive logics. As an example of this technique, we exhibit two maximal intermediate predicate constructive logics, yet leaving open the problem of stating whether the two logics are distinct. Further properties of these logics will be also investigated.

    G. Bertolotti, P. Miglioli, and D. Silvestrini. Exhibiting wide families of maximal intermediate propositional logics with the disjunction property. Mathematical Logic Quarterly, 42:501-536, 1996.
    Abstract
    We provide results allowing to state, by the simple inspection of suitable classes of posets (propositional Kripke frames), that the corresponding intermediate propositional logics are maximal among the ones which satisfy the disjunction property. Starting from these results, we directly exhibit, without using the axiom of choice, the Kripke frames semantics of $2^\aleph_0$ maximal intermediate propositional logics with the disjunction property. This improves previous evaluations, giving rise to the same conclusion but made with an essential use of the axiom of choice, of the cardinality of the set of the maximal intermediate propositional logics with the disjunction property.

    P. Miglioli, U. Moscato, and M. Ornaghi. Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic. Logic Journal of the IGPL, 5(1):145-167, 1997.
    Abstract
    Both at the propositional and the predicate level, in tableau systems of intuitionistic logic as well as in the corresponding sequent and natural calculi, the problem arises of reducing as much as possible the duplication of formulas, i.e., the reuse of formulas already used in a proof, in order to single out efficient proof search techniques. This problem has been analyzed in a paper by Dyckhoff, where a nearly optimal solution is given for intuitionistic propositional sequent and natural calculi, and in previuos papers by the authors, where an improvement is proposed of Fitting's tableau system for intuitionistic predicate logic. In the present paper we reanalyze the ideas of our previous works in the light of Dyckhoff's results. This gives rise to a tableau system for intuitionistic predicate logic which provides a good improvement of the previous tableau systems with respect to the problem of duplication. The formal setting of the paper seems to be promising to treat further intermediate logics. In this line, we analyze Kuroda logic and provide for it a tableau system involving a smaller amount of duplication than the one involved in the intuitionistic tableau system presented in the paper.
    Logic Journal of the IGPL, 5(1), 1997

    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.
    Logic Journal of the IGPL, 7(4), 1999

    S. Ghilardi and P. Miglioli. On canonicity and strong completeness conditions in intermediate propositional logics. Studia Logica, 63:1-33, 1999.
    Abstract
    By using algebraic-categorical tools, we establish four criteria in order to disprove canonicity, strong completeness, $\omega$-canonicity and strong $\omega$-completeness, respectively, of an intermediate propositional logic. We then apply the second criterion in order to get the following result: all the logics defined by extra-intuitionistic one-variable schemata, except four of them, are not strongly complete. We also apply the fourth criterion in order to prove that the Gabbay-de Jongh logic $D_1$ is not strongly $\omega$-complete.

    C. Fiorentini and P. Miglioli. A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications. Logic Journal of the IGPL, 7(6):733-753, 1999.
    Abstract
    Cut-free sequent calculi for the predicate intermediate logic CD of constant domains have appeared only very recently in literature, even if this logic has been axiomatized since the early seventies. In the present paper we propose a different cut-free sequent calculus for CD, in which a great care is devoted in avoiding duplications of formulas.
    Logic Journal of the IGPL, 7(6), 1999

Collections

    A. Bertoni, G. Mauri, P. Miglioli, and M. Ornaghi. Abstract data types and their extension within a constructive logic. In G. Kahn, D.B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of LNCS, pages 177-195. Springer-Verlag, 1984.
    P. Miglioli, U. Moscato, and M. Ornaghi. Constructive theories with abstract data types for program synthesis. In D.G. Skordev, editor, Mathematical Logic and its Applications, pages 293-302. Plenum Press, New York, 1988.
    P. Miglioli, U. Moscato, and M. Ornaghi. Pap: a logic programming system based on a constructive logic. In M. Boscarol, L. Carlucci Aiello, and G. Levi, editors, Foundations of Logic and Functional Programming, pages 143-156. Springer-Verlag, 1988.
    P. Miglioli, U. Moscato, and M. Ornaghi. Semi-constructive formal systems and axiomatization of abstract data types. In J. Diaz and F. Orejas, editors, TAPSOFT'89, LNCS, pages 337-351. Springer-Verlag, 1989.
    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. 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.

Conference Proceedings

    D. Marini and P. Miglioli. Characterization of programs and their synthesis from a formalized theory. In Mathematical Foundations of Computer Science. Proceedings of symposium and summer school, pages 259-266. Mathematical Institute of the Slovak Academy of Sciences, Computing Research Centre, United Nations D.P. Bratislava, September 1973.
    P. Miglioli. Mathematical foundations of motivation languages and synthesis maps. In A. Blikle, editor, Mathematical Foundations of Computer Science: 3rd Symposium at Jadwisin near Warsaw, volume 28 of LNCS, pages 388-408. Springer-Verlag, June 1974.
    P. Miglioli. Note sui linguaggi di motivazione e sulle mappe di sintesi. In Convegno di informatica teorica, pages 45-71, Mantova, November 1974. Gruppo Nazionale di Cibernetica e Biofisica, Associazione Italiana per il Calcolo Automatico, Associazione Europea di Informatica Teorica.
    V. De Antonellis, G. Degli Antoni, R. Polillo, P. Miglioli, and S. Rossetti. Un sistema di programmazione destinato ad operare su un frammento di lingua italiana. In Atti del terzo congresso nazionale di cibernetica e biofisica, 1974.
    G. Degli Antoni, P. Miglioli, and M. Ornaghi. Top-down approach to synthesis of programs. In Programming symposium. Proceedings, colloque sur la programmation, pages 88-108, 1974.
    G. Degli Antoni, P. Miglioli, and M. Ornaghi. Merging synthesis and top-down approach in programming. In Colloque sur la Programmation. Resumes des communications, pages 76-81, 1974.
    G. Degli Antoni, P. Miglioli, and M. Ornaghi. The sysnthesis of programs as an approach to the construction of reliable programs. In G. Huet and G. Kahn, editors, Proc. Int. Symp. on Proving and Improving Programs, Arc et Senans, pages 327-352, 1975.
    D. Marini, P. Miglioli, and M. Ornaghi. First order logic as a tool to solve and classify problems. In Jahrestagung. Proceedings, pages 669-679, 1975.
    P. Miglioli and M. Ornaghi. Sintetizzatore: un programma per la sintesi di programmi corretti. In Aica: atti del congresso annuale, pages 31-38, 1975.
    A. Bertoni, G. Mauri, and P. Miglioli. Una guida euristica alla soluzione di problemi combinatori. In Atti del convegno complessità di calcolo, modelli gestionali e territorio, pages 181-193, 1977.
    A. Bertoni, G. Mauri, and P. Miglioli. Model theoretic aspects of abstract data specification. In Proceedings of Mathematical Logic in Computer Science, pages 181-193. North-Holland, 1978.
    A. Bertoni, G. Mauri, and P. Miglioli. A characterization of abstract data types as model theoretic invariants. In Procceeding of 6th ICALP, volume 71 of LNCS, pages 26-37. Springer-Verlag, 1979.
    A. Bertoni, G. Mauri, and P. Miglioli. Towards a theory of abstract data types: a discussion on problems and tools. In International Symposium on Programming. Proceedings of the 4th Colloque International sur la Programmation, pages 44-58, 1980.
    P. Miglioli, U. Moscato, and M. Ornaghi. Trees in Kripke semantics and in intuitionistic refutation system. In E. Astesiano and C. Bhoem, editors, CAAP '81, volume 112 of LNCS, pages 316-330. Springer-Verlag, 1981.
    P. Miglioli, U. Moscato, and M. Ornaghi. Logica costruttiva e metodi di programmazione: alcune note. In Aica: atti del congresso annuale, volume 2, pages 639-650. Aica, Pavia, September 1981.
    Abstract
    Queste note fanno il punto sullo stato di una ricerca tuttora in corso il cui scopo è quello di studiare se alcuni strumenti e concetti tipici della logica costruttiva siano utilizzabili come strumento di analisi delle metodologie di programmazione e possano fornire indicazioni in tal senso. Al momento, si sono riconosciute alcune corrispondenze, che vengono illustrate informalmente con degli esempi nella seconda sezione. Nella prima, invece, si presenta una panoramica sul costruttivismo; tale panoramica non esaurisce tutte le tematiche relative, ma mette in luce quegli aspetti che riteniamo più interessanti per la teoria dei programmi. In particolare, nella penultima sottosezione si presentano, in maniera molto succinta, tre sistemi formali orientati alla computazione.

    P.Miglioli, U. Moscato, M.Ornaghi, and G. Usberti. Constructive validity and classical truth to assign meaning to programs. In Second World Conference on Mathematics at the Service of Man, pages 490-500. Universidad Politecnica De Las Palmas, 1982.
    Abstract
    This paper aims to show that some technical ideas from constructive logic provide interesting tools for programming methodology. To this end a new constructive logic E* is presented, whose proofs are interpreted as programs. A comparison is made with Intuitionistic Logic, in order to show that E* is more adequate to the practice of programming.

    P. Miglioli, U. Moscato, and M. Ornaghi. Alcuni calcoli intermedi costruttivi. In C. Bernardi, editor, Atti degli Incontri di Logica Matematica, pages 377-386, 1982.
    P. Miglioli, U. Moscato, and M. Ornaghi. Definizioni induttive nei calcoli logici costruttivi e nelle metodologie di programmazione. In Aica: atti del congresso annuale, volume 1, pages 249-257. Aica, Padova, Cleup, October 1982.
    Abstract
    Questo lavoro è una prosecuzione di quello presentato al Congresso AICA'81; in tale lavoro venivano utilizzati gli strumenti delle logioche costruttive per analizzare alcuni aspetti delle metodologie di programma zione. In particolare, sie era riconosciuta una corrispondenza fra le costruzioni relative a $\wedge$, $\vee$, $\exists$, $\forall$-limitato ed i concetti usuali di recod e file. Qui si estende l'analisi ai connettivi $\forall$ e $\rightarrow$, utilizzando una nuova sematica del costruttivismo basata sul concetto di "dato logico". Su questa base si prenderanno in esame ambiti non puramente logici, analizzando in particolare le regole specifiche associate alle definizioni induttive; si daranno alcuni esempi fra cui la derivazione della metodologia Phos.

    P. Miglioli, U. Moscato, and M. Ornaghi. Constructive proofs as programs executable by PrT Nets. In C. Girault and W. Reisig, editors, Application and Theory of Petri Nets, volume 52 of LNCS, pages 311-322. Springer-Verlag, 1982.
    P. Miglioli, U. Moscato, and M. Ornaghi. Un sistema logico-inferenziale di programmazione. In Aica: atti del congresso annuale, volume 1, pages 349-359, 1983.
    Abstract
    In questo lavoro si descrive un progetto di implementazione di un sistema logico costruttivo in cui le formule sono utilizzate come specificazioni di dati e di problemi e le prove come soluzioni effettive di questi ultimi (cioè "programmi" che li risolvono). Il sistema logico costruttivo qui utilizzato è stato trattato dagli autori nei suoi aspetti teorici in [9], mentre per l'analisi di alcune connessioni con la teoria dei programmi e con le metodologie di programmazione si vedano [10,11].

    P. Miglioli, U. Moscato, and M. Ornaghi. Alcuni sistemi costruttivi e semicostruttivi del primo ordine. In R. Ferro and A. Zanardi, editors, Atti degli Incontri di Logica Matematica, volume 3, pages 59-67, 1986.
    P. Miglioli, U. Moscato, and M. Ornaghi. Teorie del primo ordine da un punto di vista di costruttivismo `ingenuo': compatibilità costruttiva di principi matematici e logici in un sistema deduttivo grande. In A. Zanardo, editor, Atti degli Incontri di Logica Matematica, volume 4, pages 99-113, 1987.
    P. Miglioli, U. Moscato, and M. Ornaghi. A constructive logic approach to database theory. In Logic Programming-Proceeding of the First Russian Conference on Logic Programming, LNCS, pages 302-321, 1990.
    Abstract
    In this paper we propose an approach to database theory based on a constructive logic. The semantics here assumed is a particular one; it is based on the notion of info(K,F) (the information type of F), where K is the set of constants of a first order language L, F is a formula of L and info(K,F) is the set of all possible pieces of information (within L) on the "truth" of F. This constructive semantics will be used to treat problems related to relational databases such as disjunctive information and null value.

    P. Miglioli, U. Moscato, and M. Ornaghi. Program specification and synthesis in constructive formal systems. In K. K. Lau and T.P. Clement, editors, Logic Program Synthesis and Transformation, Manchester 1991, pages 13-26. Springer-Verlag, 1991.
    Abstract
    Constructive mathematics has been proposed by many authors as a theoretical basis for program synthesis, and various implementations of this idea have been developed. However, the main problem in implementation is how to build a real environment for software development. In this paper, we present the main features of a logical system we are studying which provides specification tools and a deductive system for deriving programs from their specifications. Our aim is to use this system as a starting point for a real programming environment.

    P. Miglioli, U. Moscato, and M. Ornaghi. How to avoid duplications in refutation systems for intuitionistic logic and Kuroda logic. In K. Broda, M. D' Agostino, R. Goré, R. Johnson, and S. Reeves, editors, Theorem Proving with Analytic Tableaux and Related Methods: 3rd International Workshop, Abingdon, U.K., pages 169-187, May 1994.
    Abstract
    Both at the propositional and the predicate level, in tableaux systems of intuitionistic logic as well a s in the corresponding sequent and natural calculi, the problem arises of reducing as much as possible the duplic ation of formulas, i.e., the reuse of formulas already used in a proof, in order to single out efficient proof s earch techniques. This problem has been analyzed by Dyckhoff in [2], where a nearly optimal solution is given for intuitio nistic propositional sequent and natural calculi, and in [10,11], where an improvement is proposed of Fitting's tableaux system of [3] for intuitionistic predicate logic. In the present paper we reanalyze the ideas of [10,11] in the light of Dyckhoff's results, which are considered from the point of view of a refutation calculus and in the fram e of full first order logic. This gives rise to a tableaux system for intuitionistic predicate logic which should provide a good improvement of the previous systems with respect to the problem of duplication. The formal setting of th e paper seems to be promising to treat further logics. In this line, we analyze Kuroda logic and provide for it a tableaux system involving a smaller amount of duplication than the one involved in the intuitionistic refutation calculus presented in the paper.

    P. Miglioli, U. Moscato, and M. Ornaghi. Refutation systems for propositional modal logics. In P. Baumgartner, R. H\"anle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods: 4th International Workshop, Schloss Rheinfels, St. Goar, Germany, volume 918 of LNAI, pages 95-105. Springer-Verlag, 1995.
    Abstract
    In this paper we analyse refutation systems for propositional modal logics from the point of view of studying efficient decision procedures. In particular, we focus our attention on the problem of duplications (or looping [Gir], or repetitions [Fit2]) of formulas to which the rules of the calculus are applied. For intuitionistic propositional logic this problem has been extensively analysed in sequent and natural deduction systems [Dyc]; in [MMO, MMO1] the problem of duplications in refutation systems for intuitionistic predicate logic and Kuroda logic has been treated. In [MMO, MMO1] a nearly optimal solution to this problem has been given. This result was obtained by capturing into the calculus itself the semantics of the underlying logics. Here we want to apply the ideas of [MMO, MMO1] to propositional modal logics; in particular, we will show that the introduction of an explicit sign intended to characterize the semantics of the necessity operator will avoid unnecessary duplications. For the modal logic S4 this problem has been treated in [Hud], [Wal], [Gir] for sequent calculus, matrix proof method and tableau system respectively. It turns out that the main result of [Gir] asserting that S4 is loop-free is not correct. The propositional modal logics for which complete and correct refutation systems are presented here are S4, K1, K1.1 and S5; the first three calculi are analytic and for K1.1 (also known as S4Grz) we will show that no duplication is required; for S5 (which is semi-analytic) we will introduce, following [Fit1], a suitable calculus which does not require cut rule and lowers the number of duplications.

    A. Avellone, P. Miglioli, U. Moscato, and M. Ornaghi. Generalized tableau systems for intermediate propositional logics. In D. Galmiche, editor, Proceedings of the 6th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods: Tableaux '97, volume 1227 of LNAI, pages 43-61. Springer-Verlag, 1997.
    Abstract
    Given an intermediate propositional logic L (obtained by adding to intuitionistic logic INT a single axiom-scheme), a pseudo tableau system for L can be given starting from any intuitionistic tableau system and adding a rule which allows to insert in any line of a proof table suitable T-signed instances of the axiom-scheme. In this paper we study some sufficient conditions from which, given a well formed formula H, the search for these instances can be restricted to a suitable finite set of formulae related to H. We illustrate our techniques by means of some known logics, namely, the logic $D$ of Dummett, the logics $PR_k$ ($k\geq 1$) of Nagata, the logics $FIN_m$ ($m\geq 1$), the logics $G_n$ ($n\geq 1$) of Gabbay and de Jongh, and the logic $KP$ of Kreisel and Putnam.

    A. Avellone, M. Ferrari, and P. Miglioli. Synthesis of programs in abstract data types (extended abstract). In Pre-Proceedings of LOPSTR'98. Depart. of Computer Science, University of Manchester, UMCS-98-6-1, 1998.
    A. Avellone, M. Ferrari, P. Miglioli, and U. Moscato. A tableau calculus and a cut-free sequent calculus for Dummett predicate logic. In H.C.M. de Swart, editor, Position Papers, pages 1-18. International Conference TABLEAUX'98, Analytic Tableaux and Related Methods, Katholieke Universiteit Brabant, 1998.
    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 (which are usually called ``contractions'' in the frame of the sequent calculi).

    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 LNCS, 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.

    M. Ferrari, C. Fiorentini, and P. Miglioli. Goal oriented information extraction in uniformly constructive calculi. In Proceedings of WAIT'99: Workshop Argentino de Inform\'atica Te\'orica, pages 51-63, 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.

Editor

    A. Bertoni, C. Boehm, and P. Miglioli, editors. Theoretical computer science. Proceedings of the third italian conference. World Scientific, 1989.
    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. Springer-Verlag, 1996.

Miscellaneous

    P. Miglioli. La correttezza dei programmi. Tesi di laurea, Dipartimento di Fisica, Università degli Studi di Milano. Relatore Prof. G. Degli Antoni, Correlatore Prof. M. Cugiani. In italian, 1970.
    G. Degli Antoni, P. Miglioli, and M. Ornaghi. The synthesis of programs in an intuitionistic frame. Technical report, Istituto di Cibernetica dell' Università di Milano, 1974.
    P. Miglioli. Notes on motivation-languages and synthesis-maps. Technical Report MIG-5, Istituto di Cibernetica dell' Università di Milano, 1975.
    P. Miglioli and M. Ornaghi. The synthesis of programs as an approach to the construction of reliable programs. Technical Report MIG-6, Istituto di Cibernetica dell' Università di Milano, 1976.
    P. Miglioli and M. Ornaghi. A purely logical computing model: the open proofs as programs. Technical Report MIG-7, Istituto di Cibernetica dell'Università di Milano, 1979.
    P. Miglioli, U. Moscato, M. Ornaghi, and G. Usberti. Semantical analysis of some (standard or non standard) intermediate propositional constructive logics: maximality and smoothness results. Technical Report 25-88, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1988.
    P.Miglioli, U. Moscato, M.Ornaghi, and G. Usberti. Constructive validity and classical truth to assign meaning to programs: extended version. Technical Report 31-88, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1988.
    P.Miglioli, U. Moscato, and M.Ornaghi. An improved refutation system for intuitionistic predicate logic. Technical Report 37-88, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1988.
    A. Bertoni, G. Mauri, P.Miglioli, and M.Ornaghi. Decision problems and evaluation problem in an abstract data type. Technical Report 39-88, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1988.
    A. Bertoni, G. Mauri, P. Miglioli, and M. Ornaghi. Some models of computation from a proof-theoretical point of view. Technical Report 40-88, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1988.
    P. Miglioli, U. Moscato, and M. Ornaghi. The computational model of the system pap. Technical report, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1989.
    A constructive logic approach to database theory. P. miglioli and u. moscato and m. ornaghi. Technical Report 91-91, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1991.
    Abstract
    In this paper we propose an approach to database theory based on a constructive logic. The semantics here assumed is a particular one; it is based on the notion of info (K,F) (the information type of F), where K is the set of constants of a first order language L, F is a formula of L and info (K,F) is the set of all the possible pieces of information (within L) on the "truth" of F. This constructive sematics will be used to treat problems related to relational databases such as disjuntive information and null value.

    A. Bertoni, G. Mauri, and P. Miglioli. Some uses of model theory to specify abstract data types and capture their recursiveness. Technical Report 96-93, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1993.
    Abstract
    In this paper we present a comparative analysis of some algebraic-categorical tools and of some model theoretic tools to characterize abstract data types: our aim is to show that, in order to capture a quite relevant feature such as the recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze from a model theoretic point of view various notions such as "initiality", "finality", "monoinitiality", "epifinality", "weak monoinitiality" and "weak epifinality", the latter being also called "terminality": this analysis is carried out from the double point of view of "abstractness" (which of these notions gives rise to unique up to isomorphisms models) and of "cardinality". For the second aspect, in a general model theoretic frame the considered notions do not necessarily give rise to countable models. So, we state which of them allow to select countable models: it turns out that only "initiality", "monoinitiality", "epifinality" and "terminality" capture countability if theories with a countable language are involved, while this is not the case for "finality" and "weak monoinitiality". Countability is seen as a necessary condition to get recursive data types. An extensive analysis is then devoted to the problem of the recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapses, nor it is incompatible with the "abstractness requirement". We also show that none of the above quoted categorical notions captures recursiveness. Finally, we consider our own definition of "abstract data type", which has been already presented in [3] and is based on typically model theoretic notions, even if in [3] we have erroneously emphasized the notion of "monoinitiality": we analyze our definition in the frame of the proposed formalization of recursiveness, and illustrate the sense according to which it captures recursiveness.

    P. Miglioli, U. Moscato, and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. Technical Report 97-93, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1993.
    Abstract
    We introduce a methodology to treat abstract data types (ADT), abstract parametric classes (APC) and subclasses, together with appropriate inheritance properties, by means of first order theories. The notion of a first order theory axiomatizing an ADT is based on the notion of isoinitial model and has been proposed by the authors in previous papers (Bertoni et al. (1979), Bertoni et al.(1983), Bertoni et al. (1984)). A theory formalizing an APC is seen, in this paper, as a theory $T$ incompletely axiomatizing an ADT. Given a class $\cal C$ of ADT's, the class formalized by $T$ can be seen (under suitable soundness conditions on $T$) as the class of the instances of $T$ over $\cal C$. An instantiation of $T$ by an ADT $\,I$ of $\cal C$ completes $T$ into a $T'$ formalizing an ADT $I'$, which extends $I$ and inherits the properties of the APC $T$. We use both classical and constructive methods in the following sense: on the one hand, the semantics is based on classical model theory; on the other hand, the soundness of a consistent axiomatization can be analyzed by purely syntactical methods, in terms of provability within suitable constructive systems. A theory $T$ formalizing an APC (or an ADT) is not given by a list of axioms, but by a suitable ``APC-expression", which explicitly or implicitly (but effectively) defines the axioms of $T$. We have APC-expressions to define APC's, to extend already defined APC's and to instantiate APC's (into ADT's or subclasses). We allow also ``recurrence APC-expressions". At the end of the paper we give some examples showing how the proposed methodology works.

    P. Miglioli, U. Moscato, and M. Ornaghi. An improved refutation system for intuitionistic predicate logic. Technical Report MPI-I-93-213, Max-Planck-Institut f\"ur Informatik, 1993.
    M. Ferrari and P. Miglioli. A method to single out maximal intermediate propositional logics with the disjunction property. Technical Report 98-93, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1993.
    Abstract
    We study a class of 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. The method 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. In presenting our maximal logics, we will also propose some ideas for a classification of them.

    P. Miglioli, U. Moscato, and M. Ornaghi. How to avoid duplications in refutation systems for intuitionistic logic and Kuroda logic. Technical Report 99-93, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1993.
    Abstract
    Both at the propositional and the predicate level, in tableaux systems of intuitionistic logic as well a s in the corresponding sequent and natural calculi, the problem arises of reducing as much as possible the duplic ation of formulas, i.e., the reuse of formulas already used in a proof, in order to single out efficient proof s earch techniques. This problem has been analyzed by Dyckhoff in [2], where a nearly optimal solution is given for intuitio nistic propositional sequent and natural calculi, and in [10,11], where an improvement is proposed of Fitting's tableaux system of [3] for intuitionistic predicate logic. In the present paper we reanalyze the ideas of [10,11] in the light of Dyckhoff's results, which are considered from the point of view of a refutation calculus and in the fram e of full first order logic. This gives rise to a tableaux system for intuitionistic predicate logic which should provide a good improvement of the previous systems with respect to the problem of duplication. The formal setting of th e paper seems to be promising to treat further logics. In this line, we analyze Kuroda logic and provide for it a tableaux system involving a smaller amount of duplication than the one involved in the intuitionistic refutation calculus presented in the paper.

    A. Avellone, C. Fiorentini, P. Mantovani, and P. Miglioli. A maximal intermediate predicate constructive logic. Technical Report 108-93, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 1993.
    Abstract
    We provide an example of a maximal intermediate predicate logic with the disjunction property and the explicit definability property which contains the well known Medvedev's propositional logic of the finite problems. We also show that (differently from Medvedev's logic) our intermediate predicate logic cannot have a Kripke frame semantics. Indeed, we introduce an auxiliary nonstandard predicate logic by means of a special "non-kripkean semantics", and characterize our logic in terms of such a nonstandard logic, according to a method which has been applied in previous papers to get maximal intermediate propositional logics with the disjunction property. Our technique to single out maximal intermediate predicate logics with the disjunction property and the explicit definability property starting from suitable auxiliary nonstandard predicate logics is not as general as the corresponding propositional one; however, we believe that it can be successfully applied also outside the context of the present paper.

    A. Avellone, M. Ferrari, and P. Miglioli. Dupliation-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, 1997.
    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

    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, 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

    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, 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.
    PostScript version

    M. Ferrari, P. Miglioli, and M. Ornaghi. Foundations of uniformly constructive and uniformly semiconstructive formal systems. Technical Report 256/2000, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, 2000.
    Abstract
    We propose a formalization of a notion of strongly constructive 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\vee 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. We also introduce a weaker notion of strongly semiconstructive formal system, requiring classical logic to complete the ``constructive content'' involved in its proofs. We provide examples of strongly constructive and strongly semiconstructive systems. 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.
    PostScript version