Wolfgang Schreiner - Thinking Programs: Logical Modeling and Reasoning About Languages, Data, Computations, and Executions

Mathematics is a key technology in modern society. Symbolic Computation is on its way to become a key technology in mathematics. Texts and Monographs in Symbolic Computation provides a platform devoted to reflect this evolution. In addition to reporting on developments in the field, the focus of the series also includes applications of computer algebra and symbolic methods in other subfields of mathematics and computer science, and, in particular, in the natural sciences. To provide a flexible frame, the series is open to texts of various kind, ranging from research compendia to textbooks for courses.

Indexed by zbMATH.

More information about this series at http://www.springer.com/series/3073

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

When I started my study of mathematics at the University of Innsbruck in 1960, like most freshmen, I was intimidated and impressed by the apparent intelligence of the professors who gave proofs of abstract knowledge, which was far from the concrete thinking about mathematical objects which we had seen in high-school. However, after some time, in secret, I started to doubt the quality of some of the hand-waving proofs and I wanted to look behind the scene. For this, in parallel and independent of the curriculum, I started to dig through the books on logic I found in the general library of the university. (For some reason, most of them had a yellow coverthe Springer Books on Logic. Subconsciously, this may have been the reason why, many years later, I decided that the cover the Journal of Symbolic Computation should be yellow, when I founded it in 1985.)

From that time on, it became more and more clear to me that logic is the essence of mathematical thinking and, luckily, very soon after my start as a mathematics student I got the chance to become one of the first programmers on the first computer at our university and the computer appeared to me as materialized logic. Since then, for me, mathematics, logic, and computer science was just one field and I am still fascinated and convinced by the repeated algorithmic cycles through object and meta-levels to reach higher and higher states of insight and a more and more efficient grasp of the thinking process. Understanding the spiral of logic for (algorithmic) mathematics and algorithmic mathematics for logic is so important also for steering a clear course in a time of frequent new and fancy catch words that may suggest that logical clarity and brilliance is not any more relevant in a time of intelligent machines.

In 1979, in contrast to the usual analysis/linear algebra approach, I dared to give an introduction to mathematics for first semester computer science students which was nothing else than a practical introduction to predicate logic as a working language and a unified frame for proving and programming. Over the years, many of my students shared this view on the fundamental theoretical and practical importance of logic for mathematics and informatics and did remarkable work developing ideas and tools for supporting this kind of thinking. Wolfgang Schreiner embarked on this type of research, teaching, and software development already in the mid-nineties and, over the years, accumulated enormous know-how and produced impressive and extensive teaching material and software tools for the theoretical foundation and the practical application of logic in mathematics and computer science, notably in mathematics and computer science teaching.

Now, he presents this enormous amount of work in a coherent book. I think there is hardly any other book that combines the foundation of logic, the applications of logic in computer science, and software for logic in an equally rich and comprehensive way. I wish the book a wide distribution. Given the outstanding didactic qualification of Wolfgang Schreiner, I am sure that the book will be extremely helpful for students of mathematics and computer science to get a profound training of the thinking technology that is in the center of the present age and will stay and become even more important in the next turns of the spiral of innovation.

It is also a special pleasure for me that the book appears in the RISC book series on symbolic computation with the Springer Verlag whose yellow books lured me into the field of (algorithmic) logic so many years ago. When I founded the RISC book series in 1993, for some reason, we decided that the cover should be gray. However, the contents of the books in this series were very much yellow all the time. It is great to see that, since Peter Paule took over the editorship and is giving enormous drive to the series, yellow is taking over also on the covers.