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

Papers 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.*H.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.

**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
- Proofs as games
- Computability logic-1
- 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: გამოთვლადობის ლოგიკა, §§à§Ô§Ú§Ü§Ñ
§Ó§í§é§Ú§ã§Ý§Ú§Þ§à§ã§ä§Ú, ¿É¼ÆËãÐÔÂß¼, 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, Calculus of structures, Peano
arithmetic, Implicit computational complexity