Completeness of Epistemic Coalition Logic with Group Knowledge
联盟逻辑是多智能体系统中最流行的逻辑之一。虽然联盟逻辑的认知扩展受到了广泛的关注，但其完全公理化的存在性迄今为止一直是一个开放的问题。在本文中，我们解决了其中的几个问题。我们证明了完备性认知联盟逻辑与共同知识，与分布式知识，共同和分布式知识，分别。
2011-07-01 cs.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
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
2009-02-12 cs.LO
Coalgebraic completeness-via-canonicity for distributive substructural logics
我们证明了强完备性的一系列的子结构逻辑相对于一个自然的偏序集为基础的关系语义使用一个coalgebrical版本的完整性，通过规范。通过形式化的问题，在语言的coalgebraic逻辑，我们开发了一个模块化的理论，涵盖了各种不同的逻辑在一个单一的框架下，并借给自己进一步扩展。此外，我们认为，共代数框架提供了一个系统的和原则性的方法来研究资源模型之间的关系，语义方面，和句法方面的子结构逻辑。
2016-02-02 cs.LO
On Completeness Results of Hoare Logic Relative to the Standard Model
Cook研究了霍尔逻辑相对于Peano算术的标准模型$N$的一般完备性问题，它允许使用任意算术公式作为断言。在实践中，断言将是简单的算术公式，例如算术层次中的低级别。此外，我们发现，通过限制$N$的输入，最小断言理论的复杂性，霍尔逻辑的完整性，以保持可以降低。本文进一步研究了霍尔逻辑相对于$N$的完备性，将断言限制在算术公式的子类中（并将输入限制在$N$中）。我们的完整性结果完善库克的结果，降低了复杂性的断言理论。
2017-03-01 cs.LO
Completeness-via-canonicity for coalgebraic logics
本论文旨在提供一套技术来产生具有任意秩公理的共代数逻辑的完备性结果。我们已经选择了调查的可能性，以推广什么可以说是最成功的方法之一，证明完整性的结果在“经典”模态逻辑，即完整性通过规范。这种技术特别适合于一个coalgebraic的推广，因为它的清洁和抽象的代数形式主义。
2015-10-30 cs.LO math.LO
Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic
New York University（纽约大学）；CISPA Helmholtz Center for Information Security（CISPA赫尔姆霍兹信息安全中心）
研究并发数据结构线性一致性中逻辑原子性规范与线性一致性的关系，证明Iris分离逻辑框架下能为线性一致数据结构导出逻辑原子性规范，将多种证明技术嵌入Iris并应用于多个队列实现，还建立相关联系并机械化结果。
2026-07-14 cs.LO cs.PL
P-time Completeness of Light Linear Logic and its Nondeterministic Extension
在CSL'99中，Roversi指出Girard的开创性论文“Light Linear Logic”中的图灵机编码有一个缺陷。此外，他提出了一个工作版本的编码轻仿射逻辑，但不是在轻线性逻辑。在本文中，我们提出了一个工作版本的编码轻线性逻辑。编码的想法是基于Girard的线性逻辑教程论文的评论。编码也是一个例子，显示了附加连接词的有用性。此外，我们还考虑了轻线性逻辑的非确定性扩展。我们证明了扩展系统是NP-完全的，其意义与轻型线性逻辑的P-完全性相同。
2004-10-18 cs.LO
Algebraic Logic, I Quantifier Theories and Completeness Theorems
代数逻辑研究与命题和一阶逻辑相关的代数理论。本文概述了一阶逻辑的一种新的代数方法。我们引入量词理论的概念，这是一个函子从一类单子的集合的布尔代数的范畴，连同一个唯一确定的系统的量词。这种方法的一个显著特点是，凯莱完备性定理和哥德尔完备性定理可以在量词理论中以更简单的方式陈述和证明。这两个定理是由于哈尔莫斯的polyadic代数。我们还提出了一个简单的透明的治疗超产品的模型的量词理论。
2013-01-04 cs.LO
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
有限迹上的时态逻辑与潜在无限迹上的时态逻辑不同。Rozelu首先证明了有限迹上线性时态逻辑（LTLf）的完备性，并提出了一个新的共归纳公理。我们提供了一个不同的证明，用更少，更传统的公理。我们的证明是Kröger和Merz的Henkin-Hasenjaeger式证明的直接改编。我们修改的本质是我们“注入”有限性：也就是说，我们改变证明结构以确保模型是有限的。我们的目标是提出一个全面的，可访问的证据。
2021-07-13 cs.LO
Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators
University of Oxford（牛津大学）；Birkbeck, University of London（伦敦大学伯贝克学院）；Institute for Information Transmission Problems（信息传输问题研究所）；Moscow Institute of Physics and Technology（莫斯科物理技术学院）；King’s College London（伦敦国王学院）；Kyushu Sangyo University（九州产业大学）；University of Liverpool（利物浦大学）
本文研究严格正模态逻辑在meet-半格上的Kripke完备性，探讨两种语义是否定义相同后果关系。
2019-03-22 cs.LO
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
2000-06-05 cs.LO
Strong completeness of modal logics over 0-dimensional metric spaces
我们证明了一些模态逻辑的强完备性结果与普遍的模态，关于他们的拓扑语义在0维稠密的度量空间。我们还使用紧性的失败来证明，对于某些语言和空间，没有标准的模态演绎系统是强完备的。
2019-11-28 cs.LO math.LO
Completeness of two fragments of a logic for conditional strategic reasoning
本文证明了合作条件策略推理逻辑（CCSR）的责任片段和能力片段的完备性，方法涉及标准析取、有效性归约条件、抽象博弈形式及其实现，有望推广至CSR及其他策略逻辑。
2025-02-26 cs.LO
Completeness of Flat Coalgebraic Fixpoint Logics
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性中。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的定点逻辑倾向于用表达性来换取简单性和可读性，事实上，它经常存在于μ演算的单个变量片段中。这种平坦定点逻辑的家族包括，例如，LTL、CTL和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算（如交替时间时序逻辑ATL）的平坦片段，以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
2016-06-09 cs.LO
Games and Full Completeness for Multiplicative Linear Logic
我们提出了一个游戏语义的线性逻辑，其中公式表示游戏和证明表示获胜的策略。我们表明，我们的语义产生一个范畴模型的线性逻辑和证明完全完备的乘法线性逻辑与MIX规则：每一个获胜的策略是一个独特的无割证明网的表示。{ \em history-free}策略的概念扮演了一个关键的角色;在无历史策略和交互作用几何之间建立了强有力的联系。我们的语义学结合了极性的自然概念，导致了添加剂的精细处理。我们与Joyal，Blass等人的相关工作进行了比较。
2013-11-23 cs.LO
Soundness and Completeness of the NRB Verification Logic
这篇简短的论文给出了一个模型，并证明了确定性命令式程序的NRB验证逻辑的完整性，该逻辑在过去曾被用作大型，快速变化的开源C代码档案（如Linux内核源代码）的自动语义检查的基础。该模型是一个彩色的状态转换模型，从上面的一组可能的程序的过渡近似。相应地，逻辑捕获可能在程序中的给定点触发特定缺陷的所有跟踪，但也可能标记误报。
2013-08-18 cs.LO
Many-Valued Coalgebraic Modal Logic: One-step Completeness and Finite Model Property
本文利用谓词提升方法研究了多值形式的余代数模态逻辑。余代数，被理解为一般的转移系统，可以作为各种模态逻辑的语义结构。在余代数模态逻辑中，一个著名的结果是它的完备性可以在一步水平上确定。利用正则模型的构造方法，我们将结果推广到多值情形。我们证明了基于三种不同多值代数结构的余代数模态逻辑的结果，这三种多值代数结构包括：有限值Rukasiewicz代数，用正则常数和Baaz Delta展开的交换积分Full-Lambek代数（FL $_{ew}$ -代数），以及用赋值运算展开的FL $_{ew}$ -代数.此外，我们还利用过滤技巧证明了多值余代数模态逻辑的有限模型性质。
2022-06-15 cs.LO
Expressive Completeness of Metric Temporal Logic
度量时态逻辑（Metric Temporal Logic，MTL）是线性时态逻辑的一种推广，其中Until和Since模态用表示度量约束的间隔来注释。Hirshfeld和Rabinovich的一个开创性的结果表明，在实数上，具有二进制顺序关系<和一元函数+1的一阶逻辑严格地比具有整数常数的MTL更具表达性。事实上，他们证明，没有时间逻辑的模态是由公式定义的有界量词深度可以表达完整的FO（<，+1）。在本文中，我们展示了一个令人惊讶的结果：如果我们在一阶逻辑中允许一元函数+q，（q有理数），并相应地允许MTL中的有理数常数，那么这两个逻辑具有相同的表达能力。这给出了第一个推广的坎普定理的表达完整性的LTL FO（<）的定量设置。这个结果的证明涉及Gabbay的分离概念的推广。
2013-02-16 cs.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO math.LO
Simpler completeness proofs for modal logics with intersection
有一个显着的兴趣，扩大各种模态逻辑与交叉，最突出的例子是知识和doxastic逻辑与分布式知识。这种逻辑的完备性证明往往是复杂的，特别是在标准认知逻辑中的模型类，如S5，主要是由于标准模态逻辑中模态的交集的不可定义性。在[8]中概述了S5情况的标准证明方法，后来在[13]中更详细地解释，使用“解开折叠方法”的情况来实现树状模型以处理不可定义性问题。然而，由于细节水平和对S5的依赖，这种方法不容易适应其他逻辑。在本文中，我们提出了一个更简单的证明技术，通过建立一个树状规范模型直接，这避免了复杂的过程中解开和折叠。我们证明了技术，通过显示正常模态逻辑K，D，T，B，S4和S5扩展与交叉模态的完整性。此外，这些树型规范模型是兼容的Fischer-Ladner风格的闭包，我们结合的方法来显示所提到的逻辑的完整性进一步扩展与传递关闭的联合模态PDL或认知逻辑。其中一些完备性结果是新的。
2020-04-05 cs.LO math.LO
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
Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics
双直觉稳定时态逻辑（英语：Bi-Intuitionistic Stable Tense Logics）是一种具有克里普克语义的时态逻辑，其中框架中的世界配备有前序以及相对于该前序“稳定”的可达性关系。BIST逻辑是在超图的语义背景下产生的逻辑BiSKt的扩展，因为预序的特殊情况可以表示超图的关联结构。在本文中，我们提供了，第一次，一个希尔伯特式公理化的BISKt和证明强完备性的BiSKt。我们继续证明强完备性的一类BIST逻辑得到的BiSKt由一定形式的公式扩展。此外，我们还证明了一类BIST逻辑的有限模型性质和可判定性。
2017-03-07 cs.LO math.LO
Importing soundness and completeness in modal logics
Scuola Normale Superiore di Pisa（比萨高等师范学院）
提出从表达能力更强的模态语言向较弱语言传递可靠性与完全性的通用策略，统一了多种算子可定义性概念，并通过语义不敏感性和保真翻译实现。
2026-06-24 cs.LO math.LO
Relative Completeness of Incorrectness Separation Logic
针对操作堆的程序下近似问题，本研究聚焦于用于漏洞检测的不正确性分离逻辑（ISL），通过引入含变量别名的规范化方法计算最弱后置条件，结合允许无限析取的析取范式框架，证明了ISL的相对完备性。
2025-08-03 cs.LO
Verified completeness in Henkin-style for intuitionistic propositional logic
本文在Lean定理证明器中形式化并验证了Troelstra和van Dalen提出的直觉主义命题逻辑Henkin式完备性证明，是该方法下首个经机械验证的同类成果，源码已开源。
2023-10-03 cs.LO
Weak Completeness of Coalgebraic Dynamic Logics
我们提出了Fischer和Ladner的命题动态逻辑（PDL）和Parikh的游戏逻辑（GL）的共代数概括。在早期的工作中，我们证明了一个通用的强完备性结果的余代数动态逻辑没有迭代。这些程序的共代数语义由单子T给出，模态通过谓词提升来解释，其转置是从T到邻域单子的单子态射。在本文中，我们表明，如果单子T进行了一个完整的半格结构，那么我们可以定义一个迭代构造，和适当的概念菱形和框状的谓词提升，允许定义的公理化参数在T中，pixel和一组选定的逐点程序操作。作为我们的主要结果，我们表明，如果逐点操作是“负自由”和Kleisli组合左分布在诱导加入Kleisli箭头，那么这个公理化是弱完全的标准模型类。作为特例，我们恢复了PDL和双自由博弈逻辑的弱完备性。作为一个适度的新的结果，我们获得了完整的双自由GL扩展与交叉（恶魔的选择）的游戏。
2015-09-10 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
Intuitionistic Completeness of First-Order Logic
我们建立完整的直觉一阶逻辑，iFOL，表明一个公式是可证明的，当且仅当其嵌入到最小的逻辑，mFOL，是一致有效的下布劳威尔海廷柯尔莫哥洛夫（BHK）语义，预期的语义iFOL和mFOL。我们的证明是直观的，并提供了一个有效的程序Prf，统一的最小证据转换成一个正式的一阶证明。我们已经实现了Prf。一致有效性是使用交集运算符定义的，它是话语和原子谓词域上的通用量词。一致有效的iFOL公式也是直观有效的，但不是相反。我们最强的结果需要范定理，它也可以证明经典的显示，Prf终止使用柯尼希定理。我们的完备性定理背后的基本思想是，一个单一的证据项evd见证了最小逻辑公式F的一致有效性。即使找到一个一致的实现子也保证了直觉的有效性，因为Prf（F，evd）建立了F的一阶证明，建立了它的直觉有效性，并提供了一个纯粹的逻辑规范化实现子。我们为iFOL建立完整性如下。弗里德曼证明了iFOL可以通过他的A-变换嵌入到最小逻辑（mFOL）中，将公式F映射到FA。如果F是一致有效的，那么FA也是一致有效的，并且通过我们的完备性定理，我们可以在极小逻辑中找到FA的一个证明。然后我们从FFalse直观地证明F，即通过对A和mFOL的\bot取False。我们的结果解决了Beth在1947年提出的一个悬而未决的问题。
2011-10-17 cs.LO
Conceptual completeness for subgeometric logics
University of Gothenburg（哥德堡大学）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学、法国国家科学研究中心、信息与随机研究所）；University of Cambridge（剑桥大学）
研究几何逻辑片段的“概念完备性”，通过理论与拓扑斯之间的对偶刻画，证明相干逻辑等片段在完整几何逻辑中保守嵌入，并等价于基于集合模型的传统重构定理。
2026-07-03 cs.LO math.CT math.LO
A Henkin-style completeness proof for the modal logic S5
本文提出了一个最近的形式化的Henkin风格的完整性证明的命题模态逻辑S5使用精益定理证明。形式化的证明接近于Hughes和Cresswell的证明，但是这个系统基于不同的公理选择，更好地描述为一个Mendelson系统，增加了K，T，S4和B的公理方案，以及必要性规则作为推理规则。该语言有假和蕴涵作为唯一的原始逻辑连接词和必要性作为唯一的原始模态算子。完整的源代码可以在www.example.com上获得，并且已经使用Lean 3.4.2进行了类型检查。
2021-10-23 cs.LO
Completeness for Game Logic
游戏逻辑是由Rohit Parikh在20世纪80年代引入的，作为命题动态逻辑（propositional dynamic logic，PDL）的推广，用于推理玩家在确定的2人游戏中可以强制执行的结果。从语义上讲，从程序到游戏的概括是通过从Kripke模型到单调邻域模型来反映的。Parikh提出了一个自然的PDL风格的希尔伯特系统，它很容易被证明是合理的，但它的完备性迄今为止仍然是一个开放的问题。在本文中，我们介绍了一个切免费的游戏逻辑的mu演算，和两个切免费的mu演算，操作注释公式，一个游戏逻辑和一个单调的μ演算，多模态μ演算的变体，其中的语义是由单调邻域模型，而不是Kripke结构。我们表明这些系统是健全的和完整的，帕里克的公理化的完整性如下。我们的方法建立在Afshari & Leigh（LICS 2017）最近的想法和结果的基础上，我们通过系统之间的一系列证明转换来获得完整性。一个关键的要素是从博弈逻辑到单调μ演算的有效性保持翻译。
2019-04-30 cs.LO math.LO
Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
本文提出二元混合逻辑的完备表记演算，同时构建了依赖维度的混合依赖积逻辑演算，并证明其完备性，但所有系统均不具终止性。
2023-11-14 cs.LO math.LO
Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
Imperial College London（伦敦帝国理工学院）
研究了一类用于多智能体系统推理的一阶时间认知逻辑。我们编码系统的典型属性，包括完美的回忆，同步性，无学习，并具有独特的初始状态的变量的量化解释系统，解释系统的一阶扩展。我们确定了几个单音节片段的一阶时间认知逻辑，并显示其完整性相对于其相应的类的量化解释系统。
2014-01-23 cs.AI cs.LO cs.MA
On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
本文提出首个带while循环的相对完备的基于满足性的量子霍尔逻辑，通过构造最弱前置项演算证明完备性，并成功验证Deutsch算法和量子隐形传态的正确性。
2024-05-03 cs.LO
Logic + control: On program construction and verification
本文提出了一个例子，形式化推理的语义Prolog程序的实际意义（SAT求解器的豪和国王）。该程序被视为一个带有附加控制的定子句逻辑程序。逻辑程序是通过逐步精化的方法构造的，并与其正确性和完整性证明携手并进。证明是声明性的--它们不引用任何操作语义。逻辑程序构造的每一步都遵循一种系统的方法来构造可证明正确和完整的程序。我们还证明了在最终的Prolog程序中保持了逻辑程序的正确性和完整性。此外，我们证明终止，发生检查自由和非挣扎。我们的例子展示了如何将处理“逻辑”和处理“控制”分开。大多数证明都可以在“逻辑”级别上完成，从任何操作语义中抽象出来。这个例子使用了近似的规格说明;它们在简化逻辑程序的推理中是至关重要的。它还表明，语义保持程序转换的范例可能是不够的。我们建议考虑转换保持正确性和完整性方面的近似规范。
2017-05-12 cs.LO cs.PL
Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
模态公式表示Kripke框架上的一元二阶性质，但在许多重要情况下，它们具有一阶等价物。计算这样的等价物对于逻辑和计算原因都是重要的。另一方面，模态公式的规范性也很重要，因为它意味着用规范公式公理化的逻辑的框架完备性。计算一个模态公式的一阶等价等价物相当于消除二阶量词。二阶量词消去有两种算法：基于约束消解的SCAN算法和基于Ackermann建立的逻辑等价的DLS算法。在本文中，我们介绍了一种新的算法，SQEMA，计算一阶等价物（使用阿克曼引理的模态版本），而且，用于证明规范的模态公式。与SCAN和DLS不同，它直接作用于模态公式，从而避免了Skolemization和随后的unskolemization问题。我们提出的核心算法，并说明它与一些例子。然后，我们证明了它的正确性和规范的所有公式上的算法成功。我们表明，它不仅成功的所有Sahlqvist公式，但也对更大的类的归纳公式，在我们以前的论文中介绍。因此，我们开发了一种纯粹的算法方法来证明模态逻辑中的规范完备性，特别是，建立了模态逻辑中迄今为止最普遍的完备性结果之一。
2006-03-08 cs.LO
PSPACE-completeness of bimodal transitive weak-density logic
本文利用窗口方法并结合双模态K算法，证明在弱密度逻辑中添加传递性后，其可满足性与有效性均为PSPACE完全。
2025-07-20 cs.LO
Set-Theoretic Completeness for Epistemic and Conditional Logic
在哲学和数学文献中，逻辑的标准方法是定义一种语言，这种方法也被计算机科学所采用（语法），一个适当的模型类以及语言中公式的解释（语义学），公理和推理规则的集合，表征推理（证明理论），然后通过可靠性和完整性结果将证明理论与语义联系起来。在这里，我们考虑一种在经济学文献中更常见的方法，它纯粹在语义，集合论层面上工作。我们提供了一些认知和条件逻辑的集合论完备性结果，并对比了句法和集合论方法的表达能力
2000-05-30 cs.AI cs.LO
Completeness for Two Left-Sequential Logics
左序贯逻辑提供了一种方法来推理（封闭的）命题项与原子命题，可能有副作用，并从左到右顺序评估。这样的命题术语通常用在程序设计语言中来指导程序的流程。在这篇论文中，我们探讨了两个这样的左序贯逻辑。首先，我们讨论完全求值左序逻辑，它采用完全求值策略，即，为了评估一个项，评估它的每一个原子命题，从而导致其可能的副作用发生。然后，我们转向短路（左序）逻辑，如[BP 10b]所示，其中评估可能是“短路”的，从而防止某些（如果不是全部）被评估的项中的原子命题。我们提出了评估树作为一个自然的语义逻辑，并提供公理化的最小识别的变体。由此，我们定义了一个逻辑与连接词，规定了一个完整的评估策略，以及连接词，规定了短路评估策略。
2012-06-09 cs.LO
On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop
本文针对带While循环的基于满足的概率Hoare逻辑的相对完备性这一长期开放问题，构建新型PHL系统，通过两步证明其相对完备性，为随机化程序的概率性质验证提供了理论基础。
2024-06-23 cs.LO
NEXP-completeness and Universal Hardness Results for Justification Logic
我们提供了一个较低的复杂性约束的多智能体的理由逻辑的可满足性问题，建立从我们以前的工作一般NEXP上限是紧的。然后，我们使用一个简单的修改相应的减少证明，满足所有多代理的理由逻辑从那里是很难的西格玛2 p类的第二层次的多项式-给定某些合理的条件。我们的方法改进了这些所需的条件，为同一个下界的单代理的理由逻辑，证明了巴斯和库兹涅茨在2009年，从而回答了他们的一个开放的问题。
2015-03-01 cs.CC cs.LO
The Completeness of Reasoning Algorithms for Clause Sets in Description Logic ALC
在语义Web上，元数据和本体被用来使计算机能够读取数据。Web本体语言（OWL）已被提出作为一种标准的本体语言，并已研究了各种推理系统，这种语言。描述逻辑被认为是OWL的理论基础，它们提供了描述本体和知识库的形式语言的语法和语义。此外，描述逻辑的tableau算法已经发展成为可判定问题的标准推理算法。然而，Tableau算法生成低效的推理步骤，由于其不确定性分支的析取以及存在量化的模型规模的增加。在这项研究中，我们提出了合取范式（CNF）的概念，它利用一个平面的概念形式的描述逻辑ALC，以开发算法推理的条款集。我们提出了一个有效的推理算法的条款集，任何ALC的概念转化为一个等价的CNF概念。在理论上，我们证明了CNF概念可满足性推理算法的可靠性、完备性和可终止性。
2022-08-10 cs.LO
Flat modal fixpoint logics with the converse modality
我们证明了一个通用的完整性结果，一类模态不动点逻辑对应于平面片段的双向μ演算，延长早期的工作Santocanale和Venema。我们观察到，Santocanale和Venema的证明，至少不动点的Lindenbaum-Tarski代数的某些平坦的不动点逻辑是建设性的，使用有限伴随，不再工作时，逆模态介绍。相反，我们的完整性证明直接构建了一个模型的一致性公式，使用归纳规则的方式是类似于标准的完整性证明命题动态逻辑。这种方法结合了焦点的概念，这是以前使用的基于表格的模态不动点逻辑推理。
2017-10-12 cs.LO
Proof-Theoretic Functional Completeness for the Connexive Logic C
本文通过纯证明论方法，在双边主义框架下结合相干推理理解，证明了逻辑C联结词的功能完备性。
2025-07-09 cs.LO math.LO
Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder
在本文中，我们继续在\cite{Zh21c}的研究，发展的Sahlqvist型完备性理论的混合逻辑与满意运营商和向下绑定$\mathcal{L}(@, \downarrow)$。我们按照\cite{ConRob}中的思想定义了$\mathcal{L}(@, \downarrow)$的骨架Sahlqvist公式类，但是我们遵循了一种不同的证明策略，这是纯粹的证明理论，即对于每个骨架Sahlqvist公式$ϕ$及其混合纯对应$π$，$\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$证明了$π$，因此$\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$相对于$π$定义的框架类是完备的，使用\cite{Zh21c}中定义的算法$\mathsf{ALBA}^{\downarrow}$的受限版本。
2022-07-04 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
Subreflexive Logic: Completeness without Identity
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
研究次自反逻辑，通过多种方式构建语义，包括引入海廷和布尔半代数、定义半伴随和单位等，证明其具有可靠且完备语义，能将蕴含解释为稳健后承，还允许句法消去切割，在经典情形下特定指称集语义也完备。
2026-07-28 cs.LO math.LO
Logics for Epistemic Actions: Completeness, Decidability, Expressivity
我们考虑动态版本的认知逻辑，如Baltag和Moss的“认知程序的逻辑”（2004）中所阐述的。这篇论文提出了一种动态认知逻辑的逻辑语言（实际上是由动作签名参数化的语言家族）。已有研究表明，该语言的有效性是Pi-1-1-完备的，因此不存在递归公理化的完备逻辑系统，而本文则证明了无动作迭代的片段的弱完备性结果，以及无动作迭代的片段和常识的强完备性结果。我们的工作涉及到术语重写理论的迂回。该论点使用模态过滤，因此我们得到有限的模型属性，因此可判定性。我们也给我们最大的语言翻译成PDL，从而获得第二个证明的可判定性。本文最后给出了一些关于表达能力的结果。这些主要涉及比较动作迭代自由语言与模态逻辑增强传递闭包运算符。我们回答了一个自然的问题，我们通过不同的动作签名获得的语言：我们证明了一个逻辑语言与运营商的私人公告更有表现力比一个公共公告。
2022-03-13 cs.LO math.LO
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
本文研究了$\exists^*\forall^*$语言中带有量词前缀的前向公式的分离合取和蕴涵无限制嵌套的分离逻辑在可能位置论域为可数无限或有限的情况下的可满足性问题.与带有未解释谓词和等式的一阶逻辑类似，我们称这个片段为伯奈斯-舍恩芬克尔-拉姆齐分离逻辑[BSR（SLk）]。我们表明，不同于在一阶逻辑中，（在）有限可满足性问题是不可判定的BSR（SLk），我们定义了两个非平凡的子集，这是可判定的有限和无限的可满足性，分别通过控制的范围内的普遍量化变量的出现分离的影响，以及后者的出现的极性。可判定性结果是通过分离连接词的受控消除获得的，描述为（i）将前束形式分离逻辑公式有效地翻译成少量\emph{test formulae}的组合，仅使用一阶连接词，随后（ii）将后者翻译成可均衡满足的一阶公式。
2018-02-16 cs.LO
Completeness for a First-order Abstract Separation Logic
分离逻辑（SL）断言语言的定理证明的现有工作要么集中在抽象语义上，这在大多数程序验证应用中是不容易获得的，要么集中在具体模型上，这是不可能的。具体SL中的一个重要元素是指向谓词，它表示单例堆。带有指向谓词的SL已被证明是不可递归的。在本文中，我们开发了一个一阶SL，称为FOASL，与抽象版本的指向谓词。我们证明了FOASL是健全的和完整的抽象语义，其中标准SL语义是一个实例。我们还表明，一些推理原则，涉及点到谓词可以近似为FOASL理论，从而使我们的逻辑用于推理具体的程序验证问题。我们给出了一些例子理论，是健全的分离逻辑从文献中的不同变体，包括那些与雷诺兹的语义不兼容。在实验中，我们展示了我们的FOASL为基础的定理证明，这是能够处理大量的分离逻辑与堆语义，以及非标准的语义片段。
2016-08-24 cs.LO
On the Completeness of Selective Unification in Concolic Testing of Logic Programs
Concolic测试是一种流行的动态验证技术，可用于模型检验和自动测试用例生成。我们最近在逻辑编程的上下文中引入了concolic测试。与以前的方法相比，这种设置的关键要素是一种技术，通过考虑原子可以与某些程序子句的头部统一的所有可能方式来生成适当的运行时目标。这就是所谓的“选择性”统一。在本文中，我们表明，现有的算法是不完整的，并探讨不同的替代品，以便有一个健全的和完整的算法选择性统一。
2016-08-10 cs.LO
Cut-free Completeness for Modular Hypersequent Calculi for Modal Logics K, T, and D
我们调查了最近的建议，模态hyperlipidic结石。关系超序列的解释包括沿超序列的可及性关系。这些系统给出了与Lellman的线性嵌套序列相同的超序列解释，但由Restall独立开发用于S5，并由Parisi扩展到其他正常模态逻辑。由此产生的系统遵循Dosen原则：模态规则在不同的模态逻辑中是相同的。不同的模态系统只在外部结构规则的存在或不存在方面有所不同。除了S5之外，这些系统都是模块化的，因为不同的结构规则捕获了可访问性关系的不同属性。我们提供了第一个直接的语义无割完备性证明K，T，和D，并展示了这种方法是如何失败的情况下B和S4。
2021-11-05 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
