Contribution of Warsaw Logicians to Computational Logic

• Main Author: Damian Niwiński
• Format: Article
• Language: English
• Published: MDPI AG 2016-06-01
• Series: Axioms
• Subjects: algorithmic logic; dynamic logic; μ-calculus; λ-calculus
• Online Access: http://www.mdpi.com/2075-1680/5/2/16

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