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** 247
(2016), pp.290-312.

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.*W.Xu**,*

**A cirquent calculus system with clustering and ranking**”.

Journal of Applied Logic 16 (2016), pp.37-49.

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