A non-uniform view of Craig interpolation in modal logics with linear frames
King's College London（伦敦国王学院）；University of Liverpool（利物浦大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
针对线性传递框架上的模态逻辑缺乏 Craig 插值性质的问题，提出非均匀方法研究插值存在性判定问题，证明对包含 K4.3 的有限公理化逻辑该问题可判定且为 coNP-完全。
2026-06-18 cs.LO math.LO
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
Université Paris Cité（巴黎西岱大学）；CNRS（法国国家科学研究中心）；IRIF（信息与随机研究所）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
将 Pitts 的均匀插值证明论技术扩展到直觉主义多后承设定，为直觉主义模态逻辑 KM 设计终止的多后承相继演算并构造均匀插值，同时证明 KM-代数类的连贯性。
2026-05-27 cs.LO math.LO
Mechanised uniform interpolation for modal logics K, GL, and iSL
本文在 Coq 中机械化计算并证明了模态逻辑 K、GL 和 iSL 的命题量词可定义性（一致插值），完善了 GL 的现有证明，实现了 iSL 的首次证明论构造，并提供了经过验证的计算程序。
2024-04-29 cs.LO math.LO
Uniform Agent-interpolation of Distributed Knowledge
School of Philosophy, Liaoning University（辽宁大学哲学学院）
本文提出了一种纯语法算法，用于确定具有分布式知识的模态逻辑K、KD和KT的统一插值公式。
2026-03-01 cs.LO
On Symbol Elimination and Uniform Interpolation in Theory Extensions
本文定义了广义一致插值概念，推广了覆盖与一致插值，并指出在特定理论扩展中，其计算可归约为符号消去及后续的无量词插值计算。
2025-06-02 cs.LO
Uniform Interpolation in Coalgebraic Modal Logic
一个逻辑有统一的插值，如果它的公式可以向下投影到给定的子签名，保留所有的逻辑后果，不提及删除的符号;较弱的属性（克雷格）插值允许投影公式-插值-是不同的每个逻辑后果的原始公式。这些性质是重要的，例如，逻辑理论的模块化。我们研究插值的上下文中的共代数模态逻辑，即模态逻辑公理化秩1，限制为清晰的情况下，许多模态。这种逻辑的例子包括模态逻辑K和KD，邻域逻辑及其单调变体，有限幺半群加权逻辑和联合逻辑。我们引入了一步（均匀）插值的概念，它只指一个限制逻辑没有嵌套的模态，并证明了一个共代数模态逻辑有均匀插值，如果它有一步插值。此外，我们确定保存有限的满射弱回调作为一个充分的，在单调的情况下，必要的一步插值的条件。因此，我们证明或reprove均匀插值的大多数例子上面列出的。
2022-05-01 cs.LO
Uniform Lyndon interpolation for intuitionistic monotone modal logic
本文证明了直觉单调模态逻辑$\mathsf{iM}$具有一致Lyndon插值性质性质（ULIP）.逻辑$\mathsf{iM}$是一种基于直觉的非正规模态逻辑，而ULIP属性是插值的加强，其中插值只依赖于蕴涵的前提或结论，并尊重命题变元的极性。我们的方法来证明ULIP产生明确的一致插值，并利用了一个终止的微积分$\mathsf{iM}$，我们已经为此目的开发。据我们所知，$\mathsf{iM}$具有ULIP和一个终止的逻辑演算的结果是第一个直觉非正规模态逻辑的结果。然而，而不是证明这些特定的结果，我们的目的是显示的建设性证明理论方法，我们用来证明ULIP的灵活性。它在过去几年中得到了发展，并已被应用于子结构，中间，经典（非）正规模态和直觉正规模态逻辑。根据这些结果，直觉非正规模态逻辑似乎是一个自然的下一类尝试应用该方法，我们在这方面迈出了第一步。
2022-08-09 cs.LO math.LO
Uniform Interpolation for Coalgebraic Fixpoint Logic
利用自动机与逻辑之间的联系，证明了一类广泛的余代数不动点逻辑具有一致插值性。为此，首先，我们推广的核心结果之一，在共代数自动机理论，即闭包下的投影，这是众所周知的，持有弱拉回保持函子，一类更一般的函子，即;具有准函子lax扩张的函子。然后证明了投影闭包蕴含互模拟量词的可定义性，最后证明了一致插值定理。
2015-03-08 cs.LO
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
Uniform Interpolation of Basic Tense Logic
Faculty of Humanities and Human Sciences, Hokkaido University（北海道大学人文学部人类科学学院）
本文通过扩展Visser的语义论证，证明了基本时态逻辑（双向模态逻辑）具有一致插值性质。
2026-07-01 cs.LO
Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics
Universität Bremen（不来梅大学）；University of Liverpool（利物浦大学）
研究了描述逻辑ALC中的一致内插和遗忘问题。我们的主要结果是模型理论的一致插值和他们的存在性的bisimula- tions，严格的复杂性界决定一致插值的存在性，一种方法来计算插值时，他们存在，和严格的限制他们的大小。我们使用模型理论和自动机理论的方法，作为一个副产品，还提供了保守扩展的特征和决策程序的混合。
2011-04-14 cs.AI cs.LO
Coexact completion of profinite Heyting algebras and uniform interpolation
University of Cambridge（剑桥大学）
本文将有限生成自由Heyting代数的层表示分解为有限完备化，确定有限Heyting代数的对偶范畴为K-拓扑斯的满子范畴，推广一致内插性质并建立K-拓扑斯的拓扑斯理论性质。
2026-09-07 cs.LO math.CT math.LO
Uniform Interpolation in Distributed Knowledge Modal Logics
Jinan University（暨南大学）
本文研究了分布式知识模态逻辑中的统一插值性质，通过扩展经典公式和字面消除框架，引入集体p-仿射概念，证明了六种分布式知识模态逻辑的统一插值性质。
2026-03-30 cs.LO
A proof-theoretic approach to uniform interpolation property of multi-agent modal logic
针对多智能体模态逻辑缺乏证明论进路UIP证明的问题，本文扩展已有证明系统，提出纯句法算法，证明了$\boldsymbol{\text{K}_n}$等三类多智能体模态逻辑的一致插值性质，还给出了无需二阶量词的直接证明。
2025-10-29 cs.LO
Second-Order Quantifier Elimination and Uniform Interpolation for Bath Path Logic and the Ordered Fragment
The University of Manchester（曼彻斯特大学）；Central European University（中欧大学）
考虑并扩展基本路径逻辑和一阶逻辑有序片段结果。通过引入常量斯柯伦化，将有序片段句子转化为基本路径逻辑，证明相关性质，还刻画了SCAN算法搜索空间并证明其终止性。
2026-07-07 cs.LO
Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
本文提出半解析矢列演算的通用框架，证明足够强的多模态子结构逻辑若具有此类演算则必满足 Craig 插值性质，并据此统一证明多类逻辑的 CIP，同时形式化证实几乎所有常见逻辑都缺乏“好的”矢列演算。
2024-09-03 cs.LO math.LO
Interpolation in Knowledge Representation
TU Dortmund University（图卢兹德多特蒙德大学）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；Universidade Nova de Lisboa（里斯本新大学）
本文研究了描述逻辑和逻辑编程中插值计算的理论与实践方法，探讨了其在知识表示中的应用及挑战。
2025-12-09 cs.AI cs.LO
Locality and applications to subsumption testing and interpolation in $\mathcal{EL}$ and some of its extensions
本文证明了轻量级描述逻辑（如$\mathcal{EL}$和$\mathcal{EL}^+$）中的包含问题可以表示为具有单调算子的半格类中的一致字问题。我们使用的可能性，有效的本地推理，在这样的类代数，以获得统一的PTIME决策程序的CBox包容在$\mathcal{EL}$，$\mathcal{EL}^+$及其扩展。这些地方的考虑，使我们能够提出一个新的家庭（可能是许多排序）的逻辑扩展$\mathcal{EL}$和$\mathcal{EL}^+$与$n$ -ary角色和/或数域。作为一个副产品，这使我们能够表明，${\cal EL}$和${\cal EL}^+$的代数模型具有地面插值，因此，${\cal EL}$，${\cal EL}^+$，以及本文研究的扩展具有插值。我们还展示了如何这些想法可以用于描述逻辑$\mathcal{EL}^{++}$。
2013-11-12 cs.LO
Interpolation in Classical Propositional Logic
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Potsdam（波茨坦大学）；University of Liverpool（利物浦大学）
研究经典命题逻辑中的插值法等相关概念，提出通过量词消去等四种方法计算插值，最后探讨了插值规模与电路复杂性的关系。
2026-07-08 cs.LO
Interpolation in Equilibrium Logic and Answer Set Programming: the Propositional Case
King’s College London（伦敦国王学院）；Universidad Politécnica de Madrid（马德里理工大学）；Universidad de Málaga（马拉加大学）
插值是经典逻辑和许多非经典逻辑的重要性质，在计算机科学和人工智能中有着重要的应用。在这里，我们研究的插值性质的命题版本的非单调系统的平衡逻辑，建立较弱或较强的形式的插值依赖于推理关系的精确解释。这些结果也产生了一种形式的插值地面逻辑程序下的回答集语义。对于析取逻辑程序，我们还研究了与变量遗忘概念密切相关的一致插值的性质。
2010-12-17 cs.AI cs.LO
Interpolation in Proof Theory
University of Amsterdam（阿姆斯特丹大学）；University of Bath（巴斯大学）；Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）
本研究通过证明论方法探讨了多种逻辑中的插值性质，介绍了Maehara和Pitts的方法，并展示了如何利用现代证明形式化方法构建插值证明。
2026-02-18 cs.LO
