×

Contribution of Warsaw logicians to computational logic. (English) Zbl 1415.03006

Summary: The newly emerging branch of research of Computer Science received encouragement from the successors of the Warsaw mathematical school: Kuratowski, Mazur, Mostowski, Grzegorczyk, and Rasiowa. Rasiowa realized very early that the spectrum of computer programs should be incorporated into the realm of mathematical logic in order to make a rigorous treatment of program correctness. This gave rise to the concept of algorithmic logic developed since the 1970s by Rasiowa, Salwicki, Mirkowska, and their followers. Together with Pratt’s dynamic logic, algorithmic logic evolved into a mainstream branch of research: logic of programs. In the late 1980s, Warsaw logicians Tiuryn and Urzyczyn categorized various logics of programs, depending on the class of programs involved. Quite unexpectedly, they discovered that some persistent open questions about the expressive power of logics are equivalent to famous open problems in complexity theory. This, along with parallel discoveries by Harel, Immerman and Vardi, contributed to the creation of an important area of theoretical computer science: descriptive complexity. By that time, the modal \(\mu\)-calculus was recognized as a sort of a universal logic of programs. The mid 1990s saw a landmark result by Walukiewicz, who showed completeness of a natural axiomatization for the \(\mu\)-calculus proposed by Kozen. The difficult proof of this result, based on automata theory, opened a path to further investigations. Later, Bojanczyk opened a new chapter by introducing an unboundedness quantifier, which allowed for expressing some quantitative properties of programs. Yet another topic, linking the past with the future, is the subject of automata founded in the Fraenkel-Mostowski set theory. The studies on intuitionism found their continuation in the studies of Curry-Howard isomorphism. Łukasiewicz’s landmark idea of many-valued logic found its continuation in various approaches to incompleteness and uncertainty.

MSC:

03-03 History of mathematical logic and foundations
03B40 Combinatory logic and lambda calculus
01A60 History of mathematics in the 20th century

Software:

LOGLAN

References:

[1] Grzegorczyk, A.; Some classes of recursive functions; Rozpr. Matemayczne: 1953; Volume 4 ,1-45. · Zbl 0052.24902
[2] Banach, S.; Mazur, S.; Sur les fonctions calculables; Ann. Soc. Pol. Math.: 1937; Volume 16 ,223.
[3] Mazur, S.; Computable analysis; Rozpr. Matemayczne: 1963; Volume 33 ,1-111. · Zbl 0113.24306
[4] Specker, E.; Nicht Konstruktiv Beweisbare Sätze Der Analysis; J. Symb. Log.: 1949; Volume 14 ,145-158. · Zbl 0033.34102
[5] Feferman, S.; Tarski’s Influence on Computer Science; Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS): ; . · Zbl 1126.03005
[6] Tarski, A.; Sur les ensembles définissables de nombres réels I; Fundam. Math.: 1931; Volume 17 ,210-239. · JFM 57.0060.02
[7] Presburger, M.; Über der Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt; Comptes Rendus Premier Congrès des Mathématicienes des Pays Slaves: Warsaw, Poland 1929; ,92-101.
[8] Rasiowa, H.; Sikorski, R.; ; The Mathematics of Metamatematics: Warszawa, Poland 1963; . · Zbl 0122.24311
[9] Engeler, E.; Algorithmic properties of structures; Theor. Comput. Sci.: 1967; Volume 1 ,183-195. · Zbl 0202.00802
[10] Salwicki, A.; Formalized algorithmic languages; Bull. Acad. Polon. Sci. Ser. Sci. Math. Astron. Phys.: 1970; Volume 18 ,227-232. · Zbl 0198.02801
[11] Mirkowska, G.; On formalized systems of algorithmic logic; Bull. Acad. Polon. Sci. Ser. Sci. Math. Astron. Phys.: 1971; Volume 19 ,421-428. · Zbl 0222.02010
[12] Kreczmar, A.; Effectivity Problems in Algorithmic Logic; Ph.D. Thesis: Warsaw, Poland 1973; . · Zbl 0361.02056
[13] Rasiowa, H.; ω+-valued algorithmic logic as a tool to investigate procedures; Mathematical Foundations of Computer Science: Berlin, Germany 1975; ,423-450. · Zbl 0341.68015
[14] Mirkowska, G.; Salwicki, A.; ; Algorithmic Logic: Warszawa, Poland 1987; . · Zbl 0648.03018
[15] Kreczmar, A.; Salwicki, A.; Warpechowski, M.; ; LOGLAN’88—Report on the Programming Language: Berlin, Germany 1990; . · Zbl 0703.68029
[16] Pratt, V.; Semantical Considerations on Floyd-Hoare Logic; Proceedings of the 17th Annual IEEE Symposium on Foundations of Computer Science: ; ,109-121.
[17] Harel, D.; Kozen, D.; Tiuryn, J.; ; Dynamic Logic: Cambridge, MA, USA 2000; . · Zbl 0976.68108
[18] Tiuryn, J.; Urzyczyn, P.; Some Relationships between Logics of Programs and Complexity Theory (Extended abstract); Proceedings of the 24th Annual Symposium on Foundations of Computer Science: ; ,180-184. · Zbl 0652.03028
[19] Immerman, N.; ; Descriptive Complexity: Berlin, Germany 1999; . · Zbl 0918.68031
[20] Kozen, D.; Results on the propositional μ-calculus; Automata, Languages, and Programming: Berlin, Germany 1982; ,348-359. · Zbl 0507.03005
[21] Niwiński, D.; Fixed points vs. infinite generation; Proceedings of the Third Annual Symposium on Logic in Computer Science: ; ,402-409.
[22] Rabin, M.O.; Decidability of second-order theories and automata on infinite trees; Trans. Am. Soc: 1969; Volume 141 ,1-35. · Zbl 0221.02031
[23] Walukiewicz, I.; Completeness of Kozen’s Axiomatisation of the Propositional mu-Calculus; Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science: ; ,14-24. · Zbl 1046.68628
[24] Walukiewicz, I.; Monadic second-order logic on tree-like structures; Theor. Comput. Sci.: 2002; Volume 275 ,311-346. · Zbl 1026.68087
[25] Wajsberg, M.; Untersuchungen über den Aussagenkalkül von A. Heyting; Wiad. Matematyczne: 1938; Volume 46 ,45-101. · Zbl 0019.38503
[26] Kfoury, A.; Tiuryn, J.; Urzyczyn, P.; The Undecidability of the Semi-unification Problem; Inf. Comput.: 1993; Volume 102 ,83-101. · Zbl 0769.68059
[27] Schubert, A.; Second-Order Unification and Type Inference for Church-Style Polymorphism; Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: ; ,279-288.
[28] Sørensen, M.H.; Urzyczyn, P.; ; Lectures on the Curry-Howard Isomorphism: Amsterdam, The Netherlands 2006; Volume Volume 149 . · Zbl 1183.03004
[29] Pawlak, Z.; Rough sets; Int. J. Parallel Program.: 1982; Volume 11 ,341-356. · Zbl 0501.68053
[30] Jankowski, A.; Skowron, A.; Logic for Artificial Intelligence: A Rasiowa—Pawlak School Perspective; Andrzej Mostowski and Foundational Science: Amsterdam, The Netherlands 2008; ,106-143. · Zbl 1149.01021
[31] Lipski, W.; On Semantic Issues Connected with Incomplete Information Databases; ACM Trans. Database Syst.: 1979; Volume 4 ,262-296.
[32] Buss, S.R.; Kołodziejczyk, L.; Zdanowski, K.; Collapsing modular counting in bounded arithmetic and constant depth propositional proofs; Trans. Am. Math. Soc.: 2015; Volume 367 ,7517-7563. · Zbl 1353.03071
[33] Knapik, T.; Niwiński, D.; Urzyczyn, P.; Higher-Order Pushdown Trees Are Easy; Foundations of Software Science and Computation Structures: Berlin, Germany 2002; ,205-222. · Zbl 1077.03508
[34] Bojańczyk, M.; A Bounding Quantifier; Computer Science Logic: Berlin, Germany 2004; ,41-55. · Zbl 1095.03007
[35] Bojańczyk, M.; Toruńczyk, S.; Weak MSO+U over infinite trees; Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science: ; ,48-66. · Zbl 1245.68119
[36] Bojańczyk, M.; Colcombet, T.; Bounds in ω-Regularity; Proceedings of the 21th IEEE Symposium on Logic in Computer Science: ; ,285-296.
[37] Bojańczyk, M.; Parys, P.; Toruńczyk, S.; The MSO+U Theory of (N,<) is undecidable; Proceedings of the 33rd Symposium on Theoretical Aspects of Computer Science: ; ,1-8. · Zbl 1388.03016
[38] Bojańczyk, M.; Gogacz, T.; Michalewski, H.; Skrzypczak, M.; On the Decidability of MSO+U on Infinite Trees; Automata, Languages, and Programming—41st International Colloquium: Berlin, Germany 2015; ,50-61. · Zbl 1407.03007
[39] Krajewski, S.; Srebrny, M.; On the Life and Work of Andrzej Mostowski (1913-1975); Andrzej Mostowski and Foundational Science: Amsterdam, The Netherlands 2008; ,3-14. · Zbl 1146.01008
[40] Bojańczyk, M.; Braud, L.; Klin, B.; Lasota, S.; Towards nominal computation; Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: ; ,401-412. · Zbl 1321.68139
[41] Klin, B.; Lasota, S.; Ochremiak, J.; Toruńczyk, S.; Turing machines with atoms, constraint satisfaction problems, and descriptive complexity; Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): ; ,58:1-58:10. · Zbl 1401.68079
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.