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