直觉主义可计算性逻辑
计算机科学中的逻辑
2010-03-26 v3 人工智能
逻辑
摘要
可计算性逻辑（CL）是关于计算任务与资源的系统性形式理论，在某种意义上是（语法引入的）线性逻辑基于语义的替代。凭借其具表达力且灵活的语言——其中公式表示计算问题、“真”被理解为算法可解性——CL潜在地为建构性应用理论与固有需要建构性且计算有意义底层逻辑的计算系统提供全面逻辑基础。最著名的建构主义逻辑之一是Heyting直觉主义演算INT，其语言可视为CL语言的特殊片段。然而，INT的建构主义哲学从未真正找到直观可信且数学严格语义 justification。CL有充分理由提供此种 justification，从而兑现Kolmogorov著名论题“INT = 问题逻辑”。本文包含关于CL语义的INT可靠性证明。关于CL的综合在线资料见 http://www.cis.upenn.edu/~giorgi/cl.html
引用
@article{arxiv.cs/0411008,
title = {Intuitionistic computability logic},
author = {Giorgi Japaridze},
journal= {arXiv preprint arXiv:cs/0411008},
year = {2010}
}