A cirquent calculus system with clustering and ranking
循环演算是G.Japaridze为了满足其可计算逻辑理论的需要而提出的一种新的证明理论和语义方法。Japaridze的早期文章“From formulas to cirquents in computability logic”将cirquents的概念推广到了所谓的聚类和排序的版本，并表明，通过聚类和排序的cirquents，可以捕获，提炼和推广所谓的扩展IF逻辑。雅帕里泽的治疗扩展IF逻辑，但是，是纯粹的语义，并没有演绎系统提出。本文从句法上构造了一个具有聚类和排序功能的、可靠的、完备的w.r.t.基于情境的语义学的命题片段。这样一个系统不仅可以被认为是经典命题逻辑的保守扩展，而且当被限制为不超过2秩的cirquents时，也可以被认为是完全一般性的纯命题扩展IF逻辑的公理化。
2014-09-11 cs.LO
Elementary-base cirquent calculus I: Parallel and choice connectives
循环演算是一个证明系统，操纵循环风格的结构，而不是公式。利用它，本文构建了可计算性逻辑命题片段（计算问题的博弈语义构想逻辑，见http://www.csc.villanova.edu/~japaridz/CL/）的一个合理而完整的公理化CL 16，其逻辑词汇由否定、平行和选择连接词组成，其原子表示基本的，即无移动的博弈。
2017-07-16 cs.LO math.LO
Cirquent calculus deepened
循环演算是一种新的证明理论和语义框架，其主要区别特征是基于循环，而不是更传统的方法，处理树状对象，如公式或序列。其优点包括更高的效率、灵活性和表现力。本文提出了一个详细的阐述了深推理事件逻辑，这是自然和内在的资源意识。它表明，经典逻辑，无论是在句法上还是在语义上，都只是这种更一般的、在某种意义上更基本的逻辑--以循环演算形式出现的资源逻辑--的一个特殊的、保守的片段。读者会发现各种有利于切换到新框架的论点，例如显示线性逻辑或其他基于公式的方法开发资源逻辑的表达能力不足的论点，在Cirquent演算提供的表示和证明复杂性方面，传统方法的指数改进等等。本文的主要目的之一是提供一个介绍性的起点，正如作者所希望的那样，可能有机会成为证明理论研究的一个新方向-基于电路而不是公式的证明理论。
2008-04-01 cs.LO math.LO
A propositional system induced by Japaridze's approach to IF logic
循环演算（英语：Cirquent calculus）是G.Japaridze为了满足可计算逻辑的需要而提出的一种新的证明理论和语义方法，他还表明，通过循环演算，人们可以捕获，提炼和推广独立友好（IF）逻辑。具体来说，这种方法允许我们考虑独立于命题连接词的精神，就像传统的IF逻辑考虑独立于量词一样。雅帕里泽的治疗IF逻辑，但是，是纯粹的语义，并没有演绎系统提出。本文构造了一个完备的形式系统。Japaridze的基于循环的IF逻辑语义的命题片段。这样一个系统因此可以被认为是一个公理化的纯命题IF逻辑在其充分的一般性。
2014-05-23 cs.LO math.LO
The parallel versus branching recurrences in computability logic
本文证明了可计算性逻辑的并行递归导出的基本逻辑是分支递归导出的基本逻辑的真超集。后者被称为精确捕获的cirquent演算系统CL 15，由Japaridze保持健全--但不完整--与平行递归，而不是分支递归。目前的结果是通过积极验证该猜想。第二个结果的文件表明，平行递归是严格弱于分支递归的意义上说，而后者在逻辑上意味着前者，反之亦然不成立。
2011-07-12 cs.LO
Computability Logic: a formal theory of interaction
可计算性逻辑是（交互式）可计算性的形式理论，就像经典逻辑是真理的形式理论一样。这种方法最近在“可计算性逻辑导论”（《纯粹与应用逻辑年鉴》123（2003），第1 -99页）中提出。本文重新介绍了可计算性逻辑在一个更紧凑和更少的技术方式。它是写在一个semitutorial风格与一般计算机科学，逻辑或数学观众铭记。关于这一主题的因特网资料可在http：//www.cis.upenn.edu/paggiorgi/cl.html上查阅，其他材料可在http://www.csc.villanova.edu/~japaridz/CL/gsoll.html上查阅。
2004-12-10 cs.AI cs.LO math.LO
The intuitionistic fragment of computability logic at the propositional level
从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
Intuitionistic computability logic
可计算性逻辑（Computability Logic，CL）是关于计算任务和资源的系统形式化理论，在某种意义上，它可以被看作是线性逻辑的一种基于语义的替代。凭借其富有表现力和灵活的语言，其中公式表示计算问题，“真理”被理解为算法可解性，CL可能为建设性应用理论和计算系统提供全面的逻辑基础，这些理论和系统本质上需要建设性和计算意义的底层逻辑。其中最著名的构造主义逻辑是海廷的直觉演算INT，其语言可以被看作是CL语言的一个特殊片段。然而，INT的建构主义哲学从来没有真正找到一个直观上令人信服的和数学上严格的语义证明。CL有很好的索赔提供这样一个理由，因此实现了哥洛夫的著名论文“INT =逻辑问题”。本文包含了一个可靠性证明INT的CL语义。有关CL的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html
2006-06-14 cs.AI cs.LO math.LO
A new face of the branching recurrence of computability logic
这封信介绍了可计算性逻辑的分支递归操作的一个新的、实质上简化的版本（见http：//www.cis.upenn.edu/casigiorgi/cl.html），并证明了它与旧的“规范”版本的等价性。
2011-11-21 cs.LO math.LO
Toggling operators in computability logic
Shandong University（山东大学）；Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CL）（参见http://www.cis.upenn.edu/~giorgi/cl.html）是一个将逻辑重新发展为可计算性的形式理论的研究项目，与传统上的形式真理论相反。CL中的公式代表交互式计算问题，被视为机器与其环境之间的游戏;逻辑运算符代表对这些实体的操作;“真理”被理解为有效解决方案的存在。合作语言的形式是开放的，并可能会经历一系列的扩展，随着研究的进展。到目前为止，已经研究了三种类型的合取和析取：平行的，顺序的和选择的。本文件增加了一个更自然的类型，这个集合，称为切换。切换操作可以被描述为选择操作的宽松版本，其中选择是可伸缩的，允许重新考虑任何有限次数。通过这种方式，他们在交互式计算中模拟试错式决策步骤。本文的主要技术成果是为可计算性逻辑的命题片断构造了一个合理而完整的公理化，它的词汇表和否定一起包括所有四种合取和析取：平行的、切换的、顺序的和选择的。除了切换合取和析取之外，本文还介绍了量词和递归运算的切换版本。
2010-05-01 cs.AI cs.LO math.LO
Propositional computability logic I
与经典逻辑是真的形式理论一样，最近提出的可计算性逻辑也是可计算性的形式理论。它将（交互式）计算问题理解为机器与环境的博弈，将其可计算性理解为总是赢得博弈的机器的存在，将逻辑运算符理解为计算问题的运算，将逻辑公式的有效性理解为“总是可计算”问题的方案。目前的贡献给出了一个最基本的片段的可计算性逻辑的公理化的合理性和完整性证明的详细阐述。这个片段的逻辑词汇表包含所谓的并行和选择操作的操作符，它的原子代表基本问题，即标准意义上的谓词。这篇文章是自成一体的，因为它解释了所有相关的概念。虽然在技术上没有必要，但是，熟悉基础论文“Introduction to computability logic”[Annals of Pure and Applied Logic 123（2003），pp.1-99]将极大地帮助读者理解可计算性逻辑的哲学，潜在的动机，潜力和实用性，--决定当前结果价值的背景。有关该主题的在线介绍可在http://www.cis.upenn.edu/~giorgi/cl.html和http://www.csc.villanova.edu/~japaridz/CL/gsoll.html上查阅。
2004-06-21 cs.LO math.LO
A PSPACE-Complete First Order Fragment of Computability Logic
在最近启动的一个研究计划，发展逻辑作为一个正式的理论（互动）可计算性，几个非常有趣的逻辑已被介绍和公理化。这些更大的可计算性逻辑的片段不仅旨在描述“什么”可以计算，而且还提供了一种从证明中提取计算算法的机制。其中最具表现力和基础的是CL 4，已知是（建设性的）健全和完整的基础计算语义。进一步证明了CL 4中不含盲量词的片段在多项式空间中是可判定的。目前的工作扩展了这一结果，并证明了该片段，事实上，PSPACE完成。
2013-03-31 cs.CC cs.LO
From truth to computability II
可计算性逻辑是关于计算任务和资源的形式化理论。其中的公式代表交互式计算问题，而“真理”被理解为算法的可解性。交互式计算问题，反过来，被定义为某种类型的游戏之间的机器和它的环境，与逻辑运算符代表这种游戏的操作。在为这个语义引入逻辑的增量丰富片段寻找公理化的雄心勃勃的计划中，早期的文章“从真理到可计算性I”证明了系统CL3的可靠性和完备性，其语言具有所谓的平行连接词（包括否定），选择连接词，选择量词和盲量词。本文将这一结果扩展到具有相同逻辑运算符集合的更具表现力的系统CL4。使CL4富有表现力的是在其语言中存在两种原子：基本原子，代表基本计算问题（即谓词，即零交互度的问题），和一般原子，代表任意计算问题。CL4保守地扩展了CL3，后者只是前者的一般无原子片段。从CL4语言中删除盲（经典）量词组，产生一个可判定的逻辑，尽管后者仍然是一阶的。有关可计算性逻辑的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2005-07-20 cs.AI cs.LO math.LO
Sequential operators in computability logic
Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CL）（见http：//www.cis.upenn.edu/cnigiorgi/cl.html）是一个语义学平台和研究程序，用于将逻辑重新发展为可计算性的形式理论，而不是传统上的真值的形式理论。CL中的公式代表（交互式）计算问题，被理解为机器与其环境之间的游戏;逻辑运算符表示对这些实体的操作;“真”被理解为有效解的存在，即，算法获胜策略的一部分CL的形式主义是开放式的，并可能会经历一系列的扩展，作为该主题的研究进展。到目前为止，CL一直关注的主要运营商群体是并行，选择，分支和盲运营商。本文介绍了一组新的重要算子，称为序列算子。后者的形式是连续的合取和析取、连续的量词和连续的递归。顾名思义，与这一组相关联的算法直觉是顺序计算的直觉，而不是与并行运算组相关联的并行计算的直觉：玩游戏的顺序组合意味着以顺序的方式一个接一个地玩它的组件。本文件的主要技术成果是一个健全的和完整的公理化的命题片段的可计算性逻辑的词汇，连同否定，包括所有三个-平行，选择和顺序-排序的合取和析取。这一结果的扩展到一阶水平也概述。
2008-10-15 cs.AI cs.LO math.LO
Towards applied theories based on computability logic
可计算性逻辑（Computability Logic，CL）（见http：//www.cis.upenn.edu/linggiorgi/cl.html）是一个最近启动的程序，用于将逻辑重新发展为可计算性的形式理论，而不是逻辑更传统的形式真值理论。其中的公式代表计算问题，“真理”意味着算法解决方案的存在，而证明则对这些解决方案进行编码。在致力于寻找公理化的CL更有表现力的片段的研究路线，本文介绍了一个新的演绎系统CL 12，并证明了其可靠性和完整性方面的语义CL。保守地扩展了经典谓词演算，并提供了相当多的额外的表达和演绎能力，CL 12提出了一个合理的，计算上有意义的，建设性的替代经典逻辑作为应用理论的基础。为了获得这种理论的模型实例，本文将传统的基于经典逻辑的Peano算法重建为基于可计算性逻辑的Peano算法。本贡献的目的之一是提供一个起点，作者希望，可能成为一个新的研究路线与潜在的有趣的发现-一个探索的可能是相当不寻常的元理论CL为基础的算术和其他CL为基础的应用系统。
2009-11-17 cs.AI cs.LO math.LO
A logical basis for constructive systems
这项工作致力于可计算性逻辑（CoL）-哲学/数学平台和长期项目，用于在其底层语义中用可计算性取代真理之后重新开发经典逻辑（见http：//www.cis.upenn.edu/paggiorgi/cl.html）。本文阐述了CoL框架的一些基本复杂性理论。然后证明了演绎系统CL 12关于CoL语义的可靠性和完备性，包括后者基于多项式时间可计算性而不是原则上可计算性的版本。CL 12是一个微积分系统，其中一个变量的含义直观上可以被描述为“后继变量可以在算法上还原为先行变量”，并且其中公式是由谓词字母、函数字母、变量、常数、恒等式、否定式、平行和选择连接词以及盲量词和选择量词构建的。一个案例是CL 12是一个足够的逻辑基础建设性的应用理论，包括复杂性导向的。
2011-03-14 cs.CC cs.LO math.LO
On the system CL12 of computability logic
可计算性逻辑（参见http：//www.csc.villanova.edu/cnjaparidz/CL/）是一个长期的项目，用于在建设性游戏语义的基础上重新开发逻辑，将游戏视为交互式计算问题的抽象模型。CL 12是经典一阶逻辑的一个保守扩展，它的语言用量词和连接词的所谓选择类扩充了经典逻辑的语言。这个系统已经发现富有成效的应用程序作为皮亚诺算术的建设性和复杂性为导向的版本，如多项式时间可计算性，多项式空间可计算性，和超越算术的逻辑基础。本文介绍了第三个，必不可少的复杂性措施的互动计算称为振幅复杂性，并建立了适当的CL 12相对于A-振幅，S-空间和T-时间的可计算性在一定的最小条件下的三元组（A，S，T）的功能类。这一结果极大地拓宽了CL 12的潜在应用领域。该文件是独立的，目标读者事先不熟悉的主题。
2015-07-25 cs.LO math.LO
Dynamic Probability Logic: Decidability & Computability
本文针对动态概率逻辑（DPL）的可判定性与可计算性展开研究，构建了弱完备且具有限模型性质（可判定）的证明系统$\u001b[1mH\u001b[0m_{DPL}$，还提出强完备证明系统HDPL并证明其典范模型为可计算结构。
2024-06-24 cs.LO math.LO
Propositional Computability Logic II
可计算性逻辑是关于计算任务和资源的形式化理论。它的公式代表交互式计算问题，逻辑运算符代表计算问题的运算，公式的有效性被理解为总是有算法解决方案的问题的方案。关于这一主题的全面在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上查阅。早期的文章“命题可计算性逻辑I”证明了可计算性逻辑的最小非平凡片段CL1的可靠性和完备性。本文将这一结果扩展到更有表现力的命题系统CL2。使CL2比CL1更具表达力的是其语言中存在两种原子：基本原子，表示基本计算问题（即谓词），以及一般原子，表示任意计算问题。CL2保守地扩展了CL1，后者只是前者的一般无原子片段。
2004-06-20 cs.GT cs.LO math.LO
On the toggling-branching recurrence of Computability Logic
我们引入了一个新的，大大简化版本的切换分支递归操作的可计算性逻辑，证明其等价于Japaridze的旧的，“规范”的版本，并证明这两个版本保持其参数的静态属性。
2012-07-05 cs.LO
Fundamentals of computability logic 2020
这篇文章是对可计算性逻辑的半理论式的调查。它的扩展在线版本在http://www.csc.villanova.edu/~japaridz/CL/上维护。
2020-11-01 cs.LO
A survey of computability logic
本文介绍了可计算性逻辑的概况：它的哲学和动机，主要概念和迄今为止取得的最重要的成果。这篇文章的持续更新的在线版本在http://www.csc.villanova.edu/~japaridz/CL/上维护。
2016-12-14 cs.LO
The logic of interactive Turing reduction
本文从可计算性逻辑的语义出发，将直觉蕴涵理解为交互式算法约简，给出了直觉演算的蕴涵片段的可靠性和完备性证明。这个概念--更准确地说，是归约的相关概念--是图灵归约从传统的输入/输出问题到任意交互程度的计算任务的概括。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
The countable versus uncountable branching recurrences in computability logic
本文介绍了可计算逻辑中可数分支递归的一种新的简化形式，证明了它与旧的可计算逻辑的等价性，并指出由它导出的基本逻辑是由不可数分支递归导出的基本逻辑的真超集。本文的一个进一步的结果是：可数分支递归式严格弱于不可数分支递归式，因为后者逻辑上蕴涵前者，而不是前者逻辑上蕴涵后者.
2011-07-19 cs.LO
From truth to computability I
可计算性逻辑是最近提出的一种交互计算的形式化理论。有关该主题的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html。本文包含了一个合理性和完整性证明的演绎系统CL3公理化的最基本的一阶片段的可计算性逻辑称为有限深度，元素基片段。这一结果的潜在应用领域包括交互计算理论、建设性应用理论、知识库系统、资源约束规划和行动系统。本文件是自成一体的，因为它重新介绍了所有相关定义以及主要动机。
2005-07-20 cs.AI cs.GT cs.LO
Quantum First-Order Logics That Capture Logarithmic-Time/Space Quantum Computability
本文提出量子一阶逻辑（QFO），通过特殊量子连接词和量词及函数式量子变量，刻画有界误差量子对数时间可计算性，并借助量子传递闭包算子表征量子对数空间可计算性。
2025-01-21 cs.CC cs.LO quant-ph
Computability logic: Giving Caesar what belongs to Caesar
本文是一个简短的非正式调查的可计算性逻辑-游戏语义构思的形式理论的计算资源和任务。这种相对年轻的非经典逻辑是经典一阶逻辑的保守扩展，但比后者更具表现力，产生了广泛的新的潜在应用领域。在一个合理的（即使不是严格的）意义上，直觉主义和线性逻辑也是如此，这使我们可以说CoL在其自然和“普遍”的游戏语义学基础上调和和统一了逻辑思维的三个传统（以及超越）。关于这个问题的全面在线调查可以在http://www.csc.villanova.edu/~japaridz/CL/上找到。
2019-02-14 cs.LO
In the beginning was game semantics
本文概述了可计算性逻辑--交互式计算任务和资源的游戏语义构造逻辑。只有一个非概述，在它的技术部分，致力于证明健全的仿射逻辑方面的语义可计算性逻辑。有关该主题的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-24 cs.AI cs.LO math.LO
Expressing Algorithms As Concise As Possible via Computability Logic
本文提出了一种新的算法定义和表示方法：{ \it任务逻辑}算法的概念。此概念允许用户将任务$T$的算法定义为可以共同执行$T$的一组代理。这个概念大大简化了算法开发过程，可以看作是顺序伪代码和逻辑算法的集成。这一观察结果需要对算法开发过程进行一些更改。我们提出了一个两步的方法：第一步是定义一个算法的任务$T$通过一组代理，可以共同执行$T$。第二步是将这些代理转换为（高阶）可计算性逻辑。
2013-05-09 cs.LO
PECR: A formal system based on computability logic
PECR是一个基于可计算性逻辑的形式系统，通过整合机器有限资源来探索程序可计算性，并应用于自然法则研究以严格构建真实世界现象的计算机模型。
2024-03-21 cs.LO
The Fertile Steppe: Computability Logic and the decidability of one of its fragments
本文系统介绍可计算性逻辑（CoL）及其核心语义、语法和 Cirquent Calculus 证明系统，并针对其公理化系统 CL15 给出可判定性的尝试性证明，同时探讨其在算术与人工智能中的应用价值。
2025-03-05 cs.LO
Axiomatizations and Computability of Weighted Monadic Second-Order Logic
加权一元二阶逻辑是一元二阶逻辑的加权扩展，它精确地捕捉了加权自动机的行为。它的语义是相对于半环参数化的，加权公式输出的值在半环上进行评估。Gastin和Monmege（2018）给出了加权一元二阶逻辑的抽象语义，以给出逻辑与加权自动机的等价性的更一般和模块化的证明。我们专注于抽象的语义的逻辑，我们给一个完整的公理化的完整的逻辑和一个片段没有一般的总和，从而给一个更细粒度的理解的逻辑。我们讨论了如何常见的决策问题的逻辑语言可以适应加权设置，并表明，其中许多是可判定的，虽然他们继承了坏的复杂性从底层的第一和第二阶逻辑。然而，我们表明，加权适应的可满足性是不可判定的逻辑时，使用的抽象解释。
2021-04-29 cs.FL cs.LO
Foundations of real analysis and computability theory in non-Aristotelian finitary logic
本文概述了最近提出的非阿斯特丽德有限逻辑（NAFL）的实分析和可计算性理论的新范式。NAFL（NRA）中的构造性实分析是通过将欧几里德几何中的图解概念翻译成NAFL版本的皮亚诺算术（NPA）的扩展（NPAR）来完成的。这样的翻译是可能的，因为NPA证明了存在每一个可以用NPA语言定义的自然数的无限真类。NPAR中不允许无限集合，并且禁止对适当类进行量化;因此康托的对角线方法在NRA中不能合法地公式化，并且对于任何实数的集合（“超类”）都没有“基数”。经典实分析的许多有用的方面，如牛顿和莱布尼茨的微积分，在NRA中是合理的。但悖论，如芝诺的运动悖论和巴拿赫-塔斯基悖论，解决，因为NRA只承认封闭的实数超类，特别是，开放/半开区间的实数是不允许的。NAFL版本的可计算性理论（NCT）拒绝了图灵关于停机问题的不可判定性的论证，并允许超计算。NCT的重要潜在应用是在量子和自主计算领域。
2005-09-29 cs.LO math.GM math.LO
Introduction to clarithmetic I
“Clarithmetic”是一个与皮亚诺算术类似的形式数论的通用名称，但基于可计算性逻辑（参见http：//www.cis.upenn.edu/classgi/cl.html），而不是更传统的经典或直觉逻辑。claithmetical理论的公式代表交互式计算问题，它们的“真理”被理解为算法解的存在。对这些解决方案施加各种复杂性约束会产生各种版本的clarithmetic。本文介绍了一个多项式时间可计算性的算法体系，该体系是完善的。在这个意义上，系统的每个定理T都代表一个具有多项式时间解的交互数论计算问题，而且，这样的解可以有效地从T的证明中提取出来。完备性的意义在于，每一个具有多项式时间解的交互数论问题都由系统的某个定理T表示。这篇论文是写在semitutorial风格和目标读者事先不熟悉可计算性逻辑。
2011-08-23 cs.CC cs.LO math.LO
A Simplicial Complex Model for Dynamic Epistemic Logic to study Distributed Task Computability
多智能体系统的通常认知模型S5n是基于Kripke框架的，Kripke框架是一个图，其边缘用不区分两种状态的智能体标记。我们建议通过考虑一个对偶的单纯复杂模型来揭示这个结构中隐含的高维信息。我们使用动态认识逻辑（DEL）来研究认识单纯复模型在一组主体相互通信后如何变化。我们专注于一个动作模型，表示异步代理的所谓的即时快照通信模式，因为它是分布式可计算性的核心（但我们的设置适用于其他通信模式）。从最初的认知复合体到应用动作模型后的认知复合体，存在拓扑不变量，这些拓扑不变量决定了主体在通信后获得的知识。最后，我们描述了如何分布式任务规范可以建模为一个DEL动作模型，并表明，拓扑不变量确定任务是否是可解的。因此，我们提供了一个桥梁DEL和分布式可计算性的拓扑理论，研究任务的可解性在一个共享的内存或消息传递架构。
2018-09-10 cs.DC cs.LO
On the Computability of Measures of Regular Sets of Infinite Trees
本文研究无限树上一元二阶逻辑的概率可满足性问题，提出计算随机树满足给定公式概率的方法，并证明该概率为代数数，从而将此前仅适用于较弱形式体系的结果推广到完整一元二阶逻辑。
2024-11-21 cs.LO
Computability of simple games: A complete investigation of the sixty-four possibilities
根据四个常规公理：单调性、适当性、强性和非弱性，将简单博弈分为十六种“类型”。根据有限性（有限载体的存在性）和算法可计算性，进一步将它们分为64类。对于每一个这样的类，我们要么证明它是空的，要么给出一个属于它的博弈的例子。我们观察到，如果一个类型包含一个无限博弈，那么它既包含可计算的博弈，也包含不可计算的博弈。这有力地表明，可计算性在逻辑上和概念上与常规公理无关。
2011-02-20 cs.GT cs.LO math.LO
Effective AGM Belief Contraction: A Journey beyond the Finitary Realm (Technical Report)
University of Freiburg（弗赖堡大学）；LIX - CNRS - École Polytechnique（巴黎高等理工学院LIX研究所）；Cardiff University（卡迪夫大学）
该研究探讨非有限逻辑中AGM信念收缩的可计算性，发现不可计算性普遍存在且现有策略失效，提出基于Büchi自动机的LTL可计算收缩函数新方法。
2025-08-04 cs.AI cs.LO
On Transitive modal many-valued logics
本文主要研究由赋值Kripke框架定义的模态逻辑，特别是在某些剩余格上赋值传递Kripke框架的模态逻辑的可计算性和可表示性问题。它表明，一个大家庭的这些逻辑-包括所产生的标准MV和产品代数-产生一个不可判定的后果关系。随后，传递模态Lukasiewicz逻辑的行为进行了比较，它的非传递对应，展示了一些细节有关的可计算性和等价与其他逻辑。最后，我们展示了不可判定性的有效性和局部SAT问题的传递模型时，Delta操作添加到逻辑。
2019-04-02 cs.LO
Algebra of Self-Replication
本文提出使用可通过项重写判定的极小等式逻辑来检验可计算性理论，并对两个可判定片段中的 quine 程序进行分类，解释了其本质相似性。
2023-11-19 cs.LO math.LO
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-12 cs.LO math.LO
Logical Pseudocode: Connecting Algorithms with Proofs
证明（微积分，自然演绎）和命令式算法（伪码）是两个众所周知的共存概念。那他们是什么关系？我们的答案是，\[ imperative\ algorithms\ =\ proofs\ with\ cuts \]这一观察导致一个推广的伪码，我们称之为{ \it逻辑伪码}。它类似于可计算性逻辑\cite{Jap03,Jap08}的自然演绎证明。其中的每一个陈述都对应于自然演绎中的一个证明步骤。因此，相对于伪代码，它的优点是保证每个语句相对于初始规范是正确和安全的。它也可以被看作是可计算性逻辑网（\colw）的扩展，具有正向推理能力。
2022-02-14 cs.LO
Higher-Order Termination: from Kruskal to Computability
终结性是逻辑学和计算机科学中的一个重要问题。在逻辑中，终止是证明理论的核心，通常被称为强规范化（切割消除）。在计算机科学中，终止性一直是表明程序正确性的一个重要问题。在早期的逻辑中，强规范化通常通过将序数分配给表达式来显示，以这种方式消除切割将产生具有较小序数的表达式。在验证的早期，计算机科学家使用了类似的想法，通过自然数（例如大小）来解释程序调用的参数。显示每个递归调用的参数的大小减少给出了程序的终止证明，然而这是相当弱的，因为它只能产生相当小的序数。在六十年代，泰特发明了一种新的方法来显示自然演绎的切割消除，基于项集合上的谓词，使得表达式对谓词的成员关系暗示了该表达式的强规范化属性。谓词是通过类型上的归纳定义的，或者甚至是作为一个不动点，这种方法可以产生更大的序数。后来Girard以约简或可计算性候选人的名义推广了它，它在证明类型化可达演算的强规范化性质方面表现得非常有效。
2007-01-05 cs.LO
Implementing program extraction from CL1-proofs
可计算性逻辑（Computability Logic，CoL）是一种交互计算的形式化理论。它将计算问题理解为两个玩家的游戏：机器和它的环境，使用逻辑形式主义来描述有效的可计算性原则和公式来表示计算问题。逻辑CL1是CoL的一个片段的演绎系统，逻辑词汇表包含了经典逻辑的所有算子和选择算子，原子表示经典逻辑的基本博弈即谓词。在本文中，我们提出了一个程序，采取CL1证明的任意公式$F$，并提取一个获胜的策略，$F$从证明，然后发挥$F$使用该策略。我们希望本文将提供一个起点，进一步的工作，在程序提取的CoL为基础的算法和其他CoL为基础的应用系统。
2013-11-26 cs.LO
A Game-Semantic Model of Computation
本文介绍了一种新的概念“（有效）可计算性”，称为生存能力，在游戏语义中的战略在一个内在的（即，不求助于标准的丘奇-图灵可计算性），非归纳和非公理化的方式，并显示，作为一个主要的技术成就，可行的策略是图灵完备的。因此，我们已经给出了与图灵机相同意义上的计算的数学基础，但超出了自然数的计算，例如，高阶计算，以一种更抽象的方式。作为直接推论，推广了可计算性理论中的一些著名定理，如smn定理和第一递归定理。值得注意的是，我们的游戏语义框架区分“高层次”的计算过程，直接操作的数学对象，如自然数（而不是他们的符号表示）和他们的“符号实现”，定义他们的“可计算性”，这揭示了新的光计算的概念。这项工作的目的是成为一个垫脚石走向一个新的数学基础的计算，直觉逻辑和建设性数学。
2018-06-26 cs.LO
Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
我们提出了一个基于图的布尔逻辑扩展称为布尔图逻辑（BGL）。将公式树构造为上图的余树，我们可以用纯图论的术语来描述诸如求值和蕴涵等语义概念，由此我们恢复了BGL的定义。自然，它比通常的布尔逻辑保守。（1）给出了BGL的一种基于布尔关系的自然语义，即它是一种多值语义，并证明了这种语义对于相应的蕴涵概念的充分性。(2)我们发现，评估的复杂性是NP-完全的任意图（而不是ALOGTIME-完全的公式），而蕴涵是$Π^p_2$ -完全的（而不是coNP-完全的公式）。(3)本文给出了图的模分解的归纳求值的一个递归算法。（虽然这不是多项式时间，cf。第（2）点）。(4)我们在一个博弈论的设置，在静态和序列策略，扩展位置游戏形式超越cographs的经典概念的评价。(5)我们给出了一个公理化的BGL，深推理证明理论的启发，并显示出相应的概念蕴涵的合理性和完整性。图论设置的一个特别的特征是，它逃避了某些不可行的定理，例如达斯和斯特拉斯伯格最近的结果，布尔逻辑的线性片段没有线性公理化（等价于贾帕里泽的可计算性逻辑的乘法片段或布拉斯的多元线性逻辑的游戏语义）。
2020-04-27 cs.LO math.LO
