Geodesic
Craig's interpolation theorem, in computation theory
Atti della Accademia nazionale dei Lincei. Rendiconti della Classe di scienze fisiche, matematiche e naturali, Série 8, Tome 70 (1981) no. 1, pp. 6-11.

Voir la notice de l'article provenant de la source Biblioteca Digitale Italiana di Matematica

Si espongono alcuni risultati, provati dall’Autore negli articoli citati nella bibliografia, a proposito della complessità del teorema d’interpolazione di Craig: con ciò si intende la relazione tra la lunghezza (cioè il numero di simboli) della formula $\chi$ e la lunghezza di $\varphi$ e $\psi$, ove $\varphi \to \psi$ è un’implicazione valida, e $\chi$ è un interpolante, come esibito dal teorema di interpolazione stesso. Si intende altresì sottolineare la rilevanza dello studio della complessità dell’interpolazione per far luce su alcuni importanti problemi della teoria degli algoritmi, con particolare riferimento al problema della complessità dei sistemi naturali di deduzione nella logica delle proposizioni (essenzialmente, problema PNP), oppure il problema di correlare tra loro diverse misure della complessità di una funzione, ad esempio, il tempo occorrente ad una macchina di Turing per calcolare la funzione, rispetto al tempo occorrente ad un circuito «logico». 
@article{RLINA_1981_8_70_1_a1,
     author = {Mundici, Daniele},
     title = {Craig's interpolation theorem, in computation theory},
     journal = {Atti della Accademia nazionale dei Lincei. Rendiconti della Classe di scienze fisiche, matematiche e naturali},
     pages = {6--11},
     publisher = {mathdoc},
     volume = {Ser. 8, 70},
     number = {1},
     year = {1981},
     zbl = {0523.03027},
     mrnumber = {465767},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/RLINA_1981_8_70_1_a1/}
}
TY  - JOUR
AU  - Mundici, Daniele
TI  - Craig's interpolation theorem, in computation theory
JO  - Atti della Accademia nazionale dei Lincei. Rendiconti della Classe di scienze fisiche, matematiche e naturali
PY  - 1981
SP  - 6
EP  - 11
VL  - 70
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/RLINA_1981_8_70_1_a1/
LA  - en
ID  - RLINA_1981_8_70_1_a1
ER  - 
%0 Journal Article
%A Mundici, Daniele
%T Craig's interpolation theorem, in computation theory
%J Atti della Accademia nazionale dei Lincei. Rendiconti della Classe di scienze fisiche, matematiche e naturali
%D 1981
%P 6-11
%V 70
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/RLINA_1981_8_70_1_a1/
%G en
%F RLINA_1981_8_70_1_a1
Mundici, Daniele. Craig's interpolation theorem, in computation theory. Atti della Accademia nazionale dei Lincei. Rendiconti della Classe di scienze fisiche, matematiche e naturali, Série 8, Tome 70 (1981) no. 1, pp. 6-11. http://geodesic.mathdoc.fr/item/RLINA_1981_8_70_1_a1/

[1] A.V. Aho, J.E. Hopcroft and J.D. Ullman (1974) - The design and analysis of computer algorithms, Addison-Wesley, Reading, Mass.. | Zbl

[2] J.L. Bell, M. Machover (1977) - A course in mathematical logic, North-Holland, Amsterdam. | Zbl

[3] S.A. Cook (1971) - The complexity of theorem proving procedures, «Proc. Third ACM Symposium», 151-158.

[4] S.A. Cook and R.A. Rechkow (1979) - The relative efficiency of propositional proof systems, «J. Symb. Logic», 44.1, 36-50. | Zbl

[5] W. Craig (1957) - Linear reasoning. A new form of the Herbrand-Gentzen theorem, «J. Symb. Logic», 22, 250-268. | Zbl

[6] S. Feferman (1974) - Two notes on abstract model theory, I, «Fund. Math.», 82, 153-165, and II, ibid. 89 (1975) 111-130. | fulltext EuDML | Zbl

[7] J.D. Monk (1976) - Mathematical Logic, Springer-Verlag, Berlin. | MR | Zbl

[8] D. Mundici (1981) - Robinson's consistency theorem in soft model theory, «Transactions of the AMS», 263, 231-241. | DOI | MR

[9] D. Mundici (1982) - Compactness = JEP in any logic, «Fund. Math.», to appear.

[10] D. Mundici (1981) - A group-theoretical invariant for elementary equivalence and its role in representations of elementary classes, «Studia Logica», to appear. | DOI | MR

[11] D. Mundici - Complexity of Craig's interpolation, to appear.

[12] D. Mundici - A lower bound for the complexity of Craig's interpolants in sentential logic, «Archv für math. Logik», to appear. | fulltext EuDML | DOI | MR

[13] D. Mundici (1980) - Natural limitations of algorithmic procedures in logic, «Rendiconti Accademia Nazionale Lincei», 69, 101-105. | MR

[14] M.S. Paterson (1976) - An introduction to Boolean function complexity, «Soc. Math, de France», Astérisque 38-39, 183-201.

[15] J.E. Savage (1976) - The complexity of computing, Wiley, New York.

[16] C.P. Schnorr (1976) - The network complexity and the Turing machine complexity of finite functions, «Acta Informatica», 7, 95-107. | MR | Zbl

[17] R.M. Smullyan (1971) - First-order Logic, Springer-Verlag, Berlin. | Zbl

[18] P.M. Spira (1971) - On time-hardware complexity tradeoffs for Boolean functions, Proc. 4th Hawaii Int. Symp. on System Sciences, 525-527.

[19] H. Friedman (1976) - The complexity of explicit definitionsy, «Advances in Math.», 20, 18-29.