Craig Interpolation for Quantifier-Free Presburger Arithmetic
克雷格插值已成为一个通用的算法工具，以提高软件验证。例如，插值可以加速无限状态系统的不动点计算的收敛。它们还有助于改进迭代计算的惰性抽象的细化。有效的插值程序已经提出了只有少数理论。本文给出了一种完全的无量词Presburger算术公式的插值方法。我们提出了一个新的凸变量投影整数不等式和技术，将它们与等式。插值的推导在反驳证明的规模上具有低次多项式的复杂性，并且在实践中通常是快速的。
2008-11-21 cs.LO cs.SC
Short Presburger arithmetic is hard
研究了Presburger算法（Short-PA）中短句的计算复杂性。这里的“短”是指具有有限数量的变量、量词、不等式和布尔运算的句子;输入仅由线性不等式中涉及的整数系数组成。证明了当第一个量词为$\exists$或$\forall$时，含有$m+2$交替量词的短PA句的可满足性分别是$Σ_{P}^m$ -完全或$Π_{P}^m$ -完全的.对计数版本和受限系统也进行了分析。进一步应用于随机优化中两个自然问题的困难性。
2017-10-20 cs.CC cs.LO math.CO
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic
本文提出了一种近似方法来验证计数器系统相对于线性时态逻辑的表达计数扩展中制定的属性。它可以表达，例如，通过对运行中的特定位置进行计数并施加算术约束，确保应答的数量永远不会超过对服务的请求的数量。所解决的问题是不可判定的，因此解决了平坦的下近似的系统。这提供了一个灵活的可调整的穷举和计算工作量之间的权衡，类似于有界模型检验。最近的技术和结果的平坦Kripke结构的模型检查频率特性的解除和构造一个参数化编码的（近似）问题的量化器免费Presburger算法。基于z3 SMT求解器的原型实现证明了基于RERS挑战赛问题的方法的有效性。
2019-01-17 cs.LO cs.SE
On Presburger arithmetic extended with non-unary counting quantifiers
研究扩展了非一元计数量词的Presburger算术，通过量词消去与归约技术证明其满足性在两重指数空间内可判定，并给出不同量词组合下的计算复杂度上界。
2023-07-11 cs.LO
One-Parametric Presburger Arithmetic has Quantifier Elimination
本文提出了单参数Presburger算术的量词消去算法，解决了相关开放问题，并证明其存在片段的可满足性问题属于NP且最小解具多项式位大小。
2025-06-30 cs.LO cs.SC
On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics
在过去的几十年里，大量的努力投入到确定一阶逻辑的可判定片段。这种努力产生了，除其他外，两个变量的片段和守卫片段，这取决于对语言公式施加的限制类型。尽管上述逻辑在形式化验证和知识表示等领域取得了成功，但这种一阶片段太弱，无法表达影响网络建模或统计推理所需的最简单的统计约束。在这项工作中，我们研究了这些经典的可判定逻辑与百分比量词的扩展，指定如何频繁的一个公式是满足缩进模型。令人惊讶的是，我们发现，所有提到的可判定的片段成为不可判定下这样的扩展，锐化文献中现有的结果。我们的负面结果补充的决定性的两个变量的守卫片段，甚至更有表现力的计数，即Presburger约束。我们的研究结果可以应用于推断各种模态和描述逻辑，如Presburger模态逻辑与逆向或ALCI，表达基数约束的可判定性。
2021-10-03 cs.LO
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
2018-04-28 cs.FL cs.LO
Interactive Realizers and Monads
我们提出了一个可实现的解释系统的量词自由算术，这是相当于经典算术的片段没有“嵌套”量词，这里称为EM 1-算术。我们将经典证明解释为交互式学习策略，即通过与“环境”和彼此交互来经历知识和学习的几个阶段的过程。我们通过两个合适的单子的建设给出了一个分类介绍的解释。
2010-05-17 cs.LO
Uniform Realizability Interpretations
Swansea University（斯旺西大学）；Queen Mary University of London（伦敦玛丽女王大学）
本文提出统一可实现性框架，统一并泛化逻辑中各种可实现性解释，重点处理原子公式和量词，兼顾经典与现代变体。
2026-03-04 cs.LO
Ramsey Quantifiers in Linear Arithmetics
本研究提出一种可从LIA、LRA、LIRA三种线性算术SMT理论中消除拉姆齐量词的多项式时间算法，解决了相关良基性检查、一元可分解性等开放问题，并在原型测试中取得良好效果。
2023-11-07 cs.FL cs.LO
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
一元可分解性是变量独立性的概念，它询问一阶理论中的给定公式是否可以表示为理论中一元谓词的布尔组合。最近，Veanes等人在SMT的上下文中展示了一元可分解性的有用性（即输入公式是无量词的），并发现了各种有趣的应用，包括字符串分析。然而，检查一元可分解性通常是不可判定的。某些理论的可判定性是已知的（例如，Presburger算术，Tarski的实闭域），但关于它们的计算复杂性的结果很少。本文研究了整数线性算术在SMT下的一元可分解性。我们表明，这个决策问题是CONP-完全的，当monadically可分解，一个公式承认在最坏的情况下分解的指数大小。我们提供了一个新的应用程序，我们的结果字符串约束求解长度约束。然后，我们扩展我们的结果变元分解，谓词可以承认多个自由变量（相对于一元分解）。最后，我们给出了整数线性算术中的量词消去的一个应用，其中量词块中的变量，如果是独立的，可以用指数（而不是标准的双指数）爆破消除。
2020-04-26 cs.LO
The strength of replacement in weak arithmetic
替换（或集合或选择）公理方案断言有界量词交换。我们证明了这个计划的独立性，从各种弱理论的算术，有时在复杂性的假设。
2004-09-08 cs.CC cs.LO
Analysis of logics with arithmetic
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
2025-10-29 cs.LO
Provably Total Functions of Arithmetic with Basic Terms
给出了一阶算术可证递归函数的一个新的刻画。它的主要特点是在量词规则中只使用由0、后继S和变量组成的项，即泛消和存在引进。
2012-01-05 cs.LO
Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
证明了对于任何固定的$i>0$，Presburger算术的$Σ_{i+1}$ -片段，即，它对以存在量词开始的$i+1$量词交替的限制对于$\mathsfΣ^{\mathsf{EXP}}_{i}$是完全的，$\mathsfΣ^{\mathsf{EXP}}_{i}$是弱EXP层次的第$i$层，是驻留在$\mathsf{NEXP}$和$\mathsf{EXPSPACE}$之间的多项式时间层次的类似物。这一结果完成了Presburger算法的计算复杂性景观，这一研究可以追溯到Fischer & Rabin在1974年的开创性工作。此外，我们应用的一些技术开发的证明的下限，以建立界限上的自然定义的$Σ_1$ -片段Presburger算法：给定一个$Σ_1$ -公式$Φ(x)$，它表明，一组非负的解决方案是一个最终的周期集，其周期是最多双指数，这个界是紧的。
2014-05-12 cs.LO
Separation of bounded arithmetic using a consistency statement
本文证明了Buss的有界算术族$S^1_2 \subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$不完全坍缩.更准确地说，我们证明，对于一定的$D$，$S^1_2 \subsetneq S^{2D+5}_2$持有。此外，我们可以允许$S^1_2, S^2_2, \ldots$的BASIC公理的真量词自由公式的任何有限集。根据Takeuti的论点，这意味着$\mathrm{P} \neq \mathrm{NP}$。设$\mathbf{Ax}$是BASIC公理的一个特定公式。我们证明$S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$足够大的$D$，而$S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$的系统$\mathrm{PV}^-_1(D)$，系统$\mathrm{PV}^-_1$的一个片段，诱导免费的库克的$\mathrm{PV}$，其中证明只包含公式小于$D$连接词的一阶扩展。$S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$的证明是通过直接改编的$\mathrm{…
2019-10-30 cs.LO math.LO
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
我们在定理证明器Isabelle/HOL中形式化了一个多元量词消去（QE）算法。我们的算法是完整的，因为它能够减少任何量化的公式在一阶逻辑的实算术到一个逻辑等价的量词自由公式。我们形式化的算法是Tarski的原始QE算法和Ben-Or，Kozen和Reif算法的混合，它是第一个完整的多元QE算法形式化的Isabelle/HOL。
2022-12-20 cs.LO math.AG
Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
Institute of Science and Technology Austria（奥地利科学技术研究所）；Hong Kong University of Science and Technology（香港科技大学）；Vienna University of Technology（维也纳工业大学）；Singapore Management University（新加坡管理大学）
针对量词化线性与非线性实算术公式可满足性判定中量词消去成本高昂的瓶颈，提出基于模板的Skolem化方法，利用代数几何定理自动合成函数消去量词，在理论与实验上均优于现有SMT求解器。
2024-12-18 cs.AI cs.LO
Quantifier Elimination and Craig Interpolation, Quantitatively
Cornell University（康奈尔大学）；RWTH Aachen University（亚琛工业大学）
本文提出首个针对定量分段线性量的QE算法，并展示了其在概率程序验证中的应用，包括定量CI定理和期望结果计算。
2026-11-10 cs.LO cs.PL
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
研究了带未解释一元谓词的差分逻辑的可判定性，证明实数上带单个未解释一元谓词的量化差分逻辑不可判定，而整数差分逻辑结合实数序与未解释一元谓词仍可判定。
2023-05-24 cs.LO
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version)
我们研究了在分离逻辑中增加指针运算的复杂性后果。具体来说，我们研究扩展的点到片段的符号堆分离逻辑与各种形式的Presburger算术约束。最重要的是，我们发现，即使在最小的情况下，当我们只允许简单的“差异约束”的合取，（x ′ \leq x+k）其中k是整数，多项式时间可判定性已经是不可能的：可满足性成为NP完全，无量词蕴涵成为CoNP完全蕴涵，量化蕴涵成为P2完全蕴涵（P2是多项式时间层次中的第二类）事实上，我们证明了上界是相同的，P2，即使对于全指针算术，但具有固定的指针偏移量，其中我们允许初等公式的任何布尔组合（x '= x+ k 0），（x' \leq x+ k 0）和（x'<x+ k 0），并且，除了指向公式之外，我们允许长度由k 0限定的数组的空间公式和长度由k 0限定的列表等，其中k 0是固定整数。然而，如果我们允许一种更有表现力的指针算术形式-即任意指针和上的基本公式的任意布尔组合-那么对于可满足性和无量化器蕴涵来说，复杂度的增加相对温和：它们仍然分别是NP-完全和coNP-完全的，并且对于量化蕴涵来说，复杂度似乎急剧增加。
2018-03-08 cs.LO
Peano Arithmetic and $μ$MALL
本研究提出基于线性逻辑的算术形式理论$μ$MALL，展示其函数计算方式，扩展得到经典算术系统$μ$LK+并证明其一致性、包含皮亚诺算术及相关保守性结果。
2025-08-22 cs.LO
The Yoneda Reduction of Polymorphic Types (Extended Version)
在本文中，我们探讨了一个家庭的类型同构的系统F的有效性，语义对应的某种形式的Yoneda同构从范畴论。这些同构在比β-η-等价更强的等价理论下成立，就像那些由参数性和非自然性引起的理论一样。我们表明，米田型同构产生重写的类型，我们称之为米田减少，它可以用来消除量词从多态类型，取代它们与单态类型构造函数的组合。我们建立了一些充分条件下，量词可以完全消除多态类型，我们展示了一些应用这些条件来计算居民的类型和计算程序等价系统F的一些片段。
2020-10-30 cs.LO math.LO
On Quantifiers for Quantitative Reasoning
University of Strathclyde（斯特拉斯克莱德大学）
本文提出了一种基于实数的量化谓词逻辑，引入非线性、线性加法和线性乘法连接词，并探讨了均值和调和均值作为量词的语义，同时展示了softmax和Rényi熵在该逻辑中的应用。
2025-12-02 cs.LO math.LO
Succinct Population Protocols for Presburger Arithmetic
Angluin等人证明了种群协议可以精确地计算Presburger算法（PA）中定义的谓词，Presburger算法是加法的一阶理论。作为这一结果的一部分，他们提出了一个程序，将带有余数谓词的无量词PA的任何公式$φ$（其具有与完整PA相同的表达能力）转换为具有计算$φ$的$2^{O(\text{poly}(|φ|))}$状态的群体协议。更准确地说，协议的状态数与公式中最大系数的位长和语法树的节点数都是指数关系。本文证明了带有剩余谓词的无量词PA的每个公式$φ$都可由具有$O(\text{poly}(|φ|))$状态的无领导种群协议计算。我们的证明是基于几个新的建设，这可能是独立的利益。给定一个带有余数谓词的无量词PA的公式$φ$，第一个构造产生一个计算$φ$的简洁协议（带有$O(|φ|^3)$前导）;这完成了在[STACS'18]中开始的工作，在那里我们为PA的一个片段构造了这样的协议。对于足够大的输入，我们可以摆脱这些领导者。如果输入不够大，那么它就很小，我们设计另一个构造，产生一个简洁的协议，其中一个领导者计算$φ$。我们的最后一个建筑摆脱了这个领导者的小投入。
2020-01-13 cs.CC cs.DC cs.LO
A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)
本文提出一种新形式化模型，通过操作语义一劳永逸地证明将复杂基于E-matching的公理化提供给Z3或cvc5等SMT求解器不会导致非终止，并以Dafny和Viper的集合论公理化终止性证明验证有效性。
2024-04-27 cs.LO
A Survey of Satisfiability Modulo Theory
可满足性模理论（SMT）是检验一阶公式在线性整数或实数算术或其他理论上的可满足性。在这篇综述中，我们解释了命题可满足性和合取的决策过程的组合，称为DPLL（T），以及替代的“自然域”方法。我们还涵盖了量词，克雷格插值，多项式算术，以及SMT求解器如何用于自动软件分析。
2016-06-15 cs.LO
Embedded Finite Models Beyond Restricted Quantifier Collapse
该研究突破嵌入有限模型论的两种极端认知，证明可判定结构内逻辑求值复杂度范围极广且表达能力与复杂度可脱节，还证实有限域等理论不满足量词坍缩并给出域理论判定复杂度新下界。
2024-05-20 cs.LO math.LO
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic
分离逻辑（SL）是一种众所周知的断言语言，用于具有动态分配的数据结构的程序的霍尔式模块化证明系统中。在本文中，我们研究的片段限制到Bernays-Schoenfinkel-Ramsey量词前缀$\exists^*\forall^*$，其中的量化变量的范围内的一组内存位置的一阶SL。当这个集合是未解释的（没有相关的理论）时，片段是PSPACE完备的，这与无量词片段的复杂性相匹配。然而，当量词前缀属于$\exists^*\forall^*\exists^*$时，或者当存储器位置被解释为具有线性算术约束的整数时，SL变得不可判定，从而为SL内的可判定性设置了清晰的边界。我们已经实现了一个决策程序的可判定片段的$\exists^*\forall^*$ SL作为一个专门的求解器内的DPLL（$T$）架构，在CVC 4 SMT求解器。我们的实现进行了评估，使用两组验证条件，产生（i）展开归纳谓词，和（ii）最弱的基于前置条件的验证条件生成器。实验数据表明，自动化的量词实例化具有很小的开销相比，手动基于模型的实例化。
2016-11-23 cs.LO
What's Decidable About Sequences?
我们提出了一个一阶理论的序列与整数元素，Presburger算法，并定期约束，它可以建模的重要属性的数据结构，如数组和列表。我们给出了一个决定程序的量化器的自由片段，编码到一阶理论的级联的基础上，该程序具有PSPACE复杂性。序列理论的无量词片段可以表达诸如排序性和内射性之类的属性，以及与序列的元素及其位置相关的周期性和算术事实的布尔组合（例如，“对于所有偶数i，位置i的元素具有值i+3或2i”）。由此产生的表达能力是正交的最具表现力的可判定逻辑数组。一些例子表明，该片段也适用于推理的标准框架内的公理语义序列操纵程序。
2011-02-10 cs.LO
Verified Quadratic Virtual Substitution for Real Arithmetic
本文提出了一种在Isabelle/HOL中通过线性和二次虚拟替换（VS）实现的一阶实数运算的形式化量词消去（QE）算法. Tarski-Seidenberg定理证明了实数运算的一阶逻辑可以由QE判定。然而，在实践中，QE算法是高度复杂的，并且经常结合多种方法来提高性能。VS是一个实际上成功的QE方法，目标是具有低次多项式的公式。据我们所知，这是第一个工作，正式VS二次实数算术，包括不等式。证明需要各种贡献，现有的多元多项式库在伊莎贝尔/HOL。我们的框架是模块化的，易于扩展（以方便集成未来的优化），并可以作为开发实用的通用QE算法的基础。此外，由于我们的形式化设计考虑到了实用性，我们将我们的开发导出到SML，并在文献中的378个基准上测试生成的代码，与Redlog，Z3，Wolfram Engine和SMT-RAT进行比较。这发现了一些工具中的不一致之处，强调了一种经过验证的方法对真实算术的复杂性的重要性。
2021-11-22 cs.LO
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.LO
Universal quantification makes automatic structures hard to decide
University of Oxford（牛津大学）；University of Warwick（华威大学）
本文证明了自动结构中消除全称量词时，最小NFA的识别语言需二次指数级复杂度，且判断语言是否为空为EXPSPACE完全问题。
2026-02-26 cs.LO
On the freeze quantifier in Constraint LTL: decidability and complexity
约束LTL是LTL在Presburger约束上的推广，通常被用作一种形式语言来描述具有约束的操作模型的行为。冻结量词可以是语言的一部分，如在一些实时逻辑中，但这种变量绑定机制在许多逻辑语言中（一阶时态逻辑，混合逻辑，序列图逻辑，导航逻辑，具有抽象的逻辑等）是相当普遍和普遍的。我们表明，约束LTL在简单的域（N，=）增加了冻结量词是不可判定的，这是一个令人惊讶的结果，鉴于穷人的语言约束（只有平等测试）。许多版本的无冻结约束LTL在具有定性谓词的域上是可判定的，我们的不可判定性结果实际上建立了Sigma_1^1-完备性。在积极的一面，我们提供的复杂性结果时，域是有限的（EXPSPACE-完备性）或当公式是平坦的，在某种意义上介绍的文件。我们的不可判定性的结果是尖锐的（即限制变量的数量），我们所有的复杂性特征确保完整性方面的一些复杂性类（主要是PSPACE和EXPSPACE）。
2006-09-29 cs.CC cs.LO
Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
本文利用博弈论见证结果与Krajíček技术的扩展，证明了有界算术理论（如APC1和TPV^i）无法证明分离多项式层级更高层的强复杂度下界。
2023-05-24 cs.CC cs.LO
Decidable Horn Systems with Difference Constraints Arithmetic
研究了Horn子句递归系统解的存在性问题，其中二阶变量被解释为整数关系，并利用无量词差界算法.我们从证明问题的可判定性开始“系统有解吗？“对于一类具有一个二阶变量和一个非线性递归规则的简单Horn系统，证明依赖于一个树自动机的建设，承认在加权图对应的每一个展开树的霍恩系统的所有周期。我们约束树识别只有负权重的周期，通过添加一个Presburger公式，利用每个规则被解雇的次数，并减少我们的问题的普适性Presburger约束树自动机。我们研究了这个问题的复杂性，发现它是在\textsc{NEXPtime}与\textsc{EXPtime} -硬下界。其次，我们放弃了单变量的限制，并考虑多变量二阶Horn系统的结构限制，称为\emph{flatness}。这类更一般的霍恩系统被发现是可判定的，在相同的复杂性范围内。最后，我们使用Horn系统对交替分支向量加法系统（ABVASS）的可达性问题进行了编码，并证明了对于平坦ABVASS，该问题是在co- \textsc{NEXPtime}中的。
2016-02-14 cs.FL cs.LO
