Giorgi Japaridze's  page for

Computability Logic*

(CoL)

* This material is based upon work supported by the National Science Foundation under Grant No. 0208816. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

A list of open problems

What is Computability Logic? Computability is certainly one of the most interesting and fundamental concepts in mathematics and computer science, and it would be more than natural to ask what logic it induces. Let us face it: this question has not only never been answered, but never even been asked within a reasonably coherent and comprehensive formal framework. This is where Computability Logic (CoL) comes in. It is a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader and more proper sense, Computability Logic is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme "from truth to computability". It was introduced in 2003 and, at present, still remains in its infancy stage, with open problems prevailing over answered questions. It is largely a virgin soil offering plenty of research opportunities, with good chances of interesting findings, for those with interests in logic and its applications in computer science.

Computation and computational problems in Computability Logic are understood in their most general, interactive sense, and are precisely seen as games played by a machine (computer, agent, robot) against its environment (user, nature, or the devil himself). Computability of such problems means existence of a machine that always wins the game. Logical operators stand for operations on computational problems, and validity of a logical formula means being a scheme of "always computable" problems.

Remarkably, classical, intuitionistic and linear (in a broad sense) logics turn out to be three natural fragments of Computability Logic. This is no accident. The classical concept of truth is nothing but a special case of computability -- computability restricted to problems of zero interactivity degree. Correspondingly, classical logic is nothing but a special fragment of Computability Logic. One of the main -- so far rather abstract -- intuitions associated with intuitionistic logic is that it must be a logic of problems (Kolmogorov 1932); this is exactly what computability logic is, only in a much more expressive language than intuitionistic logic. And one of the main -- again, so far rather abstract -- claims of linear logic is that it is a logic of resources. Reversing of the roles of the machine and its environment turns computational problems into computational resources, which makes Computability Logic a logic of resources, only, again, in a more expressive language than that of linear logic, and based on an intuitively convincing and mathematically strict resource semantics rather than some naive philosophy and unreliable syntactic arguments. For more about Computability Logic vs. linear logic, visit Game Semantics or Linear Logic?.

For an extended online tutorial introduction to the subject please see Lecture Notes on Computability Logic.

Potential applications of Computability Logic: The Computability Logic paradigm is not only about "what can be computed", but equally about "how can be computed". This opens application areas far beyond pure computation theory, such as:

• Knowledgebase systems. Computability Logic is an appealing alternative to the traditional knowledge base, knowledge representation and query logics. Its advantages include:
• Computability Logic is a logic of interaction, and this is what a good knowledgebase logic needs to be. After all, most of the real knowledgebase and information systems are interactive.
• Computability Logic is resource-conscious: the potential knowledge provided by a disposable pregnancy test device is knowledge of only one (even though an arbitrary one) woman's pregnancy status, but not two. Computability Logic naturally captures this sort of extremely relevant differences while the traditional systems fail to account for them.
• Computability Logic naturally differentiates between truth and an agent's actual ability to find/compute/tell what is true. To achieve similar effects, traditional knowledgebase logics have to appeal to the controversial, messy and troublemaking epistemic constructs.
• Systems for planning and action. Computability Logic might be a reasonable alternative to the traditional AI planning logics. Its advantages include:
• Computability Logic is a logic of interaction, and planning systems should be well able to account for an agent's interaction with the environment.
• A good planning logic should be able to naturally account for the fact that with one ballistic missile one can destroy only one (even though an arbitrary one) target but not two. The resource-conscious Computability Logic fits the bill.
• Computability Logic is a logic of knowledge and informational resources, which automatically takes care of the knowledge preconditions problem.
• Computability-Logic-based planning systems are immune to the notorious frame problem.
• Constructive applied theories. Computability Logic is a conservative extension of classical logic, which makes it a reasonable alternative to the latter in its most traditional and unchallenged application areas. In particular, it makes perfect sense to base applied theories (such as, say, Peano arithmetic) on Computability Logic instead of classical logic. The advantages of doing so include that Computability-Logic-based applied theories, compared with their classical-logic-based counterparts, are:
• Expressive: the language of classical logic is only a modest fraction of the language of Computability Logic.
• Computationally meaningful: every theorem of a Computability-Logic-based theory represents a computable problem rather than just a true statement.
• Constructive: any proof of a formula F in a Computability-Logic-based theory effectively encodes a solution to the computational problem represented by F.

Selected papers on Computability Logic by Japaridze (Recommendation: For the first acquaintance with the subject, most recommended is reading the tutorial-style Sections 1-10 of "In the beginning was game semantics".)

1.  G.Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pp.1-99.
Official journal version   Online preprint
Provides a fundamental introduction to the subject. It is long but easy to read. If you decide to read it, please make sure you check out the Erratum.

2.  G.Japaridze, Propositional computability logic I. ACM Transactions on Computational Logic 7 (2006), No. 2, pp. 302-330.
Official journal version   Online preprint
Contains a detailed exposition of a soundness and completeness proof for one of the most basic fragments of Computability Logic.

3.  G.Japaridze, Propositional computability logic II. ACM Transactions on Computational Logic 7 (2006), No. 2, pp. 331-362.
Official journal version   Online preprint
Extends the soundness/completeness result of its predecessor to a much more expressive fragment of Computability Logic.

4.  G.Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), No.4, pp. 489-532.
Official journal version   Online preprint
Cirquent Calculus is a new syntactic approach, which can be seen as a refinement of sequent calculus. Unlike the latter, it is flexible enough to be used as a deductive framework for computability logic.

5.  G.Japaridze, Computability logic: a formal theory of interaction. In: Interactive Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds. Springer  2006, pp. 183-223.
Official book version      Online preprint
Presents a relatively compact and nontechnical introduction to Computability Logic and an overview of the newest results. Most recommended for those whose primary interests are in computer science. Written in a semitutorial style with non-expert audience in mind.

6.  G.Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pp. 100-135.
Official journal version   Online preprint
Proves soundness and completeness for the first-order fragment CL3 of Computability Logic, which is the predicate version of logic CL1 studied in [2].

7.  G.Japaridze, From truth to computability II. Theoretical Computer Science 379 (2007), pp. 20-52.
Official journal version   Online preprint
Extends the results of its predecessor in the same sense on the first-order level as [3] extends [2] on the propositional level.

8.  G.Japaridze, Intuitionistic computability logic. Acta Cybernetica 18 (2007), No.1, pp.77-113.
Official journal version   Online preprint
Proves soundness for Heyting's intuitionistic predicate calculus with respect to the Computability-Logic semantics.

9.  G.Japaridze, The logic of interactive Turing reduction. Journal of Symbolic Logic 72 (2007), No.1, pp. 243-276.
Official journal version   Online preprint
A proof of the completeness of the implicative fragment of Intuitionistic Logic with respect to the semantics of Computability Logic.

10.G.Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), No.3, pp.187-227.
Official journal version   Online preprint
Proof of the (soundness and) completeness of the full propositional Intuitionistic Logic with respect to the semantics of Computability Logic.

11.G.Japaridze, Cirquent calculus deepened. Journal of Logic and Computation 18 (2008), No.6, pp.983-1028.

Elaborates a deep version (as opposed to the shallow version of [4]) of Cirquent Calculus for the (Ø,Ú,Ù)-fragment of Computability Logic and classical propositional logic.

12.G.Japaridze, Sequential operators in computability logic. Information and Computation 206 (2008), No.12, pp. 1443-1475.
Official journal version   Online preprint
Introduces the new, sequential group (conjunction/disjunction, quantifiers and recurrences) of game operations. Constructs sound and complete axiomatizations.

13.G.Japaridze, In the beginning was game semantics. In: Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer  2009, pp.249-350.
Official book version    Online preprint
A comprehensive overview of the philosophy, motivations and techniques of Computability Logic. Supported by ample illustrations and examples. Contains a proof of the soundness of Affine Logic, claimed but never officially proven before.

14.G.Japaridze, Many concepts and two logics of algorithmic reduction. Studia Logica 91 (2009), No.1, pp. 1-24.
Official journal version   Online preprint
The main result here is a proof of the fact that implicative binary tautologies and their instances are precisely captured by the implicative fragment of intuitionistic calculus without contraction. This is the logic of the basic (linear) sort of reduction.

15.G.Japaridze, Towards applied theories based on computability logic. Journal of Symbolic Logic 75 (2010), pp. 565-601.
Official journal version   Online preprint
Basing Peano arithmetic on Computability Logic instead of classical logic. Built on the new sound and complete deductive system CL12 for Computability Logic, which substantially strengthens the system CL3 introduced in [6].

16.G.Japaridze, Toggling operators in computability logic. Theoretical Computer Science 412 (2011), pp. 971-1004.
Official journal version     Online preprint
Introduces the new, toggling ("trial-and-error") group of game operations (conjunction/disjunction, quantifiers and recurrences). Constructs a sound and complete axiomatization for the fragment of Computability Logic which, along with negation, has all four --- parallel, toggling, sequential and choice --- sorts of conjunctions and disjunctions.

17.G.Japaridze, From formulas to cirquents in computability logic. Logical Methods in Computer Science 7 (2011), Issue 1, Paper 1, pp. 1-55.
Official journal version (free access)
Brings cirquents into Computability Logic. Brings together computability logic and Independence-Friendly Logic.

18.G.Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312-1354.
Official journal version   Online preprint
"Clarithmetic" is a generic term for arithmetical theories based on Computability Logic. The present piece of the series devoted to clarithmetic introduces a system for polynomial time computability, based on CL12.

19.G.Japaridze, Separating the basic logics of the basic recurrences. Annals of Pure and Applied Logic 163 (2012), pp. 377-389.
Official journal version   Online preprint
Shows that, even at the most basic level (namely, in combination with only ¬,¡Ä,¡Å), the parallel, countable branching and uncountable branching recurrences of computability logic validate different sets of principles.

20.G.Japaridze, A new face of the branching recurrence of computability logic. Applied Mathematics Letters   25 (2012), pp. 1585-1589.
Official journal version   Online preprint
Introduces a new, substantially simplified version of the branching recurrence operation, and proves its equivalence to the old, ¡°canonical¡±version.

21.G.Japaridze, A logical basis for constructive systems. Journal of Logic and Computation 22 (2012), pp.605-642.

Prepares a launching ground for developing complexity-oriented applied theories based on Computability Logic, namely, system CL12.

22.G.Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I.  Archive for Mathematical Logic 52 (2013), pp. 173-212.
Official journal version   Online preprint      Author¡¯s official copy
Constructs a cirquent calculus system CL15 and proves its soundness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence.

23.G.Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part II.  Archive for Mathematical Logic 52 (2013), pp. 213-259.
Official journal version   Online preprint     Author¡¯s official copy
Proves the completeness of the system CL15 of [22] with respect to the semantics of computability logic.

24.G.Japaridze, Introduction to clarithmetic III. Annals of Pure and Applied Logic 165 (2014), pp. 241-252.
Official journal version   Online preprint
In the style of [18,25], introduces systems for PA-provably recursive time (=space) computability, constructively PA-provable computability, and (not-necessarily-constructively) PA-provable computability.

25.G.Japaridze, Introduction to clarithmetic II  (under review).  28 pages.
Official journal version   Online preprint
In the style of [18], introduces systems for polynomial space computability, elementary recursive time (=space) computability, and primitive recursive time (=space) computability.

26.G.Japaridze, On the system CL12 of computability logic  (under review).  46 pages.
Official journal version   Online preprint
Significantly strengthens the results of [21] on the adequacy of CL12.

Selected (SCI-indexed) papers on Computability Logic by other authors:

1. I.Mezhirov and N.Vereshchagin,
¡°
On abstract resource semantics and computability logic¡±
.
Journal of Computer and Systems Sciences 76 (2010), pp. 356-372.
2. W.Xu and S.Liu,
¡°The countable versus uncountable branching recurrences in computability logic¡±.
Journal of Applied Logic 10 (2012), pp. 431-446.
3. 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.
4. M.Qu, J.Luan, D.Zhu, M.Du,
¡°On the toggling-branching recurrence of computability logic¡±.
Journal of Computer Science and Technology 28 (2013), pp. 278-284.
5. W.Xu and S.Liu,
¡°The parallel versus branching recurrences in computability logic¡±.
Notre Dame Journal of Formal Logic 54 (2013), pp. 61-78.
6. M.Bauer,
¡°A PSPACE-complete first order fragment of computability logic¡±.
ACM Transactions on Computational Logic 15 (2014), No 1, Article 1, 12 pages.
7. K.Kwon,
¡°Expressing algorithms as concise as possible via computability logic¡±.
IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol. E97-A (2014), pp.1385-1387.
8. W.Xu,
¡°A propositional system induced by Japaridze¡¯s approach to IF logic¡±.
Logic Journal of the IGPL (in press), 2014.
9. M.Bauer,
¡°The computational complexity of propositional cirquent calculus¡±.
Logical Methods is Computer Science (in press), 2014.