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.

What is Computability Logic?

Lecture
notes on Computability Logic

Potential applications of Computability Logic

Selected papers on Computability Logic by Japaridze

Selected papers on Computability Logic by other authors

PhD theses, MS theses and externally funded
projects on Computability Logic

Links to related websites

LaTeX macros
for the operators of Computability Logic

**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

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.

Official journal version (free access)

Elaborates a deep version (as opposed to the shallow version of [4]) of Cirquent Calculus for the (

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:

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

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

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.

Official journal version (free access)

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

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

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

24.G.Japaridze,* Introduction
to clarithmetic III.*

Official journal version Online preprint

In the style of [18,25], introduces systems for

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:**

*I.Mezhirov and N.Vereshchagin*,.

¡°On abstract resource semantics and computability logic¡±

Journal of Computer and Systems Sciences 76 (2010), pp. 356-372.*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.*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.*W.Xu and S.Liu*,

**The parallel versus branching recurrences in computability logic**¡±.

Notre Dame Journal of Formal Logic 54 (2013), pp. 61-78.*M.Bauer,*

**A PSPACE-complete first order fragment of computability logic**¡±.

**ACM Transactions on Computational Logic**15 (2014), No 1, Article 1, 12 pages.*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.*W.Xu,*

**A propositional system induced by Japaridze¡¯s approach to IF logic**¡±.

Logic Journal of the IGPL (in press), 2014.*M.Bauer,*

**The computational complexity of propositional cirquent calculus**¡±.

**Logical Methods is Computer Science**(in press), 2014.

**PhD**** theses, MS theses and
externally funded projects on Computability Logic:**

1. M.Qu,
¡°**Research on
the toggling-branching recurrence of Computability Logic**¡±.

PhD Thesis. Shandong University, 2014.

2. Y.Zhang,

¡°**Time and Space
Complexity Analysis for the System CL2 of Computability Logic**¡±.

MS Thesis. Shandong University, 2013.

3. W.Xu,

¡°**A Study of
Cirquent Calculus Systems for Computability Logic**¡±.

Research proposal funded by the National Science Foundation of China (61303030)
and the Fundamental Research Funds for the Central Universities of China
(K50513700). Xidian University,
2013-2016.

4. W.Xu,

¡°**On Some
Operators and Systems of Computability Logic**¡±.

PhD Thesis. Xidian University, 2012.

5. G.Japaridze,

¡°**A Logical Study
of Interactive Computational Problems Understood as Games**¡±.

Research proposal funded by the National Science Foundation of US
(CCR-0208816). Villanova University, 2002-2006.

**Other websites on computability logic:**

¡¤ Game Semantics or Linear Logic?

¡¤ Course on Computability Logic --- taught in 2007. Includes lecture notes in PowerPoint.

**Links
to related websites:**

¡¤ Logic and Games (Stanford Encyclopedia of Philosophy)

¡¤ Deep Inference and the Calculus of Structures

¡¤ Lambda the Ultimate: Introduction to computability logic

¡¤ Lambda the Ultimate: In the beginning was game semantics

¡¤ On abstract resource semantics and computabilty logic (video lecture by N.Vereshchagin)

¡¤ Mathematical Logic around the World

**Keywords:** გამოთვლადობის ლოგიკა, §§à§Ô§Ú§Ü§Ñ
§Ó§í§é§Ú§ã§Ý§Ú§Þ__§à§ã§ä§Ú__, ¿É¼ÆËãÐÔÂß¼, cirquent calculus, Game semantics, Resource
semantics, Linear logic, Intuitionistic logic, Constructive logics,
Interaction, Interactive computation, Knowledge representation, Knowledgebase
systems, Resourcebase systems, Systems for planning and action, Computational
logic, Deep inference, Peano arithmetic, Implicit computational complexity