A generalization of falsity in finitely-many valued logics
本文提出了多值逻辑中的一种新的否定类型，为回答以下问题提供了一种不同的方法：某个对象语言公式不具有给定的真值意味着什么？在此过程中，本文给出了任意多值逻辑中真与假的一般定义。
2022-03-31 cs.LO
Rational fuzzy attribute logic
我们提出了一个逻辑推理的if-then公式，其中涉及常数的合理的真度从单位区间。我们引入了公式的分级语义和句法蕴涵。我们证明了该逻辑是Pavelka风格的完备逻辑，并且根据真度结构的选择，该逻辑是RationalPavelka逻辑（RPL）或RationalProductLogic（RPL）的可判定片段。我们还提出了一个基于最小模型的蕴涵的特征，并研究了相关的闭包结构。
2015-02-25 cs.LO
Epistemic extensions of combined classical and intuitionistic propositional logic
逻辑$L$是由Lewitzka [7]引入的，作为一个结合了直觉主义和经典逻辑的模态系统：$L$是CPC的保守扩展，它通过嵌入$φ\mapsto\squareφ$包含IPC的副本。在这篇文章中，我们考虑$L3$，即$L$增广与S3模态公理，定义基本的认知扩展和证明完全性w.r.t.代数语义学由此产生的逻辑结合了经典知识和信仰与直觉真理。阿特莫夫和普罗波佩斯库[1]所研究的直觉主义认识逻辑的一些认识规律反映在经典模态原理中。特别是，“直觉真理$\Rightarrow$知识$\Rightarrow$经典真理”的影响是由我们的逻辑$EL3$的定理$\squareφ\rightarrow Kφ$和$Kφ\rightarrowφ$表示的，在这里我们处理的是经典而不是直觉知识。最后，我们表明，修改我们的语义产生代数模型的直觉主义认知逻辑系统介绍了[1]。
2017-02-27 cs.LO
Resolution in Linguistic First Order Logic based on Linear Symmetrical Hedge Algebra
本文研究了真值取自线性对称对冲代数的语言一阶逻辑的归结问题。我们建立语言一阶逻辑的基本组成部分，包括语法和语义。我们提出了一个解决原则，我们的逻辑解决两个子句具有矛盾的语言真值。由于语言信息是不确定的，语言逻辑中的推理是近似的。因此，我们引入了可靠性的概念，以捕捉自然近似的归结推理规则。
2014-03-30 cs.LO
A Fuzzy Logic Programming Environment for Managing Similarity and Truth Degrees
FASIL（“Fuzzy Aggregators and Similarity Into a Logic Language”的缩写）是一种模糊逻辑程序设计语言，具有隐式/显式真度注释、大量的连接词和相似性统一。FASIL集成并扩展了MALP（Multi-Adjoint Logic Programming，一种带有显式注释规则的模糊逻辑语言）和Bousi~Prolog（使用弱统一算法，非常适合灵活的查询应答）的功能。因此，它在一个框架中适当地管理相似性和真度，结合了两种语言的表达优势。本文介绍了FASILL的主要功能和实现细节。沿着该文件，我们描述了它的语法和操作语义，我们给出了线索的实施格模块和相似性模块，两个主要的构建块的新的编程环境，丰富了FLOPER系统在我们的研究小组开发。
2015-01-09 cs.LO cs.PL
Implicit definability of truth constants in Łukasiewicz logic
本文在命题逻辑的框架下，引入了一个合适的隐式可定义性概念，该概念适合于预定的实值语义，并涉及其域的元素。探讨了标准语义学中隐式定义每个理性元素的几种变体，并在此基础上得到了RationalPavelka逻辑中的理论在RationalPavelka逻辑中的忠实解释。其中一些结果已经在哈耶克的《模糊逻辑的元数学》中作为技术陈述提出。一个连接到缺乏（演绎）Beth属性在Eschukasiewicz逻辑。此外，虽然标准语义学的无理元素不能用有限的方法隐式地定义，但它们在无限的Rukasiewicz逻辑中的平行发展是可能的。作为一个应用程序的可定义性的理性，它显示了如何计算复杂性的结果，理性Pavelka逻辑可以得到类似的结果为Rankukasiewicz逻辑。可定义性概念本身的复杂性也进行了研究。最后，我们回顾了这些结果对于模糊逻辑的精确性/精确性讨论的重要性，以及对于真值常数在Eukasiewicz逻辑中的一般地位的重要性。
2018-02-23 cs.LO math.LO
A Lindström Theorem for Fitting's Modal Logic over a Finite Heyting Algebra
Department of Mathematics, Mahishadal Raj College（马希沙达尔学院数学系）
该研究针对Maruyama提出的带精确真值测试的Fitting有限Heyting值模态逻辑，建立Lindström极大性定理，证明满足紧致性、Tarski并性质及互模拟强不变的抽象扩展与原逻辑表达等价，且扩展公式的精确值纤维可被定义。
2026-08-18 cs.LO
Resolution in Linguistic Propositional Logic based on Linear Symmetrical Hedge Algebra
本文介绍了一个命题语言逻辑，作为自动不确定推理的语言信息的基础。首先，我们建立了一个基于线性对称对冲代数的真值域语言逻辑系统。然后，我们考虑哥德尔的t-范数和t-连接词来定义我们逻辑的逻辑连接词。接下来，我们提出了一个决议推理规则，其中两个条款有矛盾的语言真值可以解决。我们还给出了可靠性的概念，以捕捉的近似性质的决议推理规则。最后，我们提出了一个解决方案的最大可靠性。
2013-07-30 cs.LO
Necessity as justified truth
我们提出了一个逻辑推理的必要性和理由，这是独立于关系语义。我们选择理由的概念-来自一类“理由逻辑”（Artemov 2008，Fitting 2009）-作为必要性概念所基于的原始概念。我们的公理化扩展了Suszko的非Fregean逻辑SCI（布朗，Suszko 1972）的基本公理从证明逻辑，公理量化的命题和理由，以及一些进一步的原则。核心公理是：$φ$必然为真当且仅当存在$φ$的证明。也就是说，必要性是可以通过证明来一阶定义的。而不是定义纯粹的代数模型（布朗，Suszko 1972）的风格，我们扩展了语义研究（Lewitzka 2012）的一些代数结构处理的理由，并证明我们的演绎系统的可靠性和完整性。此外，如果我们将公理模式$\squareφ\to \square\squareφ$和公理必然性规则加入到我们的系统中，我们就能够恢复模态逻辑的必然性原则。作为主要结果，我们表明，模态逻辑S4和S5可以捕获我们的语义，如果我们施加相应的模态逻辑原则作为额外的语义约束。这将遵循从证明理论的考虑和我们的完备性定理。对于系统S4，我们也给出了一个纯模型论的证明。
2012-06-03 cs.LO
Differentiable Probabilistic Logic Networks
SingularityNET Foundation（SingularityNET基金会）；ITMO University（ITMO大学）
概率逻辑推理是OpenCog等认知架构的核心组件。然而，作为一个综合架构，OpenCog通过混合不同的推理方法促进认知协同。在本文中，我们介绍了一个可微版本的概率逻辑网络，规则操作张量真值的方式，一个链的推理步骤构建一个计算图的张量，接受真值的前提知识库作为输入，并产生真值的结论作为输出。这允许通过结合子符号优化和符号推理的反向传播来学习前提的真值和规则的公式（以具有可训练权重的形式指定）。
2019-07-10 cs.AI cs.LO
Rational Pavelka logic: the best among three worlds?
这一比较调查探讨了三种正式的推理方法与部分真实的陈述和程度的真理，在家庭的Rukasiewicz逻辑。这些方法由无限值Rukasiewicz逻辑（RPL）、理性Pavelka逻辑（RPL）和我们称为分级理性Pavelka逻辑（GRPL）的具有分级公式的逻辑表示。在$0$和$1$之间的所有有理数的真值常数被用作校准真度的技术手段。除了$0$和$1$之外，RationalPavelka逻辑表面上没有真值常数; RationalPavelka逻辑在基本语言中包含常数，并有合适的公理; GradedRationalPavelka逻辑使用分级公式和证明，遵循Pavelka的初衷，受到Goguen工作的启发。从历史上看，Pavelka的论文先于GRPL的定义，而GRPL又先于RPL;检索这些步骤，我们讨论了这些形式系统如何自然地相互演变，我们还记得这个过程是如何在Eukasiewicz逻辑领域中引起争议的。这部作品也可以被解读为逻辑学、逻辑碎片以及逻辑碎片之间关系的案例研究。
2021-12-13 cs.LO math.LO
Dunn Semantics for Contra-Classical Logics
在本文中，我展示了丰富的和系统化的饮食的例子，许多反经典逻辑可以作为FDE的变体，通过修改某些连接的真或假条件中的至少一个来获得。然后，我认为，使用邓恩语义学提供了一个清晰的理解的反经典性的来源，即，连接词，要么有经典的真理或经典的虚假条件的另一个连接。这需要对可以对评估条件进行的各种修改进行细粒度的分析，我在这里也提供了这种分析。
2022-04-14 cs.LO
How to Agree without Understanding Each Other: Public Announcement Logic with Boolean Definitions
在标准的认知逻辑中，知道p等于知道p是真的，但它并没有说理解p或知道它的意义。在本文中，我们提出了一个保守的公共公告逻辑（PAL）的扩展，其中代理人有知识或信念的真值和命题的意义。我们给出了一个完整的公理化PAL布尔定义，并讨论了各种例子。一个主体可能理解一个命题而不知道它的真值，或者反过来。此外，多个代理人可以就某件事达成一致，但不同意其含义，反之亦然。
2019-07-22 cs.LO
Modal Logics -- RNmatrices vs. Nmatrices
本文比较了模态逻辑中非确定性语义与受限非确定性语义的异同，并以MK、MKT和MKT4为例说明后者能更统一地构造最小模态逻辑M的扩张，同时讨论了两者的现有局限。
2024-12-31 cs.LO
A Pragmatic Interpretation of Quantum Logic
长期以来，学者们一直想知道，量子力学的语言是否引入了一种由量子逻辑（QL）形式化的、与经典（塔斯基）概念不相容的量子真理概念。我们表明，QL可以被解释为一个务实的语言的断言公式，正式声明的物理系统，经验证明或不合理的量子力学的框架。根据这种解释，QL在量子力学中形式化了经验证明的元语言概念的属性，而不是真理的量子概念的属性。这一结论与一般的整合主义观点一致，即把非标准逻辑解释为不同于真理的元语言概念的理论，从而避免了与经典概念的不相容，并保持了逻辑的整体性。同时，对量子真理的标准概念也作了一些说明。关键词：语用学、量子逻辑、量子力学、可解释性、全球多元主义。
2015-12-16 cs.LO quant-ph
Truth and Preferences -- A Game Approach for Qualitative Choice Logic
TU Wien（维也纳工业大学）；Institute of Logic and Computation（逻辑与计算研究所）
在本文中，我们介绍了博弈论语义（GTS）的定性选择逻辑（QCL），为了表达偏好，扩展了经典的命题逻辑与一个额外的连接称为有序析取。首先，我们证明了游戏语义可以捕获现有的程度为基础的语义QCL在一个自然的方式。其次，我们表明，游戏语义可以利用QCL的语言派生新的语义。特别是，我们提出了一个新的语义，利用GTS否定，并通过这样做，避免在现有的QCL语义否定的问题。
2022-09-27 cs.AI cs.LO math.LO
A Completeness Proof for A Regular Predicate Logic with Undefined Truth Value
我们提供了一个健全的和完整的证明系统Kleene的三元逻辑谓词的扩展。理论的概念是扩展的，对于每个函数符号，一个公式，指定何时定义的功能。“被定义”的概念通过一个简单的递归算法扩展到术语和公式。“已定义”公式的构造使得它们本身总是已定义的。完整性证明依赖于Henkin构造。对于每一个公式，公式、它的否定和它的“被定义”公式的否定之一在构造的模型上是真的。许多其他三进制逻辑在文献中可以减少到我们的。部分函数在计算机科学中无处不在，甚至在学校的方程求解中也是如此。我们的工作的动机是试图解释，正是在逻辑方面，典型的非正式方法的推理，在这样的应用。
2023-03-26 cs.LO math.LO
Dialetheism, Game Theoretic Semantics, and Paraconsistent Team Semantics
我们介绍了一个变体的依赖逻辑中的真理定义不存在的获胜策略的支持者（Eloise）在语义游戏中，但在缺乏获胜策略的对手（Abelard）。我们证明了这种语言是一阶逻辑的保守但次协调的扩展，它的有效性问题可以归结为一阶逻辑的有效性问题，它能够表达自己的真值和有效性谓词，并且它在表达上等价于通用二阶逻辑。此外，我们证明了一个次协调的非依赖逻辑公式是一致的当且仅当它是等价于一些一阶逻辑句子;另一方面，我们表明，所有的次协调依赖逻辑句子等价于一些一阶句子就真（但不一定就假）。
2014-03-14 cs.LO math.LO
Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
Lightcap；Bahcesehir University（巴赫切塞希尔大学）
本文提出Truth-Aware Decoding（TAD），一种基于程序逻辑的验证导向解码方案，通过语义守卫格约束生成过程，在保持吞吐量的同时减少幻觉，并提供了理论证明与Lean形式化验证。
2025-10-03 cs.AI 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
Essence and accident modalities meet Belnapian truth values
University of Lodz（罗兹大学）
本文在贝尔纳普-邓恩四值逻辑FDE上推广本质与偶然模态，定义本质/偶然真、假、不一致和不确定模态，给出四值S5克里普克语义及无切超相继式演算，并证明嵌入定理，获得可靠、完全和切消除结果。
2026-10-07 cs.LO math.LO
Nonclassical truth with classical strength. A proof-theoretic analysis of compositional truth over HYPE
关于经典与非经典真理理论的证明论强度的问题最近受到了一些关注。一个特别方便的案例研究涉及经典和非经典公理化的不动点语义。众所周知，四值或三值逻辑中的非经典公理化比经典公理化弱得多。在本文中，我们考虑增加一个合适的条件，一级蕴涵-最近研究的Hannes Leitgeb的标签下的“HYPE”的逻辑。我们特别表明，通过制定理论PKF HYPE得到一个理论，这是健全的固定点模型，而被证明理论上等同于其经典的对应KF。此外，我们还建立了它的示意性扩展-在Feferman的意义上-是强大的KF的示意性扩展，从而匹配的强度预测分析。
2020-08-13 cs.LO math.LO
Axiomatizing logics of fuzzy preferences using graded modalities
本文的目的是提出一个多值模态框架，形式化推理与分级偏好和命题，在风格的范Bentham等人。的经典模态逻辑偏好。为此，我们从Bou et al.的最小模态逻辑。然后，我们定义适当的扩展多模态语言与分级模态，无论是弱和严格的偏好，并与真值常数。实际上，语言中真值常量的存在使我们能够证明最小模态逻辑的模态算子Box和Diamond是可互定义的。最后，我们提出了一个公理系统，这个逻辑在一个扩展的语言（其中的偏好模态运算符是可定义的），并证明了完整性方面的预期分级偏好语义。
2019-11-15 cs.LO math.LO
An Algebraic Semantics for Possibilistic Logic
University of Padova（帕多瓦大学）
本文的第一个贡献是提出了一个类似Pavelka的可能性逻辑公式，其中语言自然地被两个表示否定的连接词（eg）和一种新型的连接词（otimes）所丰富。这个逻辑的真值空间是可能性函数的格，从代数的角度来看，它形成了一个量子。第二个贡献来自于对新连词的理解，它是来自不同来源的信息标记的组合，这使得我们的语言“动态”。给出了一个Gentzen演算，证明了它在给定的语义下是完备的。真值函数的问题在此背景下进行了讨论。
2013-02-20 cs.AI cs.LO
About Algorithm for Transformation of Logic Functions (ATLF)
本文研究了由真值表给出的逻辑函数的变换算法。所建议的算法允许变换的多值逻辑函数所需的变量数，并可以在这个意义上被看作是普遍的。
2007-12-08 cs.AI cs.LO
Internal Reasoning and Consistency in Reflective Grounded Arithmetic
EPFL（洛桑联邦理工学院）
本文在Isabelle/HOL中开发了经机器验证的RGA系统，定义了其内在真谓词，完成相关元定理闭合，证明RGA是支持非平凡数学推理的可行形式系统。
2026-10-27 cs.LO cs.PL math.LO
Minimum Model Semantics for Logic Programs with Negation-as-Failure
我们给出了一个纯粹的模型理论表征的语义逻辑程序与否定作为失败允许在条款机构。在我们的语义程序的意义是，在经典的情况下，唯一的最小模型在一个程序独立的顺序。我们使用一个扩展的真值域，它在False（最小值）和True（最大值）之间有一个不可数的线性有序真值集，中间有一个零元素。低于零的真值像可数序数一样排序。大于零的值的顺序正好相反。否定被解释为关于零的反射，然后是向零的一步;唯一不受否定影响的真值是零。我们证明了每个程序都有唯一的极小模型M_P，并且这个模型可以用T_P迭代来构造，T_P迭代是通过可数序数进行的。此外，我们还证明了M_P也可以通过一个模型交构造来获得，该构造推广了经典逻辑程序设计中著名的模型交定理。最后，我们证明了通过将无穷值模型M_P的真值和假值折叠为（经典的）真值和假值，我们得到了一个与良基模型相同的三值模型。
2003-06-03 cs.AI cs.LO cs.PL
On existential declarations of independence in IF Logic
我们分析了IF句中的量词前缀中存在量词之间的独立性声明行为，给出了一个句法判据，用以判定是否存在以该前缀开头的句子，使得其真假值的独立性声明的去除可能会影响该句子的真值。我们的结果还扩展到平衡语义值为未定的IF句子。主要定理使我们能够描述各种特定类别的量词前缀的行为，并证明作为一个显着的推论，所有存在的IF句子是等价于一阶句子。作为进一步的结果，我们证明了与知识记忆的IF句子片段只有一阶的表达能力（真理等价）。
2012-05-11 cs.LO math.LO
Modal Logic via Global Consequence
在模态逻辑中，语义结果通常由所有模型中所有世界的真值保持局部定义（关于一类框架）。它也可以通过在所有模型中保持真值来全局定义（相对于一类框架）。后者被称为整体后果，这是远远低于标准的局部研究。本文首先研究了局部推论和整体推论之间的关系。然后给出了整体结果的一些对应结果。最后，结合形式语义学中的信息推理和更新推理，给出了全局推理的两个应用。本文中的一些结果是已知的，为了完整起见，将其收集在本文中。其他人似乎是新的。我们认为，整体结果不仅在理论上是有趣的，而且在应用上也是有用的。
2019-10-06 cs.LO math.LO
Queries With Exact Truth Values in Paraconsistent Description Logics
Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800（波尔多大学、国家科学研究中心、波尔多INP、LaBRI、UMR 5800）；Japanese-French Laboratory for Informatics, CNRS, NII, IRL 2537（日法信息实验室、国家科学研究中心、日本信息机构、IRL 2537）；DI ENS, ENS, CNRS, PSL University & Inria, Paris, France（ENS DI、巴黎高等师范学院、国家科学研究中心、巴黎科学实验室与Inria、法国巴黎）
本文在准协调描述逻辑中引入四值Belnapian语义和真值算子以区分矛盾证据与正面证据，并通过归约到经典DL查询应答精确刻画了查询复杂度，证明Horn DL保持可处理的数据复杂度。
2024-08-15 cs.AI cs.DB cs.LO
Vector logic allows counterfactual virtualization by The Square Root of NOT
Universidad de la República（共和国大学）；Facultad de Ciencias（理学院）
在这项工作中，我们调查的表示使用向量逻辑，矩阵向量形式主义的逻辑函数和真值的反事实条件。在这种形式主义中，反事实可以被转换成复矩阵，用NOT的平方根之一（复矩阵）预处理蕴涵矩阵。这种数学方法证明了反事实的虚拟性。这是因为这种表示产生了一个反事实的估值，即由两个复共轭系数分别加权的两个相反真值的叠加。这一结果表明，该过程给出了一个不确定的评估投射在复杂的域。在这个基本表征之后，对给定反事实的可接受性的判断允许我们将决定转向接受或拒绝。这个移位是第二次应用NOT的两个平方根之一的结果。
2020-09-01 cs.CL 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
Logic Embeddings for Complex Query Answering
IBM Research（IBM研究院）
在不完整的知识库上进行逻辑查询是具有挑战性的，因为：1）它要求隐式链接预测，以及2）存在一阶逻辑查询的蛮力应答在存在变量的数量上是指数的。近年来的查询嵌入方法提供了快速查询的能力，但大多数方法都是用封闭区域来建模集合逻辑，缺乏否定性。支持否定的查询嵌入使用的密度存在缺点：1）只能即兴发挥逻辑，2）使用昂贵的分布，3）对答案的不确定性建模不佳。在本文中，我们提出了逻辑嵌入，一种新的方法来嵌入复杂的查询，使用Skolemisation消除存在的变量进行有效的查询。它支持否定，但改进了密度方法：1）集成了研究良好的t-范数逻辑并直接评估可满足性，2）简化了真值建模，3）用真值界建模不确定性。逻辑嵌入在对大的、不完整的知识图谱的查询应答中具有竞争力的快速和准确性，在否定查询上优于否定查询，并且特别地，提供了对答案不确定性的改进的建模，如答案集大小和嵌入熵之间的优越相关性所证明的。
2021-02-28 cs.AI cs.DB cs.LG
Mediative Fuzzy Logic: From Type-1 Foundations to Type-2, Type-3 and Quantum Extensions
Instituto Politécnico Nacional - CITEDI（墨西哥国家理工学院- CITEDI）
本文提出中介模糊逻辑的统一框架，通过中介算子处理犹豫和矛盾，建立从类型-1到类型-2、类型-3及量子扩展的语义基础，并证明其可靠性和保守性。
2026-05-21 cs.AI cs.LO quant-ph
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
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
