Craig's interpolation theorem, in computation theory

Mundici, Daniele

Atti della Accademia Nazionale dei Lincei. Classe di Scienze Fisiche, Matematiche e Naturali. Rendiconti, Tome 70 (1981), p. 6-11 / Harvested from Biblioteca Digitale Italiana di Matematica

Résumé

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

Détail

Publié le : 1981-01-01

Zbl 0523.03027

Bibliographie

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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