Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability
随机布尔可满足性（SSAT）问题是由Papadimitriou在1985年通过随机量化给命题可满足性增加一个不确定性的概率模型时提出的。SSAT有许多应用，其中概率有界模型检验（PBMC）的符号表示的马尔可夫决策过程。本文确定了克雷格插值的SSAT框架的概念，并开发了一个算法，计算这样的插值的基础上的分辨率演算SSAT。作为一个潜在的应用领域，这个新的概念克雷格插值，我们解决概率系统的符号分析。我们首先调查使用插值的概率状态可达性分析，把证伪过程采用PBMC概率安全属性的验证技术。此外，我们提出了一种基于插值的方法来概率区域稳定性，能够验证在某些区域内稳定的概率足够大。
2012-06-25 cs.LO
Computation of Interpolants for Description Logic Concepts in Hard Cases
本文针对不具备Craig插值性质的描述逻辑及跨逻辑插值难题，首次给出在ALCH和ALCQ本体下计算ALC插值的初等算法，并指出一致插值可能具有非初等大小。
2025-07-21 cs.LO
Craig Interpolation with Clausal First-Order Tableaux
我们开发的基础计算Craig-Lyndon插值的两个给定的公式与一阶定理证明，构造子句表。可以这样理解的证明器包括基于两类演算的高效的面向机器的系统：面向目标的，如模型消除和连接方法，以及自底向上的，如超表演算。我们提出了第一插值方法为代表的一阶证明封闭tableaux的收益在两个阶段，类似于已知的插值方法的分辨率证明。第一阶段是对表结构的归纳，这足以计算命题插值。我们表明，这可以线性模拟不同的突出命题插值方法，通过归纳决议演绎树。在第二阶段，插值提升，量化的变量，取代某些条款（常数和复合条款）的变量。我们证明插值提升的正确性（对于没有内置的平等的情况下）抽象的基础上Herbrand定理和不同的表征的公式被解除比在文献中。此外，我们讨论了各种微妙的方面，相关的调查和实际实现的一阶插值子句表的基础上。
2021-03-21 cs.LO
Computation and Size of Interpolants for Hybrid Modal Logics
TU Dortmund University（多特蒙德工业大学）；University of Warsaw（华沙大学）；University of Liverpool（利物浦大学）
本文研究了混合模态逻辑中插值项的存在性与计算复杂度，提出了一种新的超马赛克消除技术，证明在许多标准混合模态逻辑中，若存在Craig插值项，则可在四次指数时间内计算，同时指出统一插值项的存在性是不可判定的。
2026-05-19 cs.LO
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
在SAT和SMT中计算Craig插值的问题最近受到了很大的关注，主要是因为它在形式化验证中的应用。插值生成的有效算法已经提出了一些理论的利益-包括平等和未解释的功能，线性算术的有理数，以及它们的组合-他们成功地使用在模型检验工具。然而，对于整数上的线性算术理论（LA（Z）），找到插值的问题更具挑战性，并且为完整理论LA（Z）开发有效的插值生成器的任务仍然是正在进行的研究的目标。在本文中，我们试图缩小这一差距。我们建立在以前的工作，并提出了一种新的插值算法的SMT（LA（Z）），它利用了当前最先进的SMT（LA（Z））求解器的全部功能。我们证明了我们的方法的潜力与我们的实施所提出的算法在MathSAT SMT求解器的广泛的实验评估。
2012-08-09 cs.LO
Craig Interpolation for Quantifier-Free Presburger Arithmetic
克雷格插值已成为一个通用的算法工具，以提高软件验证。例如，插值可以加速无限状态系统的不动点计算的收敛。它们还有助于改进迭代计算的惰性抽象的细化。有效的插值程序已经提出了只有少数理论。本文给出了一种完全的无量词Presburger算术公式的插值方法。我们提出了一个新的凸变量投影整数不等式和技术，将它们与等式。插值的推导在反驳证明的规模上具有低次多项式的复杂性，并且在实践中通常是快速的。
2008-11-21 cs.LO cs.SC
Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
University of Amsterdam（阿姆斯特丹大学）；University of Groningen（格罗宁根大学）
本文解决了悬而未决的PDL Craig插值问题，基于Borzechowski的硕士论文提出循环表方法，构造性证明插值性质并给出Haskell实现，还提及Lean形式化验证的相关工作。
2026-11-02 cs.LO math.LO
Proof Tree Preserving Interpolation
克雷格插值在SMT是困难的，因为，e。例如，在一个实施例中，理论组合和整数割引入了混合文字，即。例如，包含来自两个输入公式的局部符号的文字。在本文中，我们提出了一个计划，计算克雷格插值混合文字的存在。与现有方法相反，该方案既不限制SMT求解器所做的推理，也不在提取插值之前转换证明树。我们的计划工程未解释的功能和线性算术的组合，但可扩展到其他理论。该方案在插值SMT求解器SMTInterpol中实现。
2017-05-15 cs.LO
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
Interpolation with Automated First-Order Reasoning
University of Potsdam（波茨坦大学）
从一阶逻辑全自动定理证明角度研究插值法，介绍克雷格插值的两阶段方法及获取基础插值的方式，提及等式编码等贡献，还引入二阶量词消除作为统一插值方法并描述相关算法。
2026-07-08 cs.LO
Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic
本文研究一阶模态逻辑中插值和定义存在性的可判定性，证明在S5和K的单变元片段中该问题可判定，但一致插值不可判定，并给出复杂性上界。
2025-10-07 cs.LO
A Survey of Satisfiability Modulo Theory
可满足性模理论（SMT）是检验一阶公式在线性整数或实数算术或其他理论上的可满足性。在这篇综述中，我们解释了命题可满足性和合取的决策过程的组合，称为DPLL（T），以及替代的“自然域”方法。我们还涵盖了量词，克雷格插值，多项式算术，以及SMT求解器如何用于自动软件分析。
2016-06-15 cs.LO
The interpolant existence problem for weak K4 and difference logic
针对弱 K4 与差分逻辑 DL 不具 Craig 插值性质的问题，本文用多项式或三指数大小的互模拟反例模型刻画插值元不存在性，确定其存在性问题的复杂度上界并证明弱 K4 的 coNExpTime 困难性。
2024-06-17 cs.LO
Efficient Interpolation for the Theory of Arrays
现有的Craig插值技术对于计算序列和树插值的数组理论的无量词片段是低效的：求解器需要为插值问题的每个分区$(A, B)$运行，以避免创建$AB$ -混合项。我们提出了一种新的方法，使用证明树保持插值和阵列求解器的基础上弱等价阵列。我们给出了一个插值算法的引理阵列求解器。计算的插值有最坏情况下的指数大小的扩张性引理和最坏情况下的平方大小，否则。我们表明，这些界限是严格的意义上说，有引理没有更小的插值。我们实现了该算法，并表明所产生的插值是有用的，以证明内存安全的C程序。
2018-08-03 cs.LO
Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux
我们开发的基础计算克雷格插值和类似的中间体的两个给定的公式与一阶定理证明，构造子句表。可以这样理解的证明器包括基于两类演算的高效的面向机器的系统：面向目标的，如模型消除和连接方法，以及自底向上的，如超表演算。Craig-Lyndon插值的方法涉及一个提升步骤，其中术语被量化的变量所取代，类似于已知的基于分辨率的插值，但应用于不同特征的地面公式，并在Herbrand定理的基础上证明更抽象地正确，独立于特定的微积分。访问插值是一种用于数据库查询重构的最近形式的插值，其适用于具有相对化量词的一阶公式，并约束谓词出现的量化模式。它以前已经在Smullyan的非小句tableaux的框架内进行了研究。在这里，从本质上讲，我们模拟这些与更多的面向机器的子句tableaux通过结构约束，可以确保直接由自下而上的tableau建设方法，或封闭的子句tableaux与任意演算构建，通过后处理与重组转换。
2018-10-18 cs.LO
Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
该研究证明稳定模型语义下逻辑程序的射影Beth可定义性定理，提出通过一阶Craig插值构造强等价程序的方法，并通过原型实现验证其可行性，推动可定义性与插值方法向回答集编程的迁移应用。
2024-04-28 cs.LO
Interpolation in Classical Propositional Logic
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Potsdam（波茨坦大学）；University of Liverpool（利物浦大学）
研究经典命题逻辑中的插值法等相关概念，提出通过量词消去等四种方法计算插值，最后探讨了插值规模与电路复杂性的关系。
2026-07-08 cs.LO
Interpolation in First-Order Logic
该章节系统梳理一阶逻辑及其句法片段的 Craig 插值理论、改进结果、应用及插值元计算问题，为相关文献提供入门导引。
2025-10-04 cs.LO
Unary negation
我们研究片段的一阶逻辑和最少不动点逻辑，只允许一元否定：否定的公式，最多一个自由变量。这些逻辑概括了许多有趣的已知形式主义，包括模态逻辑和$μ$ -演算，以及合取查询和一元数据。我们证明了可满足性和有限可满足性对于两个片段都是可判定的，并且我们指出了可满足性、有限可满足性和模型检验的复杂性。我们还表明，一阶逻辑的一元否定片段是模型理论上表现良好。特别是，它享有克雷格插值和投影贝丝财产。
2013-09-23 cs.LO
Interpolation-Based GR(1) Assumptions Refinement
本文考虑的问题，假设细化的背景下，反应系统的不可实现的规格。提出了一种新的基于Craig插值的GR（1）规格的对策指导综合方法。我们的基于插值的方法识别不可实现的原因，并计算直接针对不可实现的核心的假设，而不需要用户输入。因此，我们讨论了这个属性如何减少收敛到可实现性所需的最大步骤数与其他技术相比。我们描述的插值产生有用的GR（1）假设的性质，并证明结果的合理性。最后，我们证明了我们的方法比基线技术产生更弱的假设，并通过现有技术在案例研究中找到无法解决的解决方案。
2018-10-31 cs.LO
Lazy Decomposition for Distributed Decision Procedures
软件和硬件验证自动化工具的日益普及对底层决策过程提出了越来越高的要求。本文提出了一个分布式决策过程（一阶问题）的框架克雷格插值的基础上。公式是以一种懒惰的方式分发的，即，而不使用昂贵的分解算法。潜在的模型被证明是不正确的，通过使用克雷格插值和解。具有挑战性的命题可满足性问题的实验结果表明，我们的方法是能够优于传统的解决技术，即使不使用额外的资源。
2011-11-02 cs.DC cs.LO cs.SE
Quantifier Elimination and Craig Interpolation, Quantitatively
Cornell University（康奈尔大学）；RWTH Aachen University（亚琛工业大学）
本文提出首个针对定量分段线性量的QE算法，并展示了其在概率程序验证中的应用，包括定量CI定理和期望结果计算。
2026-01-09 cs.LO cs.PL
Resolution Proof Transformation for Compression and Interpolation
基于SAT、SMT和定理证明的验证方法通常依赖于不可满足性证明作为提取信息的强大工具，以减少总体工作量。例如，可以遍历证明以识别导致不可满足性的最小原因，用于计算抽象或用于导出克雷格插值。在本文中，我们专注于两个重要的方面，涉及有效处理证明的不满足性：压缩和操纵。首先，由于证明的大小通常可以非常大（输入问题的大小呈指数级），因此采用技术来压缩它以进行进一步处理确实是有益的。其次，证明可以作为一个灵活的预处理步骤，为插值计算做准备。这两种技术都是在一个框架中实现的，该框架利用本地重写规则来转换证明。我们表明，仔细使用的规则，结合现有的算法，可以导致有效的简化原始证明。我们已经评估了几个算法在广泛的不满意的问题，来自SAT和SMT测试用例。
2014-04-15 cs.LO
Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations
本文首次证明一阶逻辑可判定片段中插值存在性问题不可判定，具体包括具有两个等价关系的二变量片段及其有保护扩展，并确定了相应的布尔描述逻辑情形。
2024-04-03 cs.LO math.LO
On the Completeness of Interpolation Algorithms
该研究聚焦插值算法可得到的插值元范围问题，定义了插值算法的完备性概念，并针对多类逻辑的标准消解与相继式演算算法，得出了不完备性及不同类型的完备性结果。
2025-01-11 cs.LO math.LO
Interpolation and Model Checking for Nonlinear Arithmetic
提出了一种新的基于模型的可满足性模理论插值方法。该过程使用了一种新的与SMT求解器的交互模式，我们称之为求解模模型。这要么将给定的部分模型扩展为一组断言的完整模型，要么在不存在解决方案时返回解释（模型插值）。这种交互模式非常适合SMT的模型构建可满足性（MCSAT）框架。我们用它来开发任何MCSAT支持的理论的插值程序。特别是，这种方法导致了一个有效的非线性实算术插值程序。我们评估新的程序，将其集成到一个模型检查器，并将其与最先进的非线性算法的模型检查工具进行比较。
2021-06-08 cs.LO cs.PL cs.SC
