可计算性逻辑
维基百科，自由的百科全书
相对于是真理的形式理论的经典逻辑，Giorgi Japaridze 在 2003 年发明的可计算性逻辑是把逻辑恢复为系统的形式的可计算性理论的一个研究程序和数学框架。在这种方法下逻辑公式表示计算问题(或等价的计算资源)，而它们的有效性意味着"总是可计算的"。
计算问题和资源的理解是在它们最一般的意义上的 - 交互的意义上的。它们被形式化为机器扮演的针对它的环境的游戏，而可计算性意味着存在着一个机器针对经由环境的任何可能行为赢得了游戏。定义了这种游戏扮演机器所意味的东西，可计算性逻辑在交互层面提供了邱奇-图灵论题的一般化。
真理的经典概念转变为可计算性的特殊的零交互度的情况。这使经典逻辑成为可计算性逻辑的特殊片段。作为前者的保守扩展的同时，可计算性逻辑有着一个数量级之上的表达力、创造性和计算意义。提供了对基本问题 "什么是可以(如何)计算的?" 的系统的回答，它有潜在的广泛的应用领域。其中包括构造性应用理论，知识库系统，计划和行动系统。
除了经典逻辑之外，线性逻辑(在不严格的意义上理解)和直觉逻辑也转变成可计算性逻辑的自然片段了。因为"直觉真理"和"线性逻辑真理"的有意义的概念可从可计算性逻辑的语义中推导出来。
正在做着语义构造，至今可计算性逻辑仍没有完全开发出证明论。为它的各种片段找到演绎系统并探索它们的性质是正在研究中的领域。
[编辑] 参见
- G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1-99.
- G. Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pages 100-135.
- G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532.
[编辑] 外部链接
[编辑] 参见
- 可计算性的逻辑
- 博弈语义
- 交互计算
