可计算性逻辑中的切换运算符

可计算性逻辑中的序列运算符

Sequential operators in computability logic

可计算性逻辑（Computability Logic，CL）（见http：//www.cis.upenn.edu/cnigiorgi/cl.html）是一个语义学平台和研究程序，用于将逻辑重新发展为可计算性的形式理论，而不是传统上的真值的形式理论。CL中的公式代表（交互式）计算问题，被理解为机器与其环境之间的游戏;逻辑运算符表示对这些实体的操作;“真”被理解为有效解的存在，即，算法获胜策略的一部分CL的形式主义是开放式的，并可能会经历一系列的扩展，作为该主题的研究进展。到目前为止，CL一直关注的主要运营商群体是并行，选择，分支和盲运营商。本文介绍了一组新的重要算子，称为序列算子。后者的形式是连续的合取和析取、连续的量词和连续的递归。顾名思义，与这一组相关联的算法直觉是顺序计算的直觉，而不是与并行运算组相关联的并行计算的直觉：玩游戏的顺序组合意味着以顺序的方式一个接一个地玩它的组件。本文件的主要技术成果是一个健全的和完整的公理化的命题片段的可计算性逻辑的词汇，连同否定，包括所有三个-平行，选择和顺序-排序的合取和析取。这一结果的扩展到一阶水平也概述。

命题可计算性逻辑I

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上查阅。

可计算性逻辑的命题圆环演算

A propositional cirquent calculus for computability logic

本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。

可计算性逻辑中递归性的顺演算驯服，第I部分

The taming of recurrences in computability logic through cirquent calculus, Part I

本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。

可计算性逻辑中递归性的顺演算驯服，第II部分

The taming of recurrences in computability logic through cirquent calculus, Part II

本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。

关于可计算性逻辑系统CL12

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的潜在应用领域。该文件是独立的，目标读者事先不熟悉的主题。

基于可计算性逻辑的应用理论

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为基础的应用系统。

动态概率逻辑：可判定性与可计算性

Dynamic Probability Logic: Decidability & Computability

本文针对动态概率逻辑（DPL）的可判定性与可计算性展开研究，构建了弱完备且具有限模型性质（可判定）的证明系统$\u001b[1mH\u001b[0m_{DPL}$，还提出强完备证明系统HDPL并证明其典范模型为可计算结构。

交互式图灵归约的逻辑

The logic of interactive Turing reduction

本文从可计算性逻辑的语义出发，将直觉蕴涵理解为交互式算法约简，给出了直觉演算的蕴涵片段的可靠性和完备性证明。这个概念--更准确地说，是归约的相关概念--是图灵归约从传统的输入/输出问题到任意交互程度的计算任务的概括。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。

可计算性逻辑的流演算系统CL6的可靠性和完备性

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和经典命题逻辑的保守扩展。

从公式到可计算性逻辑中的电路

From formulas to cirquents in computability logic

可计算性逻辑（Computability Logic，CoL）（参见http：//www.cis.upenn.edu/cnigiorgi/cl.html）是一个最近引入的语义平台和雄心勃勃的计划，用于将逻辑重新发展为可计算性的形式理论，而不是逻辑传统上的形式真值理论。它的表达式代表了交互式计算任务，被视为机器与环境的游戏，而“真理”被理解为算法获胜策略的存在。CoL的形式主义是开放式的，并且已经经历了一系列的扩展，其中逻辑运算符代表了对游戏的操作。本文以一种全新的方式扩展了CoL的表达能力，将公式（CoL的早期语言仅限于此）推广到称为cirquents的电路式结构。与公式不同，后者能够解释整个游戏/任务的不同部分之间的子游戏/子任务共享。这种能力所提供的许多优点之一是，它允许我们捕获、提炼和概括众所周知的独立友好逻辑，在目前的飞跃之后，它自然成为CoL的保守片段，就像经典逻辑被认为是CoL的基于公式的版本的保守片段一样。并且可以在不熟悉CoL的情况下阅读。

命题可计算性逻辑II

Propositional Computability Logic II

可计算性逻辑是关于计算任务和资源的形式化理论。它的公式代表交互式计算问题，逻辑运算符代表计算问题的运算，公式的有效性被理解为总是有算法解决方案的问题的方案。关于这一主题的全面在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上查阅。早期的文章“命题可计算性逻辑I”证明了可计算性逻辑的最小非平凡片段CL1的可靠性和完备性。本文将这一结果扩展到更有表现力的命题系统CL2。使CL2比CL1更具表达力的是其语言中存在两种原子：基本原子，表示基本计算问题（即谓词），以及一般原子，表示任意计算问题。CL2保守地扩展了CL1，后者只是前者的一般无原子片段。

Fundamentals of computability logic 2020

This article is a semitutorial-style survey of computability logic. An extended online version of it is maintained at http://www.csc.villanova.edu/~japaridz/CL/ .

可计算性逻辑综述

A survey of computability logic

本文介绍了可计算性逻辑的概况：它的哲学和动机，主要概念和迄今为止取得的最重要的成果。这篇文章的持续更新的在线版本在http://www.csc.villanova.edu/~japaridz/CL/上维护。

从真理到可计算性

From truth to computability I

可计算性逻辑是最近提出的一种交互计算的形式化理论。有关该主题的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html。本文包含了一个合理性和完整性证明的演绎系统CL3公理化的最基本的一阶片段的可计算性逻辑称为有限深度，元素基片段。这一结果的潜在应用领域包括交互计算理论、建设性应用理论、知识库系统、资源约束规划和行动系统。本文件是自成一体的，因为它重新介绍了所有相关定义以及主要动机。

可计算性逻辑中的可数与不可数分支递归

The countable versus uncountable branching recurrences in computability logic

本文介绍了可计算逻辑中可数分支递归的一种新的简化形式，证明了它与旧的可计算逻辑的等价性，并指出由它导出的基本逻辑是由不可数分支递归导出的基本逻辑的真超集。本文的一个进一步的结果是：可数分支递归式严格弱于不可数分支递归式，因为后者逻辑上蕴涵前者，而不是前者逻辑上蕴涵后者.

一开始是游戏语义学

In the beginning was game semantics

本文概述了可计算性逻辑--交互式计算任务和资源的游戏语义构造逻辑。只有一个非概述，在它的技术部分，致力于证明健全的仿射逻辑方面的语义可计算性逻辑。有关该主题的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到

可计算性逻辑：给凯撒属于凯撒的东西

Computability logic: Giving Caesar what belongs to Caesar

本文是一个简短的非正式调查的可计算性逻辑-游戏语义构思的形式理论的计算资源和任务。这种相对年轻的非经典逻辑是经典一阶逻辑的保守扩展，但比后者更具表现力，产生了广泛的新的潜在应用领域。在一个合理的（即使不是严格的）意义上，直觉主义和线性逻辑也是如此，这使我们可以说CoL在其自然和“普遍”的游戏语义学基础上调和和统一了逻辑思维的三个传统（以及超越）。关于这个问题的全面在线调查可以在http://www.csc.villanova.edu/~japaridz/CL/上找到。

可计算性逻辑中的并行递归与分支递归

The parallel versus branching recurrences in computability logic

本文证明了可计算性逻辑的并行递归导出的基本逻辑是分支递归导出的基本逻辑的真超集。后者被称为精确捕获的cirquent演算系统CL 15，由Japaridze保持健全--但不完整--与平行递归，而不是分支递归。目前的结果是通过积极验证该猜想。第二个结果的文件表明，平行递归是严格弱于分支递归的意义上说，而后者在逻辑上意味着前者，反之亦然不成立。

可计算逻辑的PSPACE-完全一阶片断

A PSPACE-Complete First Order Fragment of Computability Logic

在最近启动的一个研究计划，发展逻辑作为一个正式的理论（互动）可计算性，几个非常有趣的逻辑已被介绍和公理化。这些更大的可计算性逻辑的片段不仅旨在描述“什么”可以计算，而且还提供了一种从证明中提取计算算法的机制。其中最具表现力和基础的是CL 4，已知是（建设性的）健全和完整的基础计算语义。进一步证明了CL 4中不含盲量词的片段在多项式空间中是可判定的。目前的工作扩展了这一结果，并证明了该片段，事实上，PSPACE完成。

用可计算性逻辑尽可能简洁地表达算法

Expressing Algorithms As Concise As Possible via Computability Logic

本文提出了一种新的算法定义和表示方法：{ \it任务逻辑}算法的概念。此概念允许用户将任务$T$的算法定义为可以共同执行$T$的一组代理。这个概念大大简化了算法开发过程，可以看作是顺序伪代码和逻辑算法的集成。这一观察结果需要对算法开发过程进行一些更改。我们提出了一个两步的方法：第一步是定义一个算法的任务$T$通过一组代理，可以共同执行$T$。第二步是将这些代理转换为（高阶）可计算性逻辑。

PECR：基于可计算性逻辑的形式系统

PECR: A formal system based on computability logic

PECR是一个基于可计算性逻辑的形式系统，通过整合机器有限资源来探索程序可计算性，并应用于自然法则研究以严格构建真实世界现象的计算机模型。

建构系统的逻辑基础

A logical basis for constructive systems

这项工作致力于可计算性逻辑（CoL）-哲学/数学平台和长期项目，用于在其底层语义中用可计算性取代真理之后重新开发经典逻辑（见http：//www.cis.upenn.edu/paggiorgi/cl.html）。本文阐述了CoL框架的一些基本复杂性理论。然后证明了演绎系统CL 12关于CoL语义的可靠性和完备性，包括后者基于多项式时间可计算性而不是原则上可计算性的版本。CL 12是一个微积分系统，其中一个变量的含义直观上可以被描述为“后继变量可以在算法上还原为先行变量”，并且其中公式是由谓词字母、函数字母、变量、常数、恒等式、否定式、平行和选择连接词以及盲量词和选择量词构建的。一个案例是CL 12是一个足够的逻辑基础建设性的应用理论，包括复杂性导向的。

量子一阶逻辑：刻画对数时间/空间量子可计算性

Quantum First-Order Logics That Capture Logarithmic-Time/Space Quantum Computability

本文提出量子一阶逻辑（QFO），通过特殊量子连接词和量词及函数式量子变量，刻画有界误差量子对数时间可计算性，并借助量子传递闭包算子表征量子对数空间可计算性。

非阿耳特里亚有限逻辑中的实分析和可计算性理论的基础

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的重要潜在应用是在量子和自主计算领域。

Axiomatizations and Computability of Weighted Monadic Second-Order Logic

Weighted monadic second-order logic is a weighted extension of monadic second-order logic that captures exactly the behaviour of weighted automata. Its semantics is parameterized with respect to a semiring on which the values that weighted formulas output are evaluated. Gastin and Monmege (2018) gave abstract semantics for a version of weighted monadic second-order logic to give a more general and modular proof of the equivalence of the logic with weighted automata. We focus on the abstract semantics of the logic and we give a complete axiomatization both for the full logic and for a fragment …

有效AGM信念收缩：超越有限领域的旅程（技术报告）

Effective AGM Belief Contraction: A Journey beyond the Finitary Realm (Technical Report)

该研究探讨非有限逻辑中AGM信念收缩的可计算性，发现不可计算性普遍存在且现有策略失效，提出基于Büchi自动机的LTL可计算收缩函数新方法。

关于无限树正则集合测度的可计算性

On the Computability of Measures of Regular Sets of Infinite Trees

本文研究无限树上一元二阶逻辑的概率可满足性问题，提出计算随机树满足给定公式概率的方法，并证明该概率为代数数，从而将此前仅适用于较弱形式体系的结果推广到完整一元二阶逻辑。

一种研究分布式任务可计算性的动态认知逻辑单纯形复合模型

A Simplicial Complex Model for Dynamic Epistemic Logic to study Distributed Task Computability

多智能体系统的通常认知模型S5n是基于Kripke框架的，Kripke框架是一个图，其边缘用不区分两种状态的智能体标记。我们建议通过考虑一个对偶的单纯复杂模型来揭示这个结构中隐含的高维信息。我们使用动态认识逻辑（DEL）来研究认识单纯复模型在一组主体相互通信后如何变化。我们专注于一个动作模型，表示异步代理的所谓的即时快照通信模式，因为它是分布式可计算性的核心（但我们的设置适用于其他通信模式）。从最初的认知复合体到应用动作模型后的认知复合体，存在拓扑不变量，这些拓扑不变量决定了主体在通信后获得的知识。最后，我们描述了如何分布式任务规范可以建模为一个DEL动作模型，并表明，拓扑不变量确定任务是否是可解的。因此，我们提供了一个桥梁DEL和分布式可计算性的拓扑理论，研究任务的可解性在一个共享的内存或消息传递架构。

肥沃的草原：可计算性逻辑及其一个片段的可判定性

The Fertile Steppe: Computability Logic and the decidability of one of its fragments

本文系统介绍可计算性逻辑（CoL）及其核心语义、语法和 Cirquent Calculus 证明系统，并针对其公理化系统 CL15 给出可判定性的尝试性证明，同时探讨其在算术与人工智能中的应用价值。

循环演算和抽象资源语义学导论

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的可靠性和完整性。

自复制的代数

Algebra of Self-Replication

本文提出使用可通过项重写判定的极小等式逻辑来检验可计算性理论，并对两个可判定片段中的 quine 程序进行分类，解释了其本质相似性。

关于传递模态多值逻辑

On Transitive modal many-valued logics

本文主要研究由赋值Kripke框架定义的模态逻辑，特别是在某些剩余格上赋值传递Kripke框架的模态逻辑的可计算性和可表示性问题。它表明，一个大家庭的这些逻辑-包括所产生的标准MV和产品代数-产生一个不可判定的后果关系。随后，传递模态Lukasiewicz逻辑的行为进行了比较，它的非传递对应，展示了一些细节有关的可计算性和等价与其他逻辑。最后，我们展示了不可判定性的有效性和局部SAT问题的传递模型时，Delta操作添加到逻辑。

算法归约的多概念和两种逻辑

Many concepts and two logics of algorithmic reduction

在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到

Logical Pseudocode: Connecting Algorithms with Proofs

Proofs (sequent calculus, natural deduction) and imperative algorithms (pseudocodes) are two well-known coexisting concepts. Then what is their relationship? Our answer is that \[ imperative\ algorithms\ =\ proofs\ with\ cuts \] This observation leads to a generalization to pseudocodes which we call {\it logical pseudocodes}. It is similar to natural deduction proof of computability logic\cite{Jap03,Jap08}. Each statement in it corresponds to a proof step in natural deduction. Therefore, the merit over pseudocode is that each statement is guaranteed to be correct and safe with respect to the i…

初等基圆积分I：平行和选择连接词

Elementary-base cirquent calculus I: Parallel and choice connectives

循环演算是一个证明系统，操纵循环风格的结构，而不是公式。利用它，本文构建了可计算性逻辑命题片段（计算问题的博弈语义构想逻辑，见http://www.csc.villanova.edu/~japaridz/CL/）的一个合理而完整的公理化CL 16，其逻辑词汇由否定、平行和选择连接词组成，其原子表示基本的，即无移动的博弈。

Clarithmetic I介绍

Introduction to clarithmetic I

“Clarithmetic”是一个与皮亚诺算术类似的形式数论的通用名称，但基于可计算性逻辑（参见http：//www.cis.upenn.edu/classgi/cl.html），而不是更传统的经典或直觉逻辑。claithmetical理论的公式代表交互式计算问题，它们的“真理”被理解为算法解的存在。对这些解决方案施加各种复杂性约束会产生各种版本的clarithmetic。本文介绍了一个多项式时间可计算性的算法体系，该体系是完善的。在这个意义上，系统的每个定理T都代表一个具有多项式时间解的交互数论计算问题，而且，这样的解可以有效地从T的证明中提取出来。完备性的意义在于，每一个具有多项式时间解的交互数论问题都由系统的某个定理T表示。这篇论文是写在semitutorial风格和目标读者事先不熟悉可计算性逻辑。

高阶终止性：从Kruskal到可计算性

Higher-Order Termination: from Kruskal to Computability

终结性是逻辑学和计算机科学中的一个重要问题。在逻辑中，终止是证明理论的核心，通常被称为强规范化（切割消除）。在计算机科学中，终止性一直是表明程序正确性的一个重要问题。在早期的逻辑中，强规范化通常通过将序数分配给表达式来显示，以这种方式消除切割将产生具有较小序数的表达式。在验证的早期，计算机科学家使用了类似的想法，通过自然数（例如大小）来解释程序调用的参数。显示每个递归调用的参数的大小减少给出了程序的终止证明，然而这是相当弱的，因为它只能产生相当小的序数。在六十年代，泰特发明了一种新的方法来显示自然演绎的切割消除，基于项集合上的谓词，使得表达式对谓词的成员关系暗示了该表达式的强规范化属性。谓词是通过类型上的归纳定义的，或者甚至是作为一个不动点，这种方法可以产生更大的序数。后来Girard以约简或可计算性候选人的名义推广了它，它在证明类型化可达演算的强规范化性质方面表现得非常有效。

实现从CL1-proofs中提取程序

Implementing program extraction from CL1-proofs

可计算性逻辑（Computability Logic，CoL）是一种交互计算的形式化理论。它将计算问题理解为两个玩家的游戏：机器和它的环境，使用逻辑形式主义来描述有效的可计算性原则和公式来表示计算问题。逻辑CL1是CoL的一个片段的演绎系统，逻辑词汇表包含了经典逻辑的所有算子和选择算子，原子表示经典逻辑的基本博弈即谓词。在本文中，我们提出了一个程序，采取CL1证明的任意公式$F$，并提取一个获胜的策略，$F$从证明，然后发挥$F$使用该策略。我们希望本文将提供一个起点，进一步的工作，在程序提取的CoL为基础的算法和其他CoL为基础的应用系统。