Computability logic

Introduced by Giorgi Japaridze in 2003, computability logic is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth. In this approach logical formulas represent computational problems (or, equivalently, computational resources), and their validity means being "always computable".

Computational problems and resources are understood in their most general - interactive sense. They are formalized as games played by a machine against its environment, and computability means existence of a machine that wins the game against any possible behavior by the environment. Defining what such game-playing machines mean, computability logic provides a generalization of the Church-Turing thesis to the interactive level.

The classical concept of truth turns out to be a special, zero-interactivity-degree case of computability. This makes classical logic a special fragment of computability logic. Being a conservative extension of the former, computability logic is, at the same time, by an order of magnitude more expressive, constructive and computationally meaningful. Providing a systematic answer to the fundamental question "what (and how) can be computed?", it has a wide range of potential application areas. Those include constructive applied theories, knowledge base systems, systems for planning and action.

Besides classical logic, linear logic (understood in a relaxed sense) and intuitionistic logic also turn out to be natural fragments of computability logic. Hence meaningful concepts of "intuitionistic truth" and "linear-logic truth" can be derived from the semantics of computability logic.

Being semantically constructed, as yet computability logic does not have a fully developed proof theory. Finding deductive systems for various fragments of it and exploring their syntactic properties is an area of ongoing research.

Literature

M. Bauer, A PSPACE-complete first order fragment of computability logic. ACM Transactions on Computational Logic 15 (2014), No 1, Article 1, 12 pages.
M. Bauer, The computational complexity of propositional cirquent calculus. Logical Methods is Computer Science 11 (2015), Issue 1, Paper 12, pages 1-16.
G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
G. Japaridze, Propositional computability logic I. ACM Transactions on Computational Logic 7 (2006), pages 302-330.
G. Japaridze, Propositional computability logic II. ACM Transactions on Computational Logic 7 (2006), pages 331-362.
G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532. Prepublication
G. Japaridze, Computability logic: a formal theory of interaction. Interactive Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds. Springer Verlag, Berlin 2006, pages 183-223. Prepublication
G. Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pages 100-135.
G. Japaridze, From truth to computability II. Theoretical Computer Science 379 (2007), pages 20–52.
G. Japaridze, Intuitionistic computability logic. Acta Cybernetica 18 (2007), pages 77–113.
G. Japaridze, The logic of interactive Turing reduction. Journal of Symbolic Logic 72 (2007), pages 243-276. Prepublication
G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187-227.
G. Japaridze, Cirquent calculus deepened. Journal of Logic and Computation 18 (2008), No.6, pp. 983–1028.
G. Japaridze, Sequential operators in computability logic. Information and Computation 206 (2008), No.12, pp. 1443–1475. Prepublication
G. Japaridze, Many concepts and two logics of algorithmic reduction. Studia Logica 91 (2009), No.1, pp. 1–24. Prepublication
G. Japaridze, In the beginning was game semantics. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249–350. Prepublication
G. Japaridze, Towards applied theories based on computability logic. Journal of Symbolic Logic 75 (2010), pp. 565–601.
G. Japaridze, Toggling operators in computability logic. Theoretical Computer Science 412 (2011), pp. 971-1004. Prepublication
G. Japaridze, From formulas to cirquents in computability logic. Logical Methods in Computer Science 7 (2011), Issue 2 , Paper 1, pp. 1-55.
G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312-1354. Prepublication
G. Japaridze, Separating the basic logics of the basic recurrences. Annals of Pure and Applied Logic 163 (2012), pp. 377-389. Prepublication
G. Japaridze, A logical basis for constructive systems. Journal of Logic and Computation 22 (2012), pp. 605-642.
G. Japaridze, A new face of the branching recurrence of computability logic. Applied Mathematics Letters 25 (2012), 1585-1589. Prepublication
G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173-212. Prepublication
G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part II. Archive for Mathematical Logic 52 (2013), pp. 213-259. Prepublication
G. Japaridze, Introduction to clarithmetic III. Annals of Pure and Applied Logic 165 (2014), 241-252. Prepublication
G. Japaridze, On the system CL12 of computability logic . Logical Methods is Computer Science 11 (2015), Issue 3, paper 1, pp. 1-71.
G. Japaridze, Introduction to clarithmetic II. Information and Computation 247 (2016), pp. 290-312.
G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1-59.
G. Japaridze, Build your own clarithmetic II: Soundness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 12, pp. 1-62.
K. Kwon, Expressing algorithms as concise as possible via computability logic. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, v. E97-A (2014), pp. 1385-1387.
X. Li and J. Liu, Research on decidability of CoL2 in computability logic. Computer Science 42 (2015), No 7, pp. 44-46.
I. Mezhirov and N. Vereshchagin, On abstract resource semantics and computability logic. Journal of Computer and System Sciences 76 (2010), pp. 356–372.
M. Qu, J. Luan, D. Zhu and M. Du, On the toggling-branching recurrence of computability logic. Journal of Computer Science and Technology 28 (2013), pp. 278-284.
N. Vereshchagin, Japaridze's computability logic and intuitionistic propositional calculus. Moscow State University, 2006.
W. Xu and S. Liu, The countable versus uncountable branching recurrences in computability logic. Journal of Applied Logic 10 (2012), pp. 431-446.
W. Xu and S. Liu, Soundness and completeness of the cirquent calculus system CL6 for computability logic. Logic Journal of the IGPL 20 (2012), pp. 317-330.
W. Xu and S. Liu, The parallel versus branching recurrences in computability logic. Notre Dame Journal of Formal Logic 54 (2013), pp. 61-78.
W. Xu, A propositional system induced by Japaridze’s approach to IF logic. Logic Journal of the IGPL 22 (2014), pp. 982-991
W. Xu, A cirquent calculus system with clustering and ranking. Journal of Applied Logic 16 (2016), pp. 37-49.

Computability logic

Literature

External links

See also