Computability logic

From Wikipedia, the free encyclopedia

Introduced by Giorgi Japaridze in 2003, computability logic is a research programme and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of proof. In this approach logical formulas represent computational problems (or, equivalently, computational resources), and their validity means being "always computable".

Computational problems and resources are understood in their most general - interactive sense. They are formalized as games played by a machine against its environment, and computability means existence of a machine that wins the game against any possible behavior by the environment. Defining what such game-playing machines mean, computability logic provides a generalization of the Church-Turing thesis to the interactive level.

The classical concept of truth turns out to be^{[citation needed]} a special, zero-interactivity-degree case of computability. This makes classical logic a special fragment of computability logic. Being a conservative extension of the former, computability logic is, at the same time, by an order of magnitude more expressive, constructive and computationally meaningful. Providing a systematic answer to the fundamental question "what (and how) can be computed?", it has a wide range of potential application areas. Those include constructive applied theories, knowledge base systems, systems for planning and action.

Besides classical logic, linear logic (understood in a relaxed sense) and intuitionistic logic also turn out to be natural fragments of computability logic. Hence meaningful concepts of "intuitionistic truth" and "linear-logic truth" can be derived from the semantics of computability logic.

Being semantically constructed, as yet computability logic does not have a fully developed proof theory. Finding deductive systems for various fragments of it and exploring their syntactic properties is an area of ongoing research.

References

G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.

G. Japaridze, Propositional computability logic I. ACM Transactions on Computational Logic 7 (2006), pages 302-330.

G. Japaridze, Propositional computability logic II. ACM Transactions on Computational Logic 7 (2006), pages 331-362.

G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532.

G. Japaridze, Computability logic: a formal theory of interaction. Interactive Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds. Springer Verlag, Berlin 2006, pages 183-223.

G. Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pages 100-135.

G. Japaridze, From truth to computability II. Theoretical Computer Science 379 (2007), pages 20–52.

G. Japaridze, Intuitionistic computability logic. Acta Cybernetica 18 (2007), pages 77–113.

G. Japaridze, The logic of interactive Turing reduction. Journal of Symbolic Logic 72 (2007), pages 243-276.

G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187-227.

G. Japaridze, Cirquent calculus deepened. Journal of Logic and Computation 18 (2008), No.6, pp. 983–1028.

G. Japaridze, Sequential operators in computability logic. Information and Computation 206 (2008), No.12, pp. 1443–1475.

G. Japaridze, Many concepts and two logics of algorithmic reduction. Studia Logica 91 (2009), No.1, pp. 1–24.

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.

G. Japaridze, Towards applied theories based on computability logic. Journal of Symbolic Logic 75 (2010), pp. 565-601.

I. Mezhirov and N. Vereshchagin, On abstract resource semantics and computability logic. Journal of Computer and System Sciences 76 (2010), pp. 356-372.

N. Vereshchagin, Japaridze's computability logic and intuitionistic propositional calculus. Moscow State University, 2006.

External links

Academic areas	Argumentation theory Axiology Critical thinking Computability theory Formal semantics History of logic Informal logic Logic in computer science Mathematical logic Mathematics Metalogic Metamathematics Model theory Philosophical logic Philosophy Philosophy of logic Philosophy of mathematics Proof theory Set theory

Foundations	Abduction Analytic truth Antinomy A priori Deduction Definition Description Induction Inference Logical form Logical consequence Logical truth Name Necessity Meaning Paradox Possible world Presupposition Probability Reason Reasoning Reference Semantics Statement Strict implication Substitution Syntax Truth Truth value Validity

Philosophical logic

Critical thinking Informal logic	Analysis Ambiguity Argument Belief Bias Credibility Evidence Explanation Explanatory power Fact Fallacy Inquiry Opinion Parsimony Premise Propaganda Prudence Reasoning Relevance Rhetoric Rigor Vagueness

Theories of deduction	Constructivism Dialetheism Fictionalism Finitism Formalism Intuitionism Logical atomism Logicism Nominalism Platonic realism Pragmatism Realism

Metalogic Metamathematics

Cantor's theorem Church's theorem Church's thesis Consistency Effective method Foundations of mathematics Gödel's completeness theorem Gödel's incompleteness theorems Soundness Completeness Decidability Interpretation Löwenheim–Skolem theorem Metatheorem Satisfiability Independence Type–token distinction Use–mention distinction

Mathematical logic

General	Formal language Formation rule Formal system Deductive system Formal proof Formal semantics Well-formed formula Set Element Class Classical logic Axiom Natural deduction Rule of inference Relation Theorem Logical consequence Axiomatic system Type theory Symbol Syntax Theory

Traditional logic	Proposition Inference Argument Validity Cogency Syllogism Square of opposition Venn diagram

Propositional calculus Boolean logic	Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables

Predicate logic	First-order Quantifiers Predicate Second-order Monadic predicate calculus

Set theory	Set Empty set Enumeration Extensionality Finite set Function Subset Power set Countable set Recursive set Domain Range Ordered pair Uncountable set

Model theory	Model Interpretation Non-standard model Finite model theory Truth value Validity

Proof theory	Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax

Computability theory	Recursion Recursive set Recursively enumerable set Decision problem Church–Turing thesis Computable function Primitive recursive function

Non-classical logic

Modal logic	Alethic Axiologic Deontic Doxastic Epistemic Temporal

Intuitionism	Intuitionistic logic Constructive analysis Heyting arithmetic Intuitionistic type theory Constructive set theory

Fuzzy logic	Degree of truth Fuzzy rule Fuzzy set Fuzzy finite element Fuzzy set operations

Substructural logic	Structural rule Relevance logic Linear logic

Paraconsistent logic	Dialetheism

Description logic	Ontology Ontology language

Many-valued logic	Three-valued logic Four-valued logic Łukasiewicz logic

Logicians

Lists

Topics	Index of logic articles Mathematical logic Boolean algebra Set theory

Other	Logicians Rules of inference Paradoxes Fallacies Logic symbols

Common logical symbols

& ∨ ¬ ~ → ⊃ ≡ \| ∀ ∃ ⊤ ⊥ ⊢ ⊨ ∴ ∵

Portal
Category
Outline
WikiProject
Talk
changes

This article is issued from Wikipedia. The text is available under the Creative Commons Attribution/Share Alike; additional terms may apply for the media files.

Computability logic

References

External links

See also