The taming of recurrences in computability logic through cirquent calculus, Part I
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。
2012-09-19 cs.LO math.LO
The taming of recurrences in computability logic through cirquent calculus, Part II
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。
2011-06-19 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
Soundness and completeness of the cirquent calculus system CL6 for computability logic
可计算性逻辑是可计算性的形式化理论。Japaridze的早期文章“Introduction to Cirquent Calculus and Abstract Resource Semantics”证明了可计算性逻辑的基本片段CL5的可靠性和完备性。本文将这一结果扩展到更具表现力的cirquent演算系统CL6，这是CL5和经典命题逻辑的保守扩展。
2011-06-12 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
Dynamic Probability Logic: Decidability & Computability
本文针对动态概率逻辑（DPL）的可判定性与可计算性展开研究，构建了弱完备且具有限模型性质（可判定）的证明系统$\u001b[1mH\u001b[0m_{DPL}$，还提出强完备证明系统HDPL并证明其典范模型为可计算结构。
2024-06-24 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
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
The countable versus uncountable branching recurrences in computability logic
本文介绍了可计算逻辑中可数分支递归的一种新的简化形式，证明了它与旧的可计算逻辑的等价性，并指出由它导出的基本逻辑是由不可数分支递归导出的基本逻辑的真超集。本文的一个进一步的结果是：可数分支递归式严格弱于不可数分支递归式，因为后者逻辑上蕴涵前者，而不是前者逻辑上蕴涵后者.
2011-07-19 cs.LO
From formulas to cirquents in computability logic
Shandong University（山东大学）；Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CoL）（参见http：//www.cis.upenn.edu/cnigiorgi/cl.html）是一个最近引入的语义平台和雄心勃勃的计划，用于将逻辑重新发展为可计算性的形式理论，而不是逻辑传统上的形式真值理论。它的表达式代表了交互式计算任务，被视为机器与环境的游戏，而“真理”被理解为算法获胜策略的存在。CoL的形式主义是开放式的，并且已经经历了一系列的扩展，其中逻辑运算符代表了对游戏的操作。本文以一种全新的方式扩展了CoL的表达能力，将公式（CoL的早期语言仅限于此）推广到称为cirquents的电路式结构。与公式不同，后者能够解释整个游戏/任务的不同部分之间的子游戏/子任务共享。这种能力所提供的许多优点之一是，它允许我们捕获、提炼和概括众所周知的独立友好逻辑，在目前的飞跃之后，它自然成为CoL的保守片段，就像经典逻辑被认为是CoL的基于公式的版本的保守片段一样。并且可以在不熟悉CoL的情况下阅读。
2011-04-27 cs.AI cs.CC 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
Computability logic: Giving Caesar what belongs to Caesar
本文是一个简短的非正式调查的可计算性逻辑-游戏语义构思的形式理论的计算资源和任务。这种相对年轻的非经典逻辑是经典一阶逻辑的保守扩展，但比后者更具表现力，产生了广泛的新的潜在应用领域。在一个合理的（即使不是严格的）意义上，直觉主义和线性逻辑也是如此，这使我们可以说CoL在其自然和“普遍”的游戏语义学基础上调和和统一了逻辑思维的三个传统（以及超越）。关于这个问题的全面在线调查可以在http://www.csc.villanova.edu/~japaridz/CL/上找到。
2019-02-14 cs.LO
A PSPACE-Complete First Order Fragment of Computability Logic
在最近启动的一个研究计划，发展逻辑作为一个正式的理论（互动）可计算性，几个非常有趣的逻辑已被介绍和公理化。这些更大的可计算性逻辑的片段不仅旨在描述“什么”可以计算，而且还提供了一种从证明中提取计算算法的机制。其中最具表现力和基础的是CL 4，已知是（建设性的）健全和完整的基础计算语义。进一步证明了CL 4中不含盲量词的片段在多项式空间中是可判定的。目前的工作扩展了这一结果，并证明了该片段，事实上，PSPACE完成。
2013-03-31 cs.CC cs.LO
The parallel versus branching recurrences in computability logic
本文证明了可计算性逻辑的并行递归导出的基本逻辑是分支递归导出的基本逻辑的真超集。后者被称为精确捕获的cirquent演算系统CL 15，由Japaridze保持健全--但不完整--与平行递归，而不是分支递归。目前的结果是通过积极验证该猜想。第二个结果的文件表明，平行递归是严格弱于分支递归的意义上说，而后者在逻辑上意味着前者，反之亦然不成立。
2011-07-12 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
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
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
In the beginning was game semantics
本文概述了可计算性逻辑--交互式计算任务和资源的游戏语义构造逻辑。只有一个非概述，在它的技术部分，致力于证明健全的仿射逻辑方面的语义可计算性逻辑。有关该主题的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-24 cs.AI cs.LO math.LO
Thoughts on sub-Turing interactive computability
本文提出可计算性逻辑的新研究方向，将无限内存等不可能具备的资源视为计算设备的外部资源，主张在表达计算问题的逻辑公式前件中明确核算这类资源，研究无需此类资源的亚图灵交互可计算性。
2024-11-03 cs.LO
Quantum First-Order Logics That Capture Logarithmic-Time/Space Quantum Computability
本文提出量子一阶逻辑（QFO），通过特殊量子连接词和量词及函数式量子变量，刻画有界误差量子对数时间可计算性，并借助量子传递闭包算子表征量子对数空间可计算性。
2025-01-21 cs.CC cs.LO quant-ph
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
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
The Fertile Steppe: Computability Logic and the decidability of one of its fragments
本文系统介绍可计算性逻辑（CoL）及其核心语义、语法和 Cirquent Calculus 证明系统，并针对其公理化系统 CL15 给出可判定性的尝试性证明，同时探讨其在算术与人工智能中的应用价值。
2025-03-05 cs.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
Introduction to Cirquent Calculus and Abstract Resource Semantics
本文介绍了一种改进的微积分的方法，称为cirquent演算。而在Gentzen风格的证明树兄弟姐妹（或堂兄弟姐妹等）序列是不相交的公式序列，在圆微积分中，它们可以共享元素。明确地允许或禁止共享资源，从而将子结构逻辑的资源感知直觉带到一个更微妙的层次，cirquent演算提供了比cirquent演算更大的灵活性和功能。随着可计算性逻辑的诞生，对新的演绎工具的需求也随之而来（见http：//www.cis.upenn.edu/linggiorgi/cl.html）--这是一种语义构建的计算资源形式理论，它顽固地抵制了传统句法方法框架内的任何公理化尝试。循环微积分打破了僵局。从其规则的全部集合中去除收缩，产生了可计算性逻辑的基本片段CL 5的健全和完整的系统。另一方面，在微积分中做同样的事情，会把婴儿和洗澡水一起扔掉，导致严格较弱的仿射逻辑。可计算性逻辑的一个隐含的主张是，它是CL 5，而不是仿射逻辑，充分体现了传统上与后者相关的资源哲学。为了加强这一主张，本文进一步引入了一个抽象的资源语义，并显示了CL 5的可靠性和完整性。
2005-12-23 cs.LO math.LO
Algebra of Self-Replication
本文提出使用可通过项重写判定的极小等式逻辑来检验可计算性理论，并对两个可判定片段中的 quine 程序进行分类，解释了其本质相似性。
2023-11-19 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
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-12 cs.LO math.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
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
Ptarithmetic
Villanova University（维拉诺瓦大学）
本文介绍了ptarithmetic（“多项式时间算术”的缩写）--一种类似于著名的Peano算术的形式数论，但它是基于最近诞生的可计算性逻辑（见http：//www.cis.upenn.edu/paggiorgi/cl.html）而不是经典逻辑。ptarithmetic的公式表示交互式计算问题，而不仅仅是真/假语句，它们的“真”被理解为存在一个多项式时间解。本文所阐述的算法体系是完善的。在这个意义上，系统的每个定理T都代表了一个具有多项式时间解的交互数论计算问题，而且，这样的解可以有效地从T的证明中提取出来。完备性的意义在于，每一个具有多项式时间解的交互数论问题都由系统的某个定理T表示。这篇论文是独立的，并且可以在没有任何先前对可计算性逻辑的熟悉的情况下阅读。
2010-02-26 cs.AI cs.CC cs.LO
Logics of formal inconsistency arising from systems of fuzzy logic
Artificial Intelligence Research Institute (IIIA), CSIC（西班牙科学研究理事会人工智能研究所）
本文提出了模糊逻辑与次协调的一种非常精确和基础性的相遇。具体而言，在本文中，我们介绍了扩展的模糊逻辑MTL的原始运营商的一致性和不一致的风格，所谓的逻辑形式不一致（LFIs）。本方法的主要新颖之处在于定义了MTL-代数上这类算子的公设，从而定义和公理化了一族逻辑，扩展了MTL，其度保持对应物是次协调的，而且是LFI。
2014-03-08 cs.AI cs.LO math.LO
Cognitive Binary Logic - The Natural Unified Formal Theory of Propositional Binary Logic
本文提出了一种形式化理论，它将命题二元逻辑描述为一种语义封闭的形式语言，并允许在相同的（计算）形式语言中，使用相同的数据结构来表达和测试语法和语义上良好的公式、形式证明（在希尔伯特接受中的可论证性）、演绎（根岑的可论证性观点）、CNF化和解构。本文还指出，认知二元逻辑是一种自我描述的理论，它解构了说谎者悖论。
2011-06-12 cs.LO math.LO
On Logic of Formal Provability and Explicit Proofs
1933年，哥德尔考虑了两种描述可证明性的模态方法。一个捕获了形式可证明性，并导致了逻辑GL和Solovay的完备性定理。另一种是以模态逻辑S4为基础，发展出阿特莫夫的证明逻辑LP。本文研究了作者提出的逻辑GLA，它是GL和LP语言的结合体。GLA具有Kripke风格的语义和相应的完备性定理。建立了GLA关于算术可证性语义的可靠性和完备性。
2014-05-11 cs.LO math.LO
Relations between assumption-based approaches in nonmonotonic logic and formal argumentation
Institute of Philosophy II, Ruhr Universität Bochum（波鸿鲁尔大学第二哲学研究所）；Ruhr Universität Bochum（波鸿鲁尔大学）
在本文中，我们作出的贡献，统一的形式模型的可废止推理。我们提出了几个翻译之间的正式论证框架和非单调逻辑推理合理的假设。更具体地说，我们将自适应逻辑转换为基于推理的论证，将ASPIC+、ASPIC+转换为基于推理的论证，将基于推理的论证的一个片段转换为自适应逻辑。自适应逻辑与梅金森的默认假设密切相关，并且与KLM和Shoham的偏好语义传统中的一类重要系统密切相关。因此，我们的研究结果也提供了正式的论证和后者的方法之间的密切联系。
2016-04-01 cs.AI cs.LO
A Modal Logic for Possibilistic Reasoning with Fuzzy Formal Contexts
Institute of Information Science, Academia Sinica（学术院信息科学研究所）
本文提出了一种用于模糊形式背景的可能性推理的双类型加权模态逻辑，实现了对模糊概念的扩展，并展示了逻辑的表达能力和扩展可能性。
2025-12-31 cs.AI cs.LO
Category theory, logic and formal linguistics: some connections, old and new
Université de Bordeaux（波尔多大学）
我们抓住出版的机会，从\emph{Logic, categories, semantics}研讨会在\emph{Journal of Applied Logic}调查一些当前的趋势，在逻辑，即直觉和线性类型的理论，交织分类，几何和计算的考虑。此后，我们提出如何这些丰富的逻辑框架可以模拟语言传达意义的方式。
2014-01-25 cs.CL cs.LO math.CT
Rapid Prototyping Formal Systems in MMT: 5 Case Studies
逻辑框架是元形式主义，其中可以定义对象逻辑和相关形式系统的语法和语义。这允许对象逻辑从框架继承实现，例如，解析器、类型检查器或模块系统。但是，如果所需的对象逻辑落在逻辑框架的舒适区之外，这些定义可能会变得麻烦或不可行。因此，MMT系统比以前的框架抽象得更远：它根本不假设类型系统或逻辑，并允许其内核算法由几乎任意的规则集定制。特别是，这允许在MMT中实现标准逻辑框架，如LF。但它这样做没有链接用户到一个特定的元形式主义：用户可以灵活地适应MMT的对象逻辑的要求it.In本文中，我们提出了一系列的案例研究，这样做，定义越来越复杂的对象逻辑在MMT。我们尽可能使用优雅的声明式逻辑定义，但在必要时将全新的规则注入内核。我们的经验表明，MMT的方法可以非常容易和快速地获得非常不同的正式系统的原型实现。
2019-10-24 cs.LO
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第六届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2015）的会议记录。研讨会于2015年9月21日和22日在意大利热那亚举行。专题讨论会的会议记录载有三次应邀演讲的摘要和13篇论文，这些论文是经过仔细评估后被接受在会议上介绍的。被接受的论文的主题包括算法博弈论，自动机理论，形式化验证，模态和时序逻辑。
2015-09-23 cs.FL cs.LO
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第12届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2021）的会议记录。Gandalf 2021研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2021-09-16 cs.FL cs.GT cs.LO
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第13届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2022）的会议记录。Gandalf 2022研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2022-09-19 cs.FL cs.GT cs.LO
Implementation of Formal Semantics and the Potential of Non-Classical Logic Systems for the Enhancement of Access Control Models: A Literature Review
该文献综述梳理了经典逻辑在现有访问控制模型中的应用及模型局限，探究了用非经典逻辑系统增强访问控制模型的潜力，并明确了经典逻辑对RBAC、ABAC模型正确性的描述与证明作用。
2023-08-24 cs.CR cs.LO
Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification
本文是关于GandALF 2026研讨会论文集的介绍，该会议于2026年在丹麦奥尔堡举行，旨在汇集博弈、自动机、逻辑与形式化验证领域的研究者，促进理论与应用的交叉融合。
2026-10-08 cs.FL cs.LO
Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第七届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2016）的会议记录。研讨会于2016年9月14日至16日在意大利卡塔尼亚举行。研讨会的会议记录包括3个特邀演讲的摘要和21篇论文全文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题涵盖算法博弈论，自动机理论，综合，形式化验证，动态，模态和时态逻辑。
2016-09-13 cs.FL cs.GT cs.LO
Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification
该论文集汇集GandALF 2023关于博弈、自动机、逻辑与形式验证的研究，旨在连接学界与业界并推动理论及应用的交叉融合。
2023-09-29 cs.CC cs.FL cs.LO
