Computability logic is a formal theory of computability, introduced by Japaridze in 2003. That is in the same sense as classical logic is a formal theory of truth. While the central semantic concept in classical logic is (Tarskian) truth, computability logic is based on a concept of computability. The formulas of classical logic represent propositions or predicates; in computability logic they represent computational problems or, equivalently, computational resources. While validity in classical logic means being "always true", in computability logic it means being "always computable". The classical concept of truth turns out to be a special case of computability (as it is understood in computability logic). Hence classical logic is a special fragment of computability logic.
Computational problems/resources are understood in their most general - interactive sense. They are formalized as games played by a machine against the environment, with computability meaning existence of a machine that wins the game against any possible behavior by the environment. Defining, in precise terms, what such a game-playing machine means, computability logic provides a generalization of the Church-Turing thesis to the interactive level.
Computability logic is a conservative extension of classical logic and, being more expressive, constructive and computationally meaningful, it has a wide range of application areas. Those, besides theory of computation, include constructive applied systems, knowledge base systems, systems for planning and action. Besides classical logic, intuitionistic and linear logics (understood in a relaxed sense) also turn out to be natural fragments of computability logic.
Computability logic is an attempt to lay foundations for a comprehensive and systematic theory of interactive computation. By turning logic from a theory of truth into a theory of computability, it brings these two disciplines closer together.
