Adapting Real Quantifier Elimination Methods for Conflict Set Computation
实闭域上的可满足性问题是可判定的。在可满足性模理论的背景下，限制于文字的合取集，即多项式约束集的问题是特别重要的。中心问题之一是计算这些集合的不可满足性的良好解释，即获得其合取已经不可满足的输入约束的小子集。我们采用两种常用的实量词消去方法，柱形代数分解和虚拟替代，提供这样的冲突集，并证明我们的方法在实践中的性能。
2015-11-03 cs.LO
Partial Quantifier Elimination
本文研究了部分量词消去（PQE）问题。给定公式exists（X）[F（X，Y）& G（X，Y）]，其中F，G是合取范式，PQE问题是寻找一个公式F*（Y），使得F* & exists（X）[G]与exists（X）[F & G]逻辑等价.我们解决PQE问题，通过生成和添加到F子句的自由变量，使条款的F与量化的变量冗余。传统的量词消去问题（QE）是PQE的一种特殊情况，其中G为空，因此需要使具有量化变量的输入公式的所有子句变得冗余。PQE的重要性是双重的。首先，许多问题更自然地用PQE而不是QE来表述。其次，在许多情况下，PQE可以比QE更有效地解决。我们描述了一个PQE算法的依赖序列的机器的基础上，并给出实验结果显示的承诺PQE。
2017-04-01 cs.LO
Transfer Function Synthesis without Quantifier Elimination
传统上，传递函数是针对程序中的每个操作逐个指令地手动设计的。在这样的设置中，传递函数描述单个指令的语义，详细说明给定的抽象输入状态如何映射到抽象输出状态。一个指令序列（一个基本块）的净效应可以通过组成组成指令的传递函数来计算。然而，可以通过应用单个传递函数来提高精度，该传递函数将块的语义作为一个整体来捕获。由于块是依赖于程序的，因此这种方法需要自动化。因此，人们对自动计算传递函数越来越感兴趣，最显著的是使用基于量词消去的技术。虽然概念上优雅，量词消去不可避免地引起计算瓶颈，这限制了这些方法的适用性，以小块。本文提供了一种计算传递函数的方法，该方法完全消除了量词消去，因此可以被看作是对这个问题的回应。该方法的实用性证明了通过生成传递函数的输入和输出状态所描述的线性模板约束，其中包括间隔和八边形。
2012-09-28 cs.LO
Partial Quantifier Elimination And Property Generation
本文研究了命题CNF公式的部分量词消去（PQE），提出两种PQE求解器，并证明其在性质生成、验证有缺陷的FIFO缓冲区及电路不变式生成中优于完整量词消去。
2023-05-25 cs.LO
Table-based Quantifier Elimination
Independent Researcher（独立研究者）
提出一种基于表的量词消去方法，用于求解受限公式的可满足性问题，并在SMT求解器预处理器中实现，利用SQLite高效执行关系操作，在SAT和ASP基准测试上提升性能。
2026-06-25 cs.LO
Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits
本文提出一种谓词逻辑模型，其中每个术语和谓词都有独立于变量赋值的绝对指称，通过代数和替换、量词等概念实现，并证明了普通模型可转换为该模型，从而证明了完备性。
2023-12-27 cs.LO
Partial Quantifier Elimination By Certificate Clauses
本研究提出基于证书子句的命题CNF公式部分量词消去算法START，可用于时序电路不变式生成与缺陷检测，在FIFO缓冲器和HWMCC-13基准上表现出优于现有方法的缺陷发现能力。
2024-08-17 cs.LO
Structure-Aware Computing, Partial Quantifier Elimination And SAT
本文探讨了通过部分量化消除实现结构感知计算的方法，展示了其在验证问题中的应用，并论证了量化消除本身可受益于结构感知计算。
2026-05-11 cs.LO
Verification Of Partial Quantifier Elimination
本文针对部分量词消去（PQE）求解器结果难以验证的问题，提出了一个简单的基于SAT的验证器VerPQE，并通过实验结果证明了其有效性。
2023-04-03 cs.LO
Quantifier Elimination by Dependency Sequents
研究合取范式（CNF）中布尔公式的存在性量词消去问题.我们提出了一种新的方法来解决这个问题称为依赖序列的推导（DDS）。依赖性-冗余度（D-冗余度）用于记录一组量化变量在部分分配下是冗余的。我们引入了一个类似于解析的操作，称为join，它从两个现有的D序列中产生一个新的D序列。我们还表明，DDS是合成的，即如果我们的输入公式是一个连接的独立公式，DDS自动识别和利用这些信息。我们介绍了一种基于DDS的算法，目前的实验结果表明其潜力。
2013-06-02 cs.LO
Quantifier Elimination With Structural Learning
考虑了含有存在量词的命题CNF公式的量词消去问题。QE在形式化验证中起着关键作用。前面，我们提出了一种基于以下观察的方法。为了执行量化宽松，人们只需要添加一组依赖于自由变量的子句，这使得量化子句（即具有量化变量的子句）冗余。为了实现这种方法，我们引入了一个分支算法，使量化子句在子空间中冗余，并合并分支的结果。为了实现这个算法，我们开发了机器的D-序列。D-子句是一个记录，说明量化子句在指定的子空间中是冗余的。子句的冗余是一种结构属性（即，它只适用于逻辑上等价的公式的子集，而不是语义属性）。因此，在SAT问题中，重复使用D-序列并不像重复使用冲突子句那么容易。在本文中，我们解决这个问题。我们引入了一个新的定义的D-序列，使他们的可重用性。我们开发了一个理论，表明在什么条件下，D-射线可以安全地重复使用。
2018-10-15 cs.LO
Quantifier Elimination over Finite Fields Using Gröbner Bases
利用格罗布纳基方法，给出了有限域上一阶理论的一个代数量词消去算法.该算法依赖于有限域上的强零点和消去理想的性质。我们分析了算法的理论复杂性，并展示了其在生物控制器模型的形式化分析中的应用。
2011-04-05 cs.LO cs.SC
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
Seoul National University（首尔大学）
我们在循环不变推理的上下文中解决谓词生成问题。受基于插值的抽象精化技术的启发，我们应用插值定理来合成程序文本隐含的谓词。我们的技术能够提高[14]中基于学习的循环不变推理算法的有效性和效率。我们报告的实验结果的例子，从Linux，SPEC2000，和焦油实用程序。
2012-09-28 cs.LG cs.LO
Fast Approximations of Quantifier Elimination
针对精确量词消去计算成本高的问题，提出基于egraph数据结构的QEL框架，统一支持量化约简与基于模型的投影，实现了数组和ADT理论的MBP，集成到Z3后在相关任务中性能优于现有最优方法。
2023-06-16 cs.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
A general approach to asymptotic elimination of aggregation functions and generalized quantifiers
Uppsala University（乌普萨拉大学）；Ludwig-Maximilians-Universität München（慕尼黑路德维希-马克西米利安大学）；German University of Digital Science（德国数字科学大学）
本文提出一种基于局部连续性概念的一般方法，用于渐近消除单位区间真值逻辑中的聚合函数，并间接消除莫斯托夫斯基风格广义量词。
2025-11-18 cs.LO math.LO
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
University of Potsdam（波茨坦大学）
近年来，哥德尔的本体论证明及其变体被形式化，并以各种方式使用自动化工具进行分析。我们补充这些分析与建模的基础上扩展谓词量化的一阶逻辑在自动化环境中。公式宏用于构造复杂的公式和任务。分析作为一个生成的类型集文件，其中非正式的解释穿插着漂亮的打印公式和输出的推理机的一阶定理证明和二阶量词消去。以前未被注意或模糊的方面和细节哥德尔的证明变得明显。二阶量词消去的实际应用的可能性和遇到的消除任务可以作为基准。
2021-10-21 cs.AI cs.LO
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
本文描述了离散实闭域在Coq证明助手中的形式化。这个抽象的结构捕捉例如实代数数的理论，一个具有良好算法性质的实数的可判定子集。实代数数和更一般的半代数簇的理论是实分析中许多有效方法的核心，包括非线性算术的决策过程或实值函数的优化方法。在定义了离散实闭域的抽象结构和多项式实根的基本理论之后，根据计算机代数中关于量词消去的标准文献，给出了一个基于伪余项序列的代数证明的形式化.这种形式化涵盖了理论的很大一部分，这是在计算机代数实践中实现的有效算法的基础。这项工作的成功为这些有效方法的正式认证铺平了道路。
2012-02-15 cs.LO
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
Technische Universität Dresden（德累斯顿工业大学）
对于关系一元公式（Löwenheim类），二阶量词消去，这是密切相关的计算一致插值，投影和遗忘-操作，目前受到关注的知识处理-总是成功的。Heinrich Behmann从1922年开始对这个类的可判定性证明是通过等价保持公式重写的消元法进行的。在这里，我们重建的结果从Behmann的出版物的详细和讨论相关的问题，在现代方法的背景下，二阶量词消去在计算逻辑。此外，广泛的文件的信件和手稿在贝曼的遗赠，关注二阶量词消去，包括一个评论登记册和英文摘要的德语来源，重点是技术材料。在20世纪20年代后期，Behmann试图为谓词的元数大于1的公式开发一种基于消除的决策方法。他的手稿和与威廉·阿克曼的通信显示了今天仍然感兴趣的技术方面，并深入了解了阿克曼1935年的里程碑式论文“Untersuchungen über das Eliminationsproblem der mathematischen Logik”的起源，该论文奠定了两种流行的现代二阶量词消去方法的基础。
2017-12-19 cs.AI cs.LO
Pseudo-Complex Quantifier Elimination
Chalmers University of Technology and University of Gothenburg（查尔姆斯理工大学和哥德堡大学）；University of Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国研究与发展研究所、洛林计算与自动化实验室）；MPI-INF and Saarland University（德国马克斯·普朗克 informatics 研究所和萨尔兰大学）
提出一种在复数域上进行量词消去的框架，通过归约到实数量词消去并启发式重解释结果，在Logic1系统中实现并给出计算实例。
2026-06-12 cs.LO cs.SC
Quantifier Elimination for Statistical Problems
Microsoft Research（微软研究院）；Technion（以色列理工学院）
最近对Tarski的实数一阶理论中的量词消去过程进行了改进，使得完全自动地解决以下问题的小实例成为可能：1。列出了包含隐变量的图形模型所隐含的所有等式和不等式约束。2.将图形模型与隐藏变量（即，模型等价、包含和重叠）。3.关于模型或模型的一部分的识别，以及关于从模型导出的量的界限的问题。4.确定给定的一组独立断言是否。我们讨论了量词消去的基础，并演示了它在这些问题中的应用。
2013-01-23 cs.AI cs.LO
Property Checking Without Inductive Invariants
本文提出基于 PQE 的安全属性证明过程，无需生成归纳不变式，并借助深度优先搜索高效发现深层缺陷。
2020-10-29 cs.LO
Integer Linear-Exponential Programming in NP by Quantifier Elimination
本文提出基于量词消去的NP过程判定整数线性指数约束系统可解性，证明对应存在性理论的可满足性为NP完全，改进了EXPSPACE上界，并得到整数线性规划的非确定性多项式时间高斯消去变体。
2024-07-09 cs.LO
Partial Quantifier Elimination With Learning
我们考虑一个修改的量词消去（QE）问题称为部分QE（PQE）。在PQE中，只有一小部分公式被带出量词的范围。PQE的吸引力在于许多验证问题，例如等价性检查和模型检验，都可以归结为PQE，并且后者比完全QE容易得多。前面，我们介绍了一种基于D序列机制的PQE算法。D-C是一个记录，说明一个子句在一个量化的CNF公式中在一个指定的子空间中是多余的。为了使该算法有效，重要的是重用学习的D序列。然而，重用D-序列是不容易的SAT求解器中的冲突条款，因为冗余是一个结构，而不是语义属性。在前面，我们修改了D序列的定义，使其能够安全地重用。本文提出了一种基于新D序列的PQE算法。它在两个方面不同于它的前身。首先，新算法可以学习和重用D序列。其次，该算法逐一证明子句的冗余性，一旦当前目标子句在当前子空间中被证明是冗余的，就立即进行回溯。这使得新的PQE算法类似于SAT求解器，只要一个子句被证伪，就可以回溯。我们的实验表明，新的PQE算法优于其前身。
2019-07-13 cs.LO
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
2018-04-28 cs.FL cs.LO
One Quantifier Alternation in First-Order Logic with Modular Predicates
添加模谓词产生了一阶逻辑FO在词上的推广。FO[<，MOD]与顺序比较$x<y$和$x \equiv i \mod n$的谓词的表达能力已经由Barrington，Compton，Straubing和Therien研究过。FO[<，MOD]-片段的研究由Chaubard，Pin和Straubing发起。最近，Dartois和Paperman证明了双变量片段FO 2 [<，MOD]中的可定义性是可判定的。在本文中，我们继续这一工作路线。我们给出了Sigma 2 [<，MOD]中词语言的一个有效的代数刻画.片段Sigma 2由前束范式中的一阶公式组成，具有以存在块开始的两个量词块。此外，我们还证明了Sigma 2 [<，MOD]的最大子类Delta 2 [<，MOD]在否定下是封闭的，它具有与二元逻辑FO 2 [<，MOD]相同的表达能力。这将Therien和Wilke的结果FO 2 [<] = Delta 2 [<]推广到模块化谓词。作为副产品，我们获得了FO 2 [<，MOD]的另一个可判定的特征。
2014-07-01 cs.FL cs.LO
The Dual of Quantifier Elimination: Boolean Elimination over C and R
该研究通过证明在C和R上布尔组合的多项式等式和不等式可转换为单变量量词形式，提供了经典量词消除的对偶方法，展示了线性度数界和明确构造。
2025-12-22 cs.LO math.LO
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
本文提出一种基于结构约简的Petri网广义可达性属性检查方法，通过线性复杂度的变量消去投影过程将属性转化为约简网的等价公式，可作为现有模型检测器的预处理步骤，实验证明其在约简量有限时依然有效。
2024-01-08 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
Removal of Quantifiers by Elimination of Boundary Points
我们考虑从布尔CNF公式中消除存在量词的问题。我们的方法基于以下观察。通过增加F的预解式子句消除边界点，可以消除量化CNF公式F对一组变量的依赖性。这种方法类似于[9]中描述的量词消去方法。本论文中描述的方法的差异是双重的：{ \bullet }分支仅在量化变量上执行，{ \bullet }通过调用SAT求解器来执行边界点的显式搜索。尽管我们在此之前发表了论文[9]，但从时间上讲，本报告的方法首先开发。在[10]、[11]中对该方法进行了初步介绍。由于准备专利申请，我们推迟了这种方法的出版[8]。
2012-06-05 cs.DM cs.LO
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
研究了带未解释一元谓词的差分逻辑的可判定性，证明实数上带单个未解释一元谓词的量化差分逻辑不可判定，而整数差分逻辑结合实数序与未解释一元谓词仍可判定。
2023-05-24 cs.LO
Finite-Degree Predicates and Two-Variable First-Order Logic
我们考虑有限字上的二元一阶逻辑，其量词交替数是固定的。我们表明，所有的语言与一个中立的字母定义的顺序和有限程度的谓词也可以定义的顺序谓词。从这个结果中，我们得到了分离的交替层次的二元逻辑上的这个签名。
2015-07-29 cs.LO
A Simple Quantifier-free Formula of Positive Semidefinite Cyclic Ternary Quartic Forms
研究了半正定循环三元四次型的量词消去问题。我们利用完备判别系统理论、Maple15中的函数\RealTriangularize和所谓的对称不等式等式判定法解决了这个问题。提出了一个等价的简单无量词公式，该公式很难通过以往的方法或量词消去工具自动获得。
2012-10-17 cs.LO math.AG
The evaluation of geometric queries: constraint databases and quantifier elimination
我们对几何消除的算法任务进行建模（例如，实数和复数的基本场论中的量词消去）。作为一个特殊的情况下，这样的几何消除任务，我们认为样本点查询。我们展示了指数较低的复杂性边界，以评估几何查询在一般情况下，在特定情况下的样本点查询。虽然本文是理论性的，但其目的是探索计算机实现的约束数据库查询评估算法的可能性和（复杂性）限制，基于最先进的几何消除过程及其实现的原理，例如，“Kronecker”软件包。
2011-10-13 cs.CC cs.DB cs.LO
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report
通常，分布式系统的验证任务是通过计数器抽象来完成的。这种抽象有时可以通过模拟和互模拟来证明。在这项工作中，我们提供的逻辑基础，这种做法，通过一个专门设计的技术，二阶量词消去。我们的方法，一旦应用到规范的验证问题的参数化分布式系统，产生整数变量系统，准备好模型检查当前基于SMT的工具。我们证明了该方法的可行性与原型实现和第一次实验。
2017-12-05 cs.DC cs.LO cs.SE
Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability
我们证明了一个家庭的命题公式在合取范式，使一个公式的大小$N$需要大小$2^{Ω(\sqrt[7]{N/logN})}$反驳使用树型OBDD反驳系统Atserias，Kolaitis和Vardi关于所有变量排序。所有已知的符号量词消去算法在不可满足的CNF上运行时都生成树状证明，因此该下限适用于这些算法的运行时。此外，下界推广了早期基于OBDD的不可满足性证明的结果，因为它适用于所有变量排序，它适用于根据任意时间表处理子句时，它适用于通过量化消除变量时。
2007-01-09 cs.CC cs.LO
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
RPTU University Kaiserslautern-Landau（莱茵兰-普法尔茨技术大学凯泽斯劳滕-兰道分校）；Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）
REAL工具通过高效消除Ramsey量词，在LIRA中实现快速消除，应用于存活性检查和单子分解等程序验证问题。
2026-01-22 cs.FL cs.LO
The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating
我们研究消除量词在一阶公式通过希尔伯特的ε-运营商（或-粘合剂），以下伯奈斯的明确定义的存在和全称量词符号的ε-条款。这种消除在1939年希尔伯特-伯奈斯的第一个ε定理的证明中第一次明确出现。我们认为这个证据有一个漏洞。这种消除与明确定义总是终止的错误假设有关。令人惊讶的是，据我们所知，没有人证明这个消除过程的汇合或终止。甚至关于不融合和终止问题的公开性的神话也在流传。我们展示了这种消除过程的汇合和终止，通过一个直接的，简单的，易于验证的证明，基于一个新的定理，如何获得终止弱规范化。
2016-11-19 cs.LO math.LO
One-Parametric Presburger Arithmetic has Quantifier Elimination
本文提出了单参数Presburger算术的量词消去算法，解决了相关开放问题，并证明其存在片段的可满足性问题属于NP且最小解具多项式位大小。
2025-06-30 cs.LO cs.SC
Model Theory of Monadic Predicate Logic with the Infinity Quantifier
本文建立了模型理论性质的$\mathrm{FOE}^{\infty}$，一元一阶逻辑的变化，具有广义量词$\exists^\infty$（“有无限多”）。我们提供了语法定义的片段$\mathrm{FOE}^{\infty}$表征四个不同的语义属性的$\mathrm{FOE}^{\infty}$ -句子：（1）是单调的和（2）（斯科特）连续在一个给定的一元谓词集;（3）有真理下保持采取子模型或（4）不变量下采取继承。在每一种情况下，我们产生一个有效定义的映射，将任意句子$φ$翻译成属于相应句法片段的句子$φ^{p}$，其属性是$φ$等同于$φ^{p}$，当它具有相关的语义属性时。我们的方法是首先提供这些结果在更简单的设置一元一阶逻辑（$\mathrm{FOE}$）和（$\mathrm{FO}$）的平等，然后移动到$\mathrm{FOE}^{\infty}$包括广义量词$\exists^\infty$到图片。作为我们的推论，我们得到了上述四个语义性质对于$\mathrm{FOE}^{\infty}$ -语句是可判定的。此外，我们的结果是直接相关的自动机和表达模bisimilirity的一元二阶逻辑的变种的特征。该应用程序是在一个配套文件中开发的。
2018-09-10 cs.LO math.LO
Quantifier Elimination Meets Treewidth
KLSS, Institute of Software Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；University of Oxford（牛津大学）；National Key Laboratory of Space Integrated Information System, Institute of Software Chinese Academy of Sciences（空间信息集成系统国家重点实验室，中国科学院软件研究所）；School of Mathematical Sciences, Peking University（北京大学数学科学学院）；School of Computer Science, Peking University（北京大学计算机学院）；Zhongguancun Laboratory（中关村实验室）
本文提出利用树宽参数的动态规划框架，通过量化消除过程中的结构稀疏性，将FME和CAD的复杂度从双指数降低到单指数。
2026-11-04 cs.CC cs.LO cs.SC
Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases
Millennium Institute for Foundational Research on Data（千禧数据基础研究所）
来自可能不一致的数据库的查询的一致答案是从数据库的每个可能的修复中同时检索的答案。修复是与原始不一致实例差异最小的一致实例。以前已经表明，数据库修复可以被指定为一个析取逻辑程序的稳定模型。在本文中，我们展示了如何使用修复程序转换问题的一致性查询回答问题的推理w.r.t.用二阶谓词逻辑写成的理论。它还研究了如何一阶理论，而不是通过应用二阶量词消去技术。
2021-10-18 cs.AI cs.DB cs.LO
An efficient quantifier elimination procedure for Presburger arithmetic
本文提出一种可在单指数时间内消去存在量词变量块的Presburger算术量词消去过程，纠正了双重指数时间上界为紧的旧有论断，并据此确定了单元可分解性、良拟序判定及Ramsey量词公式等问题的精确复杂度。
2024-05-02 cs.FL cs.LO math.LO
A case study of the difficulty of quantifier elimination in constraint databases: the alibi query in moving object databases
在约束数据库模型中，空间和时空数据通过实数上的多项式等式和不等式的布尔组合来存储。多项式约束扩充的关系演算是约束数据库的标准一阶查询语言。虽然这种查询语言的表达能力已被广泛研究，查询的有效评估的困难，通常涉及某种形式的量词消去，已收到相当少的关注。现有量词消除软件的效率低下和量词消去的固有困难已被证明是约束数据库系统实际实现的瓶颈。在本文中，我们专注于一个特定的查询，称为\emph{alibi query}，询问是否两个移动的对象，其位置是已知的，在某些时刻的时间，可能会满足，给定一定的速度限制。这个查询可以被看作是一个约束数据库查询，它的求值依赖于消除一个由三个存在量词组成的块。通用消除算法的实现在特定情况下，出于实际目的，在回答不在场证明查询时太慢，并且在参数情况下完全失败。本文的主要贡献是参数不在场证明查询的一个解析解，它可以用来回答这个查询在特定的情况下，在常数时间。我们还给出了一个解析解的不在场证明查询在一个固定的时刻。我们提出的解决方案是基于几何论证，它们说明了这样一个事实，即一些实际问题需要创造性的解决方案，至少在理论上，现有的系统可以提供一个解决方案。
2007-12-12 cs.CC cs.DB cs.LO
Cut-Elimination for the Bimodal Logic GR
Japan Coast Guard Academy（日本海上保安大学校）
本文提出GR双模逻辑的超序列演算，证明了切消定理。
2026-05-15 cs.LO
A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
本文研究循环证明系统中消切性质失效的原因，证明即使将语言限制为一元归纳谓词和一元函数，消切性质在简单循环证明系统中仍不成立，改进了先前需三元谓词的反例。
2025-03-05 cs.LO math.LO
"ReLIC: Reduced Logic Inference for Composition" for Quantifier Elimination based Compositional Reasoning and Verification
本文研究了组合推理与验证中的量词消去问题。对于组合推理，QE提供了我们的方法的基础，作为组合的演算，以获得最强的系统属性在单步的，从给定的组件原子属性和它们的互连关系。我们首先为时间无关属性开发了这个框架，后来将其扩展到时间相关属性组合。此外，这种扩展还要求将给定的性质沿时间移动，以跨越感兴趣的时间范围，对于最强的系统性质，最少的时间范围不超过组件级原子性质的总时间范围。系统的初始条件也是以同样的方式由组件的原子初始条件组成的。它是用来验证所需的系统级属性，以及派生的最强的系统属性，通过归纳。我们的组合方法是统一的，无论组合类型（级联/并行/反馈）的时间相关和时间无关的属性。我们开发了一个新的原型验证器ReLIC（Reduced Logic Inference for Composition），实现了上述方法。我们通过几个说明性和实际的例子来证明它。此外，我们先进的$k$归纳为基础的模型检查与QE的能力，制定其基础和归纳步骤到QE的问题，所有的变量都是普遍量化的。我们的QE求解器Redlog与$k$ -归纳为基础的模型检查工具JKind的集成，显示了成功解决的非线性问题，SMT功能的JKind未能解决。最后，我们还展示了最近在工业V\&V工具套件中采用我们的方法，用于Simulink模型和深度神经网络（DNN）的增强静态分析。
2021-02-28 cs.LO
Quantifier Elimination and Craig Interpolation, Quantitatively
Cornell University（康奈尔大学）；RWTH Aachen University（亚琛工业大学）
本文提出首个针对定量分段线性量的QE算法，并展示了其在概率程序验证中的应用，包括定量CI定理和期望结果计算。
2026-11-10 cs.LO cs.PL
Computing Witnesses Using the SCAN Algorithm
Institute for Discrete Mathematics and Geometry, TU Wien（TU维也纳离散数学与几何研究所）；Department of Computer Science, University of Manchester（曼彻斯特大学计算机科学系）
本文提出扩展SCAN算法以解决更一般的问题，即找到等价于一阶公式的二阶量化符见证者，并提供原型实现。
2026-04-30 cs.LO
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)
克雷格插值已经成为产生候选程序不变量的有效手段。我们提出的Presburger算法的理论结合（i）未解释的谓词（QPA+UP），（ii）未解释的功能（QPA+UF）和（iii）扩展数组（QPA+AR）的插值程序。我们证明，这些组合可以有效地内插不使用量词，即使输入公式是量词自由。我们继续识别QPA+UP和QPA+UF的片段，这些片段具有在插值下封闭的保护量化的限制形式。这些片段中的公式可以很容易地映射到带有整数除法的无量词表达式。对于QPA+AR，我们制定了一个健全的插值程序，可能会产生不受限制的量词插值。
2010-11-03 cs.LO
Spatial logics with connectedness predicates
我们考虑量化器自由空间逻辑，设计用于定性空间表示和推理在AI中，并扩展它们的手段来表示区域的拓扑连通性和限制其连接组件的数量。我们调查这些逻辑的计算复杂性，并表明，连接性约束可以增加复杂性从NP到PSpace，ExpTime，如果组件计数是允许的，NExpTime。
2010-10-18 cs.LO
Computing Witnesses Using the SCAN Algorithm (Extended Preprint)
本文扩展了基于饱和定理证明的SCAN算法，使其不仅能进行二阶量词消去，还能寻找产生逻辑等价一阶公式的二阶量词实例，并提供了原型实现，为模态对应理论、知识表示和验证等领域的应用奠定基础。
2025-05-30 cs.LO
Using Quantifier Elimination to Enhance the Safety Assurance of Deep Neural Networks
Honeywell Aerospace（霍尼韦尔航空航天）
机器学习和深度神经网络（DNN）领域的进步使得复杂和自主系统的快速发展成为可能。然而，严格确保此类系统安全运行的固有复杂性阻碍了其在航空航天和医疗设备等安全关键领域的实际应用。因此，人们对探索使用高级数学技术（如形式方法）来解决这一挑战的兴趣激增。事实上，这些努力的初步结果是有希望的。沿着这些路线，我们建议使用量词消去（QE）-一种形式化的方法技术，作为一种补充技术的国家的最先进的静态分析和验证程序。使用机载防撞DNN作为案例，我们说明了使用QE制定通过网络的精确距离前向传播，以及分析其鲁棒性。我们讨论了这项正在进行的工作的初步结果，并探讨了未来扩展这种方法和/或将其与其他方法集成以执行DNN高级安全保证的可能性。
2019-09-18 cs.AI cs.LG cs.LO
Better Answers to Real Questions
我们考虑的是存在主义问题而不是现实。扩展的量词消去通过提供额外的答案来推广常规量词消去的概念，这些答案是对量化变量的可能赋值的描述。通过虚拟替换实现的扩展量词消去已成功地应用于科学和工程中的各种问题。到目前为止，这些实现产生的答案包括无穷小和无穷大的数字，这在实践中很难解释。我们在这里介绍了一个后处理过程，将固定参数的所有答案转换为标准实数。我们的程序的相关性证明了我们的实施从文献中，在那里它显着提高了结果的质量的各种例子的应用。
2015-01-21 cs.LO cs.SC
