arXiv 2104.150532021-04-30cs.LO

具有有限模型性质的S4的一些构造性变体

Some constructive variants of S4 with the finite model property

Philippe Balbiani, Martín Diéguez, David Fernández-Duque

摘要：

逻辑CS4和IS 4是模态逻辑S4的直觉变体。有限模型属性是否适用于这些逻辑中的每一个一直是一个长期存在的开放问题。在本文中，我们介绍了两个逻辑密切相关的IS 4：GS 4，通过增加哥德尔-达米特公理到IS 4，和S4 I，通过颠倒的角色模态和直觉关系。然后证明了CS4、GS4和S4 I都具有有限模型性质。

英文摘要：

The logics CS4 and IS4 are intuitionistic variants of the modal logic S4. Whether the finite model property holds for each of these logics has been a long-standing open problem. In this paper we introduce two logics closely related to IS4: GS4, obtained by adding the Godel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that CS4, GS4, and S4I all enjoy the finite model property.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

构造模态逻辑的嵌套序列

On Nested Sequents for Constructive Modal Logics

我们提出了各种模态逻辑的演绎系统，这些模态逻辑可以通过添加公理d，t，b，4和5的组合从正常模态逻辑CK的构造性变体中获得。这包括标准模态逻辑K4、S4和S5的构造变体。我们使用我们的演示形式主义的嵌套序列，并给出一个句法证明削减消除。

2015-09-02cs.LO

坍缩构造性与直觉主义模态逻辑

Collapsing Constructive and Intuitionistic Modal Logics

本文证明模态逻辑KB的构造性与直觉主义变体等价，与Das和Marin关于K的变体不等价的结果形成对比。

2024-10-01cs.LOmath.LO

构造性可证性逻辑

Constructive Provability Logic

我们提出了建设性的可证明性逻辑，一个直观的模态逻辑，通过允许逻辑反射可证明性来验证哥德尔和Löb的可证明性逻辑的Löb规则。这种逻辑的两个不同的变体，CPL和CPL*，在自然演绎和微积分的形式，然后被证明是等价的。此外，我们讨论了使用建设性的可证明性逻辑来证明分层否定逻辑编程中的直觉和结构证明理论。

2012-05-29cs.LOcs.PL

用IZF从构造性HOL证明中抽取程序<br>语义

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics

丘奇的高阶逻辑是有影响的证明助手-- HOL和PVS的基础。Church的逻辑有一个简单的集合论语义，使其可信和可扩展。我们因素HOL到一个建设性的核心加上公理的排中律和选择。我们同样的因素标准集理论，ZFC，到一个建设性的核心，IZF，公理排除中间和选择。然后，我们提供了标准的集合论语义，这样的方式，建设性的核心HOL映射到IZF。我们使用的析取，数值存在性和长期存在的IZF属性提供了一个程序提取能力，从证明建设性的核心。我们可以用两种不同的方式实现析取和数值存在性：一种是使用Rathjen对IZF的可实现性，另一种是使用Moczydlowski对IZF的一个新的直接弱归一化结果。后者也可以用于术语存在属性。

2008-09-09cs.LO

具有有限双关系框架性质的构造性S4模态逻辑

Constructive S4 modal logics with the finite birelational frame property

IRIT, Toulouse University（图卢兹大学 IRIT）；LERIA, University of Angers（昂热大学 LERIA）；Department of Philosophy, University of Barcelona（巴塞罗那大学哲学系）；Department of Mathematics, Ghent University（根特大学数学系）

本文证明了直觉主义模态逻辑CS4具有有限框架性质，并研究了与IS4相关的GS4、GS4^c和S4I逻辑，为它们建立了有限双关系框架性质，从而证明了可判定性，并给出了NEXPTIME上界。

2026-06-23cs.LO

构造μ-演算：游戏语义与非良基证明系统

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems

Institute of Sciece Tokyo, Japan（东京科学研究所）

本文研究基于构造模态逻辑CK的μ-演算变种，定义了游戏语义并证明其等价于双关系李普克内语义，进而利用游戏语义证明了完全标记的非良基证明系统的正确性与完备性，并探讨如何将其扩展到其他非经典模态逻辑的μ-演算。

2026-04-25cs.LOmath.LO

更多相关论文收起更多论文

带有构造性钻石算子的均匀插值

Uniform interpolation with constructive diamond

University of Amsterdam（阿姆斯特丹大学）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）

本文通过构造性方法证明构造性K（CK）和Wijesekera的K（WK）具有均匀插值性质，填补了直觉主义模态逻辑中独立box和diamond算子均匀插值研究的空白。

2026-05-27cs.LOmath.LO

LogicProof：一种基于网络的交互式教育定理证明器，用于经典和构造性逻辑中的自然演绎和相继式演算

LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics

Technical University of Košice（科希策理工大学）

介绍LogicProof这一用于教育的交互式网络定理证明器，支持经典和构造性逻辑的自然演绎与相继式演算，经学生测试能提升对形式证明构建的理解，补充现有教学方法。

2026-07-07cs.LO

计算树逻辑与故障跟踪测试的构造等价性

A Constructive Equivalence between Computation Tree Logic and Failure Trace Testing

形式化验证的两个主要系统是模型检验和基于代数模型的测试。模型检验基于某种形式的时态逻辑，例如线性时态逻辑（LTL）或计算树逻辑（CTL）。CTL是一种强大而现实的逻辑，它能够表达进程的最有趣的属性，如活性和安全性。基于模型的测试基于进程的某些操作语义（例如跟踪、故障或两者）及其关联的前序。除了互模拟之外，最细粒度的前序（主要是理论上的重要性）是基于故障跟踪的。我们表明，这两个最强大的变种是等价的，也就是说，我们表明，对于任何故障跟踪测试存在一个CTL公式相当于它，反之亦然。我们所有的证明都是构造性的和算法性的。我们的结果允许一个大系统的部分被指定为逻辑，而其他部分被指定为代数，从而结合了最好的两个（逻辑和代数）的世界。

2019-01-30cs.LO

构造类型论（扩充版）中一阶逻辑的完备性定理

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)

我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。

2021-12-14cs.LOmath.LO

直觉主义单调模态逻辑：证明论与语义

Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Bern（伯尔尼大学）

研究直觉主义单调模态逻辑IM，通过构造性邻域模型刻画其自然扩展族，提出基于经典单调模态逻辑M的结构演算，证明IM的可判定性，揭示M与K的构造性和直觉主义变体之间的类比。

2026-07-01cs.LOmath.LO

关于构造性和Rosser性质：更仔细地看一些Gödelean证明

On Constructivity and the Rosser Property: a closer look at some Gödelean proofs

从构造性和Rosser性质的角度研究了Kleene、Chaitin和Boolos对哥德尔第一不完全性定理的证明。不完备性定理的证明具有Rosser性质，当真实但不可证明的句子的独立性可以通过仅假设理论的（简单）一致性来证明时。众所周知，哥德尔自己的证明，他的不完备性定理不具有罗瑟性质，我们表明，也没有克莱因或布尔斯的证明。然而，我们表明，一个变种Chaitin的证明可以有Rosser属性。哥德尔、罗瑟和克莱因的证明是构造性的，因为他们通过算法的方式从理论中明确地构造了独立的句子。我们表明，Chaitin和Boolos的证明不是建设性的，他们证明的仅仅是存在的独立的句子。

2018-02-14cs.LOmath.LO

通过希尔伯特第十问题的不可判定性构造性证明里希的定理和停机问题

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

本文基于希尔伯特第十问题的不可判定性，通过双见证构造方法，构造性地证明了里希定理和停机问题的不可判定性，无需使用对角线法或自指。

2026-10-30cs.CRcs.LO

统一代数：完全简单类型λProlog的模型与构造性完备性

Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog

本文为λProlog语言基础逻辑HOHH建立模型论，证明消解的可靠性与完备性，并利用最小不动点及Lindenbaum代数变体给出构造性证明，同时提出新的切割消去方法。

2024-05-23cs.LOcs.PLmath.LO

具有不相容证明与反驳的双边主义基扩张语义

Bilateralist base-extension semantics with incompatible proofs and refutations

Department of Computer Science, University College London（伦敦大学学院计算机科学系）；Faculty of Sciences, University of Lisbon（里斯本大学理学院）

本文提出带不相容证明与反驳的双边自然演绎系统及基扩张语义，证明其可靠完备，并将其与 Nelson 构造性假相联系。

2025-10-19cs.LO

构造性主模态模态逻辑的复杂性

The Complexity of the Constructive Master Modality

本文提出了两种构造性主模态逻辑，并证明其复杂性为 EXPTIME，同时解决了相关逻辑的有效性问题

2026-07-22cs.LOmath.LO

基本直觉主义条件逻辑的证明论视角（扩展版）

A Proof-Theoretic View of Basic Intuitionistic Conditional Logic (Extended Version)

本文从证明论角度研究基本直觉主义条件逻辑，为IntCK引入嵌套演算、为CCKbox引入矢列演算，并在此基础上定义带might算子的保守扩张CCK，给出其模型类、公理化及若干扩张结果。

2025-07-03cs.LO

模态和构造逻辑的标记系统的精化及其应用

Refining Labelled Systems for Modal and Constructive Logics with Applications

Australian National University（澳大利亚国立大学）；Laboratoire d’informatique de l’École polytechnique（巴黎综合理工学院计算机实验室）

本文介绍了“结构精化方法”，它作为一种手段转换的模态和/或建设性逻辑的关系语义到一个“经济”的证明系统，通过连接两个证明理论的范式：标记和嵌套演算。标记序列的形式主义已经成功地在拥有理想的证明理论的性质，可以自动生成大型类的逻辑切割免费演算。尽管有这些品质，标记系统使用了复杂的语法，明确地结合了相关逻辑的语义，这样的系统通常违反了子公式属性的高度。相比之下，嵌套微积分使用更简单的语法，并坚持严格阅读子公式属性，使这样的系统在自动推理算法的设计中非常有用。然而，嵌套演算范式的缺点是，关于这种演算的自动构造（如在标记设置中）的一般理论基本上是不存在的，这意味着嵌套系统的构造和它们的属性的确认通常是在个案的基础上完成的。细化方法连接这两种范式在一个富有成效的方式，通过转换成嵌套的（或，精制标记）系统与前保持整个转换过程中的属性标记系统。为了证明精化的方法和它的一些应用，我们考虑文法逻辑，一阶直觉逻辑和道义STIT逻辑。介绍了细化标记演算将被用来提供第一个证明搜索算法的道义STIT逻辑。此外，我们使用我们的精炼标记演算的语法逻辑，以表明在类中的每一个逻辑具有有效的林登插值属性。

2021-07-30cs.AIcs.DMcs.FL

尼尔森自由逻辑中确定描述词的二元量词

A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic

本文在Nelson次协调逻辑N4及其负自由变体中考察并改进了Kürbis的二元量词I，给出嵌入函数、自然演绎系统和Kripke语义，以构造性假和次协调逻辑解决Russell确定描述词解释中的悖论问题。

2024-12-31cs.LO

通过矢列演算实现描述逻辑的构造性插值与基于概念的Beth可定义性

Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents

Institute of Artificial Intelligence, Technische Universität Dresden（德累斯顿工业大学人工智能研究所）

本文提出基于矢列系统的构造性方法，首次证明高表达力描述逻辑RIQ具有基于概念的Beth可定义性，并可从证明中计算插值式以提取隐式概念的显式定义。

2024-10-18cs.AIcs.DBcs.LO

使用GLINTS检查Maude变体

Inspecting Maude Variants with GLINTS

本文介绍了GLINTS，一个图形化的工具，探索不同的缩小计算在Maude。Maude的最新版本2.7.1提供了相当复杂的统一特性，包括收敛理论模公理（如结合性、交换性和恒等式（ACU））的有序方程统一。这种新颖的等式统一依赖于项$t$的“变体”集合的内置生成，即，计算代换$σ$的$t σ$的标准形式。变体生成依赖于一种称为“折叠变体窄化”的新颖窄化策略，该策略在形式推理、定理证明、测试、协议分析和模型检验中开辟了新的应用，特别是当理论满足“有限变体属性”时，即，理论中的每一项都有有限数量的最一般的变体。然而，变体收缩计算可能非常复杂，Maude只是以文本格式表示，通常太重而无法调试甚至无法理解。GLINTS系统为以下操作提供支持：（i）确定给定理论是否满足有限变体属性，（ii）彻底探索变体缩小计算，（iii）自动检查节点“嵌入”和“封闭性”模公理，以及（iv）查询和检查变体树的选定部分。本文件正在考虑被TPLP接受。

2017-07-18cs.LOcs.PL