All references in this article are exclusively by a single author, G. Japaridze. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources. Find sources: "Computability logic" – news · newspapers · books · scholar · JSTOR(May 2020)
Computability logic (CoL) is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic, which is a formal theory of truth. It was introduced and so named by Giorgi Japaridze in 2003.[1]
In classical logic, formulas represent true/false statements. In CoL, formulas represent computational problems. In classical logic, the validity of a formula depends only on its form, not on its meaning. In CoL, validity means being always computable. More generally, classical logic tells us when the truth of a given statement always follows from the truth of a given set of other statements. Similarly, CoL tells us when the computability of a given problem A always follows from the computability of other given problems B1,...,Bn. Moreover, it provides a uniform way to actually construct a solution (algorithm) for such an A from any known solutions of B1,...,Bn.
CoL formulates computational problems in their most general—interactive—sense. CoL defines a computational problem as a game played by a machine against its environment. Such a problem is computable if there is a machine that wins the game against every possible behavior of the environment. Such a game-playing machine generalizes the Church–Turing thesis to the interactive level. The classical concept of truth turns out to be a special, zero-interactivity-degree case of computability. This makes classical logic a special fragment of CoL. Thus CoL is a conservative extension of classical logic. Computability logic is more expressive, constructive and computationally meaningful than classical logic. Besides classical logic, independence-friendly (IF) logic and certain proper extensions of linear logic and intuitionistic logic also turn out to be natural fragments of CoL.[2][3] Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL.
CoL systematically answers the fundamental question of what can be computed and how; thus CoL has many applications, such as constructive applied theories, knowledge base systems, systems for planning and action. Out of these, only applications in constructive applied theories have been extensively explored so far: a series of CoL-based number theories, termed "clarithmetics", have been constructed[4][5] as computationally and complexity-theoretically meaningful alternatives to the classical-logic-based first-order Peano arithmetic and its variations such as systems of bounded arithmetic.
Traditional proof systems such as natural deduction and sequent calculus are insufficient for axiomatizing nontrivial fragments of CoL. This has necessitated developing alternative, more general and flexible methods of proof, such as cirquent calculus.[6][7]
^ G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99. doi:10.1016/S0168-0072(03)00023-X
^G. Japaridze, In the beginning was game semantics?. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249–350. doi:10.1007/978-1-4020-9374-6_11 Prepublication
^G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187–227. doi:10.1016/j.apal.2007.05.001
^G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312–1354. doi:10.1016/j.ic.2011.07.002 Prepublication
^G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods in Computer Science 12 (2016), Issue 3, paper 8, pp. 1–59.
^G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489–532. doi:10.1093/logcom/exl005 Prepublication
^G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173–212. doi:10.1007/s00153-012-0313-8 Prepublication
and 27 Related for: Computability logic information
Computabilitylogic (CoL) is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed...
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated...
(also known as computability theory). Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their...
Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic...
Logics for computability are formulations of logic that capture some aspect of computability as a basic notion. This usually involves a mix of special...
Japaridze is best known for his invention of computabilitylogic, cirquent calculus, and Japaridze's polymodal logic. During 1985–1988 Japaridze elaborated...
of mathematical logic topics. For traditional syllogistic logic, see the list of topics in logic. See also the list of computability and complexity topics...
Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in...
Walter A. Carnielli (2000). Computability: Computable Functions, Logic, and the Foundations of Mathematics, with Computability: A Timeline (2nd ed.). Wadsworth/Thomson...
hard- and easy-play machines elaborated within the framework of computabilitylogic, Dina Q. Goldin's Persistent Turing Machines (PTMs), and Yuri Gurevich's...
theory, and computability theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic. However, it...
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion...
logic, whose formal development is somewhat standard (see first-order logic and higher-order logic). Philosophy portal Chu spaces Computabilitylogic...
In quantum computing and specifically the quantum circuit model of computation, a quantum logic gate (or simply quantum gate) is a basic quantum circuit...
Tarski "changed the face of logic in the twentieth century". Alonzo Church and Alan Turing proposed formal models of computability, giving independent negative...
each producing output data from given input data. Computability theory, which studies computability of functions from inputs to outputs, and for which...
This is a list of computability and complexity topics, by Wikipedia page. Computability theory is the part of the theory of computation that deals with...
v t e Logic of Computable Functions (LCF) is a deductive system for computable functions proposed by Dana Scott in 1969 in a memorandum unpublished until...
proof theory capable of "taming" various nontrivial fragments of his computabilitylogic, which had otherwise resisted all axiomatization attempts within...
rule Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Computability and logic. Cambridge: Cambridge University Press. p. 364. ISBN 978-0-521-87752-7...
Fuzzy logic is a form of many-valued logic in which the truth value of variables may be any real number between 0 and 1. It is employed to handle the concept...
this property that is referred to as charge recovery logic, adiabatic circuits, or adiabatic computing (see Adiabatic process). Although in practice no nonstationary...
Macmillan Publishing Co., ISBN 0-02-324880-7 Boolos, Burgess, Jeffrey. Computability and Logic, 4th Ed, Cambridge, 2002. Wiktionary has definitions related to...
organizations, clubs and societies of both a formal and informal nature. Computability theory Computer security Glossary of computer hardware terms History...
Global Information