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 *

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, *On the system CL12
of computability logic*. ** Logical Methods in
Computer Science **11
(2015), Issue 3, paper 1, pp.1-71.

Official journal version (free access)

Significantly strengthens the results of [21] on the adequacy of

26.G.Japaridze, *Introduction
to clarithmetic II. *** Information and Computation**
(to appear). 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.

27.G.Japaridze, ** Build your
own clarithmetic I** (under review). 49
pages.

Official journal version Online preprint

Introduces a scheme of clarithmetical systems. Tuning its parameters in a “mechanical” manner, one obtains particular clarithmetical theories for a very broad range of target computational tricomplexities, i.e. combinations of time, space and amplitude complexities. Published in two parts for technical reasons.

28.G.Japaridze, ** Build your
own clarithmetic II** (under review). 50
pages.

Official journal version Online preprint

Continuation/completion of [27].

**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**11 (2015), Issue 1, Paper 12, pp.1-16.

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

- Y.Zhang,

“**Time and Space Complexity Analysis for the System CL2 of Computability Logic**”.

MS Thesis. Shandong University, 2013. - 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. - W.Xu,

“**On Some Operators and Systems of Computability Logic**”.

PhD Thesis. Xidian University, 2012. - 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)

· Villanova professor honored for research (Philadelphia Inquirer article)

· 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