Which are the True Defeasible Logics?
本文探讨了可废止逻辑的模糊定义问题，基于新引入的可废止逻辑 $DL(\partial_{||})$ 的特征，定义了一类既能容纳新逻辑又保留传统可废止逻辑性质的逻辑类。
2024-05-29 cs.LO
Decidability of an Expressive Description Logic with Rational Grading
本文考虑了描述逻辑中实现理性分级的句法对象-概念构造子，即部分限制。部分限制能够表达关于后继集合的合理部分的语句，从本质上丰富了DL的表达能力。我们研究了一个扩展的研究DL ALCQIHR+部分限制，并证明了在扩展逻辑的推理仍然是可判定的。证明使用表格技术与指数技术，旨在处理部分限制。
2019-05-24 cs.LO
Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules
我们的手稿研究线性时间（与UNTIL和NEXT）逻辑的基础上的概念不传递时间。非传递时间特别是，我们展示了如何在这样的框架中表示知识的概念（在这里，我们认为逻辑操作NN和操作UNTIL（实际上，时间整体）是针对过去）。我们研究的基本数学问题是任何逻辑系统的基本问题-可判定性和可判定性w.r.t.可接受的规则首先，我们考虑具有非一致非传递性的逻辑，并描述如何解决这种逻辑的可判定性问题。然后，我们考虑了这种逻辑的一种修改--具有一致不传递性的线性时态逻辑，并解决了推理规则的可容许性问题。在论文的结论部分列举了一系列有待解决的问题。
2015-03-30 cs.LO
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
2009-02-12 cs.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
Axiomatizations of Team Logics
在一个模块化的方法，我们提升希尔伯特式证明系统的命题，模态和一阶逻辑广义系统为各自的团队为基础的扩展。我们对Väänänen的一阶群逻辑TL的无依赖片段FO（~），命题群逻辑PTL，量化命题群逻辑QPTL，模态群逻辑MTL，以及相应的依赖、独立、包含和排除逻辑，得到了合理而完整的公理化.作为完备性证明的关键步骤，我们证明了上述逻辑在某种意义上承认从公式中消除模态和量词的语义保持性。
2018-03-26 cs.LO
On an ecumenical natural deduction with stoup -- Part I: The propositional case
由Gentzen提出并由Prawitz进一步研究的自然演绎系统是最著名的证明理论框架之一。它的成功部分是基于这样一个事实，即自然演绎规则呈现了逻辑常数的简单表征，特别是在直觉主义逻辑的情况下。然而，为了处理经典逻辑而对直觉规则集进行扩展的做法受到了很多批评。事实上，大多数这样的扩展都在通常的引入和消除规则之外增加了管理否定的额外规则。因此，几个元逻辑属性，最突出的一个是和谐，失去了。Dag Prawitz提出了一个自然演绎的普世体系，其中经典逻辑和直觉主义逻辑被编入同一个体系。在这个系统中，古典主义逻辑学家和直觉主义逻辑学家将共享全称量词、合取词、否定词和荒谬的常量，但他们各自有自己的存在量词、析取词和蕴涵词，具有不同的含义。Prawitz的主要观点是，这些不同的含义是由一个双方都能接受的语义框架给出的。在本文中，我们提出了一种不同的方法适应，自然演绎框架，吉拉德的stoup机制。这将允许定义一个纯粹的和谐自然演绎系统的命题片段普拉维茨的普世逻辑。
2022-04-06 cs.LO
The Attack as Strong Negation, Part I
在经典逻辑中加入强否定$N$，将论证中“$x$攻击$y$“的攻击关系解释为$(x\to Ny)$。我们写了一个相应的对象级别（仅使用$N$）的经典理论，为每个论证网络，并表明，该理论的经典模型完全对应于完整的扩展的论证网络。我们通过例子展示了这种方法如何简化抽象论证网络的研究。我们比较与其他翻译的抽象论证网络到逻辑，如经典谓词逻辑或模态逻辑，或逻辑编程，我们也比较与抽象辩证框架。
2015-06-10 cs.LO
A Proof-theoretic Semantics for Intuitionistic Linear Logic
Department of Computer Science, University College London（伦敦大学学院计算机科学系）
本文扩展了Gheorghiu等人对直觉主义乘法线性逻辑的基扩展语义，为完整的直觉主义线性逻辑（包括模态连接词bang）提供了证明论语义，并讨论了处理bang连接词的挑战。
2026-06-12 cs.LO
Arbitrary Arrow Update Logic with Common Knowledge is neither RE nor co-RE
具有公共知识的任意箭头更新逻辑（Arbitrary Arrow Update Logic with Common Knowledge，AAULC）是一种动态认知逻辑，具有（i）表示特定类型的信息变化的箭头更新运算符和（ii）量化箭头更新的任意箭头更新运算符。通过将图灵机的执行过程编码到AAULC中，我们证明了AAULC中的有效公式和可满足公式都不是递归可重算的。特别是，它遵循AAULC没有递归公理化。
2017-07-27 cs.LO
Open Higher-Order Logic (Long Version)
我们介绍了一个变化Barthe等。的高阶逻辑，其中公式被解释为开放对象而不是封闭对象上的谓词。这样，具有内在函数性质的概念，如连续性，可微性或单调性，可以按照底层程序的结构以非常自然的方式表达和推理。我们给开放的高阶逻辑在不同的口味，特别是在其关系和本地版本，后者被定制的情况下，属性仅在底层功能的定义域的一部分。
2022-11-19 cs.LO
Proof systems for partial incorrectness logic (partial reverse Hoare logic)
本文为部分不正确性逻辑（部分反向霍尔逻辑）定义了普通和循环两种证明系统，证明其可靠且相对完备，并通过循环不变式及循环证明转化方法完成完备性证明。
2025-02-28 cs.LO cs.PL
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
Fuzzy inequational logic
Palacky University, Olomouc（奥洛穆茨帕拉茨基大学）
我们提出了一个逻辑推理的分次不等式，推广了普通的不等式逻辑中使用的泛代数。该逻辑处理项之间的不平等形式的原子谓词公式，并在分级设置中形式化它们的语义蕴涵和可证明性，从而可以从部分真的假设中得出部分真的结论。我们遵循Pavelka的方法，定义一般程度的语义蕴涵和证明使用完整的剩余格结构的真度。我们证明了这个逻辑是Pavelka式完备的。此外，我们给出了一个逻辑推理的分级“若-则”规则，这是得到的一般结果的特殊情况。
2015-03-23 cs.AI cs.LO
Logic interpretations of ANN partition cells
Brandenburgische Technische Universität Cottbus-Senftenberg（科特布斯-森夫滕勃兰登堡工业大学）
本文针对由ReLU层和线性层组成的前馈人工神经网络，提出一种新的逻辑解释方法，通过将输入空间分解为网络划分单元并推导表示分类交互模式的二元逻辑树，实现了利用逻辑工具集分析和操作ANN语义。
2024-08-26 cs.AI cs.LO
Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)
我们引入一种新形式的逻辑关系，在度量关系的精神，使我们能够分配给每一对程序的数量测量他们的距离，而不是一个布尔值代表他们是等价的。微分逻辑关系的新颖之处在于，不（一定）用数值来度量项之间的距离，而是用某种数学对象来度量，这种数学对象以某种方式反映了被比较项的交互复杂性，即类型。我们将这一概念推广到简单型的代数演算中，并给出了可靠性定理的一种形式。我们还看到普通的逻辑关系和度量关系可以被看作是微分逻辑关系的实例。最后，我们表明，微分逻辑关系可以组织在一个carbohydrate封闭范畴，相反度量关系，这是众所周知的没有这样的结构，但只有一个monoidal封闭范畴。
2019-04-27 cs.LO cs.PL
Pomset logic: the other approach to non commutativity in logic
30年前，我介绍了经典线性逻辑的一个非交换变体，称为“pomset逻辑”，它是从线性逻辑的一种特殊范畴解释（称为相干空间）中产生的。除了线性逻辑中常见的交换乘法连接词外，pomset逻辑还包括一个非交换连接词“$\triangleleft$“，称为“before”，结合和自对偶：$(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$。一个pomset逻辑证明的结论是一个偏序的多集公式。Pomset逻辑具有割消和指称语义的证明网演算，忠实地嵌入了证明网演算。对pomset逻辑的研究已经重新开放，最近的结果是关于漂亮的证明网，关于它的微积分，或者关于它的后续演算，如Guglielmi和Strassburger的深度推理。因此，现在是我们发表一个完整的介绍pomset逻辑，包括出版和未出版的材料，旧的和新的结果。Pomset逻辑（1993）是线性逻辑（1987）的非交换变体，就像Lambek演算（1958！）它也可以用作语法形式主义。这两种演算是完全不同的，但我们希望我们在这里给出的代数表示，用公式作为代数项，用证明（网）正确性的语义概念，更好地匹配兰贝克关于逻辑应该是什么的观点。
2023-02-03 cs.LO math.LO
A Standard Grammar for Temporal Logics on Finite Traces
支持时态逻辑公式的工具的异构性在互操作性方面提出了几个挑战。特别是，一个标准的语法的时间逻辑有限的痕迹，尽管类似于一个无限的痕迹，目前失踪。本文提出了一种用于在有限迹上解释的几种时态逻辑形式的标准语法，如线性时态逻辑（LTLf）、线性动态逻辑（LDLf）、纯过去线性时态逻辑（PLTLf）和纯过去线性动态逻辑（PLDLf）。
2021-06-07 cs.LO cs.SE
Approximating Defeasible Logics to Improve Scalability
Reasoning Research Institute（推理研究所）
可废止规则用于提供法律文件的可计算表示，最近，已被建议作为可解释AI的基础。这样的应用程序引起了人们对实现的可伸缩性的关注。可废止逻辑$DL(\partial_{||})$被引入作为$DL(\partial)$的更可扩展的替代方案，这是众所周知的。在本文中，我们考虑使用（实现）$DL(\partial_{||})$作为一个计算辅助计算结论在$DL(\partial)$和其他可废止的逻辑，而不是作为一个替代$DL(\partial)$。我们确定的条件下，$DL(\partial_{||})$可以取代$DL(\partial)$没有改变得出的结论，和条件下，$DL(\partial_{||})$可以用来得出一些有效的结论，剩下的由$DL(\partial)$。
2021-08-11 cs.AI cs.LO
A logical analysis of instrumentality judgments: means-end relations in the context of experience and expectations
本文提出了使用时态逻辑的工具性分析的启发工作的G. H。冯·赖特。文章的第一部分包含了哲学基础。我们讨论冯赖特的一般理论的代理和他的帐户的工具性。此外，我们提出了一些改进，这个框架，通过严格的定义所涉及的核心概念。在第二部分中，我们开发了一个逻辑系统，称为行动和期望的时态逻辑（TLAE）。该逻辑的灵感来自于一个基于不确定时间的命题动态逻辑片段。证明了该系统相对于其给定的语义是弱完备的。然后，我们采用TLAE形式化和分析的工具关系中定义的第一部分的文件。最后，我们指出了我们的工作的哲学含义和可能的扩展。
2023-02-23 cs.LO math.LO
On a coalgebraic view on Logic
在本文中，我们提出了从一个角度对逻辑过渡到其他方法，并特别适用于获得一个coalgebraic表示的逻辑。这个过程的核心要素是将结果关系视为范畴中的态射。
2012-02-04 cs.LO math.LO
Strongly Complete Logics for Coalgebras
函子的余代数以统一的方式模拟不同类型的转移系统。本文主要讨论了集基余代数有限逻辑的统一描述。特别地，给出了从任意集合函子构造逻辑的一般方法，并在附加的假设下证明了该方法是强完备的。我们分三部分进行。第一部分论证了筛余极限保持函子是指保持泛代数结构的函子。我们的主要定理在这里指出，函子保持筛选余极限当且仅当它有一个有限的表示的操作和方程。此外，函子的代数范畴的表示是从基础范畴和函子的表示中合成地获得的。第二部分研究了在ind-completions上函子的代数，并将Jo nsson和Tarski关于带算子的布尔代数的典型扩张的定理推广到了这个情形。第三部分在第一部分的基础上展示了如何将有限逻辑与任何有限集保持函子T相关联。在第二部分的基础上，我们证明了在T上的一个合理条件下，该逻辑是强完备的。
2012-09-11 cs.LO math.CT
EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 1: ESPACE-Algorithms
已知乘积逻辑K_4xS_5和S_4xS_5以及子集空间的逻辑SSL的可满足性问题都在N_2EXPTIME中。我们提出ESPACE算法，这些问题的复杂性，提高了这个上限。在另一篇论文中，我们证明了这些问题是EXPSPACE-困难的。这表明这三个问题都是EXPSPACE完备的。
2019-08-09 cs.CC cs.LO math.LO
Guarded Second-Order Logic, Spanning Trees, and Network Flows
根据Courcelle的一个定理，一元二阶逻辑和守护二阶逻辑（其中也可以量化的边缘集）有相同的表达能力，对所有可数$k$-稀疏超图类。在本文的第一部分中，我们将这个结果推广到任意基数的超图。在第二部分中，我们提出了一个概括处理的方法编码的顶点集的单顶点。
2010-02-16 cs.DM cs.LO
A tensorized logic programming language for large-scale data
Kyoto University（京都大学）；National Institute of Advanced Industrial Science and Technology (AIST)（产业技术综合研究所）
介绍了一种基于张量嵌入的逻辑程序设计语言T-PRISM。我们的嵌入方案是对最先进的概率逻辑程序设计语言之一PRISM中的分布语义的修改，通过用多维数组替换分布函数，即，张量T-PRISM由逻辑程序设计和数值计算两部分组成。前者在一阶逻辑级别提供灵活和可解释的建模，后者利用GPU的并行化和硬件加速提供可扩展的计算。结合这两部分提供了从符号推理到深度学习的非常广泛的高级声明性建模。为了体现这种程序设计语言，我们还介绍了一种新的语义，称为张量语义，它结合了传统的最小模型语义在逻辑编程与张量的嵌入。在T-PRISM中，我们首先使用逻辑推理从给定的程序中导出一组与张量相关的方程，即，在符号空间中执行Prolog，然后在连续空间中通过TensorFlow求解导出的方程。使用我们的初步实施T-PRISM，我们已经成功地处理了广泛的建模。我们已经成功地处理了真正的大规模数据的声明式建模。本文提出了一种基于FB 15 k和WN 18数据集的知识图谱DistMult模型。
2019-01-20 cs.LG cs.LO
A temporal semantics for Nilpotent Minimum logic
在[Ban97]中指出了粗糙集（特别是准粗糙代数）与三值Rukasiewicz逻辑之间的联系。本文给出了幂零最小逻辑NM（[Fod95，EG01]）的一个类时态语义，其中每个时刻的逻辑都是由N_3给出的：证明了一个完备性定理。这是在[AGM08]和[ABM09]中开始的工作的继续，在这些工作中，作者为哥德尔（[Göd32]，[Dum59]）和基本逻辑（[Háj98]）的多值逻辑构建了时间语义。
2013-10-22 cs.LO math.LO
Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic
本文建立了直觉主义非交换逻辑的自然演绎或λ演算公式的规范化--它同时涉及交换和非交换连接词。这种演算首先介绍了德格罗特，而不是经典版本的Abrusci和Ruet承认充分熵，允许为了放宽到任何suborder。我们的结果还包括，作为一个特殊的情况下，正常化的自然演绎Lambek演算的产品，这是不足为奇的，但尚未证明。对于全熵的直觉非交换逻辑，至今没有一个证明网语法;对于语言应用，与自然演绎或多或少等价的逻辑演算由于缺乏标准的Curry-Howard同构而不方便。
2014-02-03 cs.FL cs.LO
EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness
已知乘积逻辑K4 xS 5和S4 xS 5的可满足性问题是NEXPTIME-困难的，子集空间的逻辑SSL的可满足性问题是PSPACE-困难的。我们提高这些问题的复杂性的下限，表明这三个问题是EXPSPACE-硬下的对数空间减少。在另一篇论文中，我们表明，这些问题是在ESPACE。这表明这三个问题都是EXPSPACE完备的。
2019-08-09 cs.CC cs.LO math.LO
Modular Labelled Sequent Calculi for Abstract Separation Logics
抽象分离逻辑是霍尔逻辑的一系列扩展，用于推理操纵诸如存储器位置之类的资源的程序。这些逻辑是“抽象的”，因为它们独立于任何特定的具体资源模型。他们的断言语言，称为命题抽象分离逻辑（PASL），以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。特别地，这些逻辑包含连接词$*$和$-\!*$，分别表示资源的组成和扩展。这种额外的表达能力是有代价的，因为所产生的逻辑都是不可判定的。鉴于其广泛的适用性，甚至半决策程序，这些逻辑是可取的。虽然在文献中讨论了几个PASL和它们与BBI的关系，但这些逻辑的证明理论和自动推理是本文的会议版本解决的开放问题，该版本使用无割标记演算为各种PASL开发了模块化证明理论。本文非平凡地改进了以前的工作，给出了一个一般框架的演算上的任何新的公理在逻辑满足一定的形式对应的推理规则在我们的框架，和完整性证明一般考虑这样的公理。我们的基础演算处理Calcagno等人。的原始逻辑的分离代数，增加了健全的规则，部分确定性和cancellativity，同时保持削减消除。然后，我们证明了分离逻辑中的许多重要性质，如不可分单元、不相交性、可分裂性和交叉分裂性，都可以用我们的一般公理形式表示。因此，我们的框架免费提供了这些属性的推理规则和完整性。最后，我们展示了我们的演算如何减少到具有全局标签替换的演算，从而实现更高效的实现。
2018-03-26 cs.LO cs.PL
The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I
混合逻辑的可满足性问题是不可判定的。这引发了一个关于可判定和可处理片段的研究计划。在本文中，我们调查的影响，限制命题部分的语言的可判定性和可满足性问题的复杂性在任意的，传递的，总的框架，框架的基础上的等价关系。我们还考虑了不同的模态和混合算子。我们跟踪边界的可判定性，并给出了精确的复杂性，大多数片段，特别是包括否定的所有片段。对于单调片段，我们能够区分容易的情况下，从困难的情况下，这取决于允许的一组操作。
2009-06-08 cs.CC cs.LO
Partial Orders, Residuation, and First-Order Linear Logic
Université de Montpellier（蒙彼利埃大学）；LIRMM（计算机科学、机器人技术与微电子实验室）；CNRS（法国国家科学研究中心）
我们将研究一阶线性逻辑的证明理论和语言学方面。我们将证明，以这样一种方式添加偏序约束，即每个子定义子的先行公式上的唯一线性序，允许我们定义许多有用的逻辑运算符。此外，偏序约束提高了证明搜索的效率。
2020-08-14 cs.CL cs.LO math.LO
Access Hoare Logic
Swansea University（斯旺西大学）
本文提出访问霍尔逻辑，用于分析计算机程序的访问安全，证明其正确性和完备性，并与标准霍尔逻辑建立联系，展示其与其它方法的根本差异。
2026-03-30 cs.CR cs.LO cs.SC
Sequentiality vs. Concurrency in Games and Logic
顺序性/并发性的区别和语义的证明之间的连接进行了研究，特别是游戏和线性逻辑。
2011-11-30 cs.LO math.LO quant-ph
