可计算性逻辑

相对于是真理的形式理论的经典逻辑，在2003年发明的可计算性逻辑()是把逻辑恢复为系统的形式的可计算性理论的一个研究程序和数学框架。在这种方法下逻辑公式表示计算问题（或等价的计算资源），而它们的有效性意味着"总是可计算的"。

计算问题和资源的理解是在它们最一般的意义上的 - 交互的意义上的。它们被形式化为机器扮演的针对它的环境的游戏，而可计算性意味着存在着一个机器针对经由环境的任何可能行为赢得了游戏。定义了这种游戏扮演机器所意味的东西，可计算性逻辑在交互层面提供了邱奇-图灵论题的一般化。

真理的经典概念转变为可计算性的特殊的零交互度的情况。这使经典逻辑成为可计算性逻辑的特殊片段。作为前者的保守扩展的同时，可计算性逻辑有着一个数量级之上的表达力、创造性和计算意义。提供了对基本问题"什么是可以（如何）计算的?"的系统的回答，它有潜在的广泛的应用领域。其中包括构造性应用理论，知识库系统，计划和行动系统。

除了经典逻辑之外，线性逻辑（在不严格的意义上理解）和直觉逻辑也转变成可计算性逻辑的自然片段了。因为"直觉真理"和"线性逻辑真理"的有意义的概念可从可计算性逻辑的语义中推导出来。

正在做着语义构造，至今可计算性逻辑仍没有完全开发出证明论。为它的各种片段找到演绎系统并探索它们的性质是正在研究中的领域。

参见
*可计算性的逻辑
*博弈语义
*交互计算

• 直觉主义
• BHK释义
• 直觉类型论
• 经典逻辑
• 中间逻辑
• 线性逻辑
• 构造性证明
• Curry-Howard对应
• 博弈语义

參考文獻
G. Japaridze, [http://www.sciencedirect.com/science/article/pii/S016800720300023X Introduction to computability logic] *. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
G. Japaridze, [http://portal.acm.org/citation.cfm?id=1131313.1131318&coll=portal&dl=ACM&idx=1131313&part=periodical&WantType=periodical&title=ACM%20Transactions%20on%20Computational%20Logic%20%28TOCL%29&CFID=71203179&CFTOKEN=21225900 Propositional computability logic I]*. ACM Transactions on Computational Logic 7 (2006), pages 302-330.
G. Japaridze, [http://portal.acm.org/citation.cfm?id=1131313.1131319&coll=portal&dl=ACM&idx=1131313&part=periodical&WantType=periodical&title=ACM%20Transactions%20on%20Computational%20Logic%20%28TOCL%29&CFID=71203179&CFTOKEN=21225900 Propositional computability logic II]*. ACM Transactions on Computational Logic 7 (2006), pages 331-362.
G. Japaridze, [http://logcom.oxfordjournals.org/cgi/content/abstract/16/4/489 Introduction to cirquent calculus and abstract resource semantics] *. Journal of Logic and Computation 16 (2006), pages 489-532.
G. Japaridze, [http://www.springerlink.com/content/l10m555830730182/ 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, [https://web.archive.org/web/20070519230525/http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V1G-4JS1M3B-1&_user=10&_handle=V-WA-A-W-AD-MsSAYWA-UUA-U-AACVWWCADC-AACAYUCEDC-EDADUYDDA-AD-U&_fmt=summary&_coverDate=07%2F25%2F2006&_rdoc=8&_orig=browse&_srch=%23toc%235674%232006%23996429998%23626672!&_cdi=5674&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=8f62c93dd24dd2c3f48cf7c77e05228d From truth to computability I]*. Theoretical Computer Science 357 (2006), pages 100-135.
G. Japaridze, [http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V1G-4MV758R-2&_user=1536200&_coverDate=01%2F17%2F2007&_alid=540937878&_rdoc=1&_fmt=summary&_orig=search&_cdi=5674&_sort=d&_docanchor=&view=c&_ct=2&_acct=C000053374&_version=1&_urlVersion=0&_userid=1536200&md5=ce039afe954def15cbd8e9438488f011 From truth to computability II]*. Theoretical Computer Science 379 (2007), pages 20–52.
G. Japaridze, [https://web.archive.org/web/20171017112707/http://www.inf.u-szeged.hu/actacybernetica/edb/vol18n1/Japaridze_2007_ActaCybernetica.xml Intuitionistic computability logic]*. Acta Cybernetica 18 (2007), pages 77–113.
G. Japaridze, [https://web.archive.org/web/20150628201840/http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.jsl%2F1174668394 The logic of interactive Turing reduction]*. Journal of Symbolic Logic 72 (2007), pages 243-276.
G. Japaridze, [http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6TYB-4NSWYVP-1&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_version=1&_urlVersion=0&_userid=10&md5=3a7cf451f14038839aba1d27bd89393f The intuitionistic fragment of computability logic at the propositional level]*. Annals of Pure and Applied Logic 147 (2007), pages 187-227.
G. Japaridze, [https://archive.today/20130415174625/http://logcom.oxfordjournals.org/cgi/content/abstract/exn019 Cirquent calculus deepened]*. Journal of Logic and Computation 18 (2008), No.6, pp. 983–1028.
G. Japaridze, [http://clx.doi.org/10.1016/j.ic.2008.10.001 Sequential operators in computability logic]*. Information and Computation 206 (2008), No.12, pp. 1443–1475.
G. Japaridze, [http://www.springerlink.com/content/04t6780731373n13/ Many concepts and two logics of algorithmic reduction]*. Studia Logica 91 (2009), No.1, pp. 1–24.
G. Japaridze, [https://archive.today/20130203153059/http://www.springerlink.com/content/m022011617448676/?p=a62bebfc0dec4164a3a3ba90fefb86aa&pi=10 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, [https://web.archive.org/web/20150629001449/http://projecteuclid.org/DPubS?verb=Display&version=1.0&service=UI&handle=euclid.jsl%2F1268917495&page=record Towards applied theories based on computability logic]*. Journal of Symbolic Logic 75 (2010), pp. 565-601.
I. Mezhirov and N. Vereshchagin, [http://portal.acm.org/citation.cfm?id=1808347.1808575 On abstract resource semantics and computability logic]*. Journal of Computer and System Sciences 76 (2010), pp. 356-372.
N. Vereshchagin, [https://web.archive.org/web/20160303185501/http://lpcs.math.msu.su/~ver/papers/japaridze.ps Japaridze's computability logic and intuitionistic propositional calculus]*. Moscow State University, 2006.

外部链接
*[https://web.archive.org/web/20110411024825/http://www.cis.upenn.edu/~giorgi/cl.html Computability Logic Homepage]
[https://web.archive.org/web/20190419120954/http://www.csc.villanova.edu/~japaridz/ Giorgi Japaridze][https://web.archive.org/web/20160303174250/http://www.csc.villanova.edu/~japaridz/CL/gsoll.html Game Semantics or Linear Logic?]
*[http://www.csc.villanova.edu/~japaridz/CL/clx.html 可计算性逻辑课程]