Computability logic: A formal theory of interaction

Abstract

Generalizing the traditional concepts of predicates and their truth to interactive computational problems and their effective solvability, computability logic conservatively extends classical logic to a formal theory that provides a systematic answer to the question of what and how can be computed, just as traditional logic is a systematic tool for telling what is true. The present chapter contains a comprehensive yet relatively compact overview of this very recently introduced framework and research program. It is written in a semitutorial style with general computer science, logic and mathematics audiences in mind. © 2006 Springer-Verlag Berlin Heidelberg.