zbMATH — the first resource for mathematics

Tarski’s influence on computer science. (English) Zbl 1425.03003
Garrido, Ángel (ed.) et al., The Lvov-Warsaw school. Past and present. Cham: Birkhäuser. Stud. Univers. Log., 391-404 (2018).
This is an interesting contribution to the history of the relations between logic and computer sciences by one of the major logicians of the 20th century. This paper builds on and completes the biography of Alfred Tarski co-written by the author and his wife, Anita Feferman. The central question of the paper is the following:
“Tarski became recognized as one of the most important logicians of the twentieth century through his many contributions to the areas of set theory, model theory, the semantics of formal languages, decidable theories and decision procedures, undecidable theories, universal algebra, axiomatics of geometry, and algebraic logic. What, in all that, are the connections with computer science?”
After recalling Tarski’s pioneering figure as a logician in the US, the article indicates a month-long Summer Institute in Symbolic Logic held at Cornell University in 1957 as a turning point for this story: “the first to include many speakers from the emerging field of computer science, the theoretical foundations of which had been laid in the 1930s by Gödel, Church, Turing, Post, and Kleene.”
Some of Tarski’s prior students, present at the meeting, worked into the practical applications of one of Tarski’s major results, namely his decision procedure for the algebra of real numbers, and in this way they helped disseminating the knowledge of Tarski’s logical works among computer scientists. Around the same years, companies such as IBM employed researchers with background in mathematics and logic, some of whom had also attended the 1957 memorable meeting.
Another episode crediting the importance of Tarski for the development of computer science regards the vicissitudes related to the publication of his paper The completeness of elementary algebra and geometry. Unable to publish this paper in Paris in 1940, because of the II world war, Tarski revised and published it years later as a RAND report under the title: A decision procedure for elementary algebra and geometry (1948). The RAND corporation was chiefly interested in applying Tarski’s decision method to game theory, and this practical interest for decidability explains the change in the title of the paper.
Even if Tarski had not a high opinion for his students who took a career in computer science, he nevertheless made an effort to reformulate his results in a language more digestible to mathematicians. This can also explain the circulation of his results within mathematicians and then among computer scientists.
On these grounds the author can conclude: “In whatever way the claim is formulated, I think it is fair to say that Tarski’s ideas and the approaches he promoted are so pervasive that even if his influence in this and the various other areas of computer science about which I spoke was not direct it was there at the base, and – to mix a metaphor – it was there in the air, and so the nature and importance of his influence eminently deserves to be recognized.”
Besides being in its own an informative piece in the history of 20th century logic, this article could be also taken as a starting point for further works in the sociology of logic and computer sciences.
For the entire collection see [Zbl 1403.01005].
03-03 History of mathematical logic and foundations
68-03 History of computer science
01A70 Biographies, obituaries, personalia, bibliographies
Biographic References:
Tarski, Alfred
Full Text: DOI
[1] Ajtai, M., Gurevich, Y.: Datalog vs. first-order logic. J. Comput. Syst. Sci. 49, 562-588 (1994) · Zbl 0824.68034
[2] Atserias, A., Dawar, A., Kolaitis, P.G.: On preservation under homomorphisms and unions of conjunctive queries. In: 23rd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS), pp. 319-329. ACM (2004) · Zbl 1326.68117
[3] Barwise, J., Feferman, S. (eds.): Model-Theoretic Logics. Springer, Berlin (1985) · Zbl 0587.03001
[4] Ben-Or, M., Kozen, D., Reif, J.H.: The complexity of elementary algebra and geometry. J. Comput. Syst. Sci. 32(2), 251-264 (1986) · Zbl 0634.03031
[5] Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: CAV’97: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 400-411. Springer, London (1997)
[6] Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: ACM Symposium on Theory of Computing, pp. 460-467. ACM, New York (1988)
[7] Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Series in Symbolic Computation. Springer, Berlin (1998) · Zbl 0906.03033
[8] Codd, E.F.: A relational model of data for large shared data banks. Commun. ACM 13(6), 377-387 (1970) · Zbl 0207.18003
[9] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition - preliminary report. SIGSAM Bull. 8(3), 80-90 (1974)
[10] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proceedings Second GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33, pp. 134-183. Springer, Berlin (1975) (Reprinted in: Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Series in Symbolic Computation, pp. 85-121. Springer, Berlin (1998)) · Zbl 0318.02051
[11] Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299-328 (1991) (Reprinted in: (Reprinted in: Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Series in Symbolic Computation, pp. 174-200. Springer, Berlin (1998)) · Zbl 0754.68063
[12] Davis, M.: The prehistory and early history of automated deduction. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 1: Classical Papers on Computational Logic 1957-1966, pp. 1-28. Springer, Berlin (1983)
[13] Ebbinghaus, H.D., Flum, J.: Finite Model Theory, 2nd edn. Springer, Berlin (1991) · Zbl 0932.03032
[14] Feferman, A.B., Feferman, S.: Alfred Tarski: Life and Logic. Cambridge University Press, New York (2004) · Zbl 1062.03002
[15] Feferman, S.: Tarski’s conceptual analysis of semantical notions. In: Benmakhlouf, A. (ed.) Sémantique et épistémologie, pp. 79-108. Editions Le Fennec, Casablanca [distrib. J. Vrin, Paris] (2004)
[16] Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundam. Math. 47, 57-103 (1959) · Zbl 0088.24803
[17] Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: Karp, R. (ed.) Complexity of Computation. SIAM-AMS Proceedings, vol. 7 , pp. 27-42. American Mathematical Society, Providence (1974) (Reprinted in: (Reprinted in: Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Series in Symbolic Computation, pp. 122-135. Springer, Berlin (1998))
[18] Formisano, A., Omodeo, E.G., Policriti, A.: Three-variable statements of set-pairing. Theor. Comput. Sci. 322(1), 147-173 (2004) · Zbl 1058.03028
[19] Formisano, A., Omodeo, E.G., Policriti, A.: The axiom of elementary sets on the edge of Peircean expressibility. J. Symb. Log. 70, 953-968 (2005) · Zbl 1100.03042
[20] Fribourg, L., Olsén, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 1243, pp. 213-227. Springer, Berlin (1997)
[21] Gierz, G., Hoffman, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices and Domains. Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press, Cambridge (2003)
[22] Gyssens, M., Saxton, L.V., Van Gucht, D.: Tagging as an alternative to object creation. In: Freytag, J.C., Maier, D., Vossen, G. (eds.) Query Processing for Advanced Database Systems, pp. 201-242. Kaufmann, San Mateo (1994)
[23] Halmos, P.: I Want to be a Mathematician: An Automathography. Springer, Berlin (1985) · Zbl 0569.01020
[24] Henkin, L., Monk, D., Tarski, A.: Cylindric Algebras, vol. 1. North-Holland, Amsterdam (1971) · Zbl 0576.03043
[25] Henkin, L., Monk, D., Tarski, A.: Cylindric Algebras, vol. 2. North-Holland, Amsterdam (1971) · Zbl 0576.03043
[26] Hodges, W.: Truth in a structure. Proc. Aristot. Soc. 86, 131-151 (1985-1986)
[27] Imieliński, T., Lipski, W. Jr.: The relational model of data and cylindric algebras. J. Comput. Syst. Sci. 28(1), 80-102 (1984) · Zbl 0557.68067
[28] Kanellakis, P.C.: Elements of relational database theory. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 1073-1156. MIT Press, Cambridge (1990) · Zbl 0900.68090
[29] Lassez, J.L., Nguyen, V.L., Sonnenberg, E.A.: Fixed point theorems and semantics: a folk tale. Inf. Process. Lett. 14, 112-116 (1982) · Zbl 0488.68015
[30] Maddux, R.D.: The origin of relation algebras in the development and axiomatization of the calculus of relations. Stud. Logica 50(3-4), 421-455 (1991) · Zbl 0754.03042
[31] Makowsky, J.A.: Algorithmic uses of the Feferman-Vaught theorem. Ann. Pure Appl. Logic 126, 159-213 (2004) · Zbl 1099.03009
[32] Oppen, D.C.: A \(\(2^{2^{2^{pn}}}\)\) upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci. 16, 323-332 (1978) · Zbl 0381.03021
[33] Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I congrs des Mathmaticiens des Pays Slaves, 92-101 (1929)
[34] Rosen, E.: Some aspects of model theory and finite structures. Bull. Symb. Log. 8, 380-403 (2002) · Zbl 1017.03015
[35] Rossman, B.: Existential positive types and preservation under homomorphisisms. In: Panangaden, P. (ed.) Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science. LICS 2005, pp. 467-476. IEEE Computer Society Press, Washington (2005)
[36] Scott, D.S.: Data types as lattices. SIAM J. Comput. 5, 522-587 (1976) · Zbl 0337.02018
[37] Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P. (eds.) FME 2002: Formal Methods - Getting IT Right, Copenhagen, pp. 1-20. Springer, Berlin (2002) · Zbl 1064.68558
[38] Tarski, A.: On the calculus of relations. J. Symb. Logic 6, 73-89 (1941) · Zbl 0026.24401
[39] Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951) (Reprinted in: Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Series in Symbolic Computation, pp. 24-84. Springer, Berlin (1998))
[40] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285-309 (1955) · Zbl 0064.26004
[41] Tarski, A.: The concept of truth in formalized languages. In: Corcoran, J. (ed.) Logic, Semantics, Metamathematics. Papers from 1923 to 1938, 2nd edn., pp. 182-278. Oxford University Press, Oxford (1983) (original date (1935))
[42] Tarski, A.: On definable sets of real numbers. In: Corcoran, J. (ed.) Logic, Semantics, Metamathematics. Papers from 1923 to 1938, 2nd edn., pp. 110-142. Oxford University Press, Oxford (1983) (Original date (1931))
[43] Tarski, A., Givant, S.: A Formalization of Set Theory Without Variables. Number 41 in Colloquium Publications. American Mathematical Society, Providence (1987) · Zbl 0654.03036
[44] Tarski, A., Givant, S.: Tarski’s system of geometry. Bull. Symb. Log. 5, 175-214 (1999) · Zbl 0932.01031
[45] Tarski, A., Vaught, R.L.: Arithmetical extensions of relational systems. Compos. Math. 13, 81-102 (1957) · Zbl 0091.01201
[46] Van den Bussche, J.: Applications of Alfred Tarski’s Ideas in Database Theory. In: International Workshop on Computer Science Logic. Lecture Notes in Computer Science, vol. 2142, pp. 20-37. Springer, Berlin (2001) · Zbl 0999.68055
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.