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
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
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
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
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
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
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
"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
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
自动结构是由同步有限状态自动机表示的无限结构。本文关注有限词和树（排名/排名）的自动结构。我们调查的“有向版本”的拉姆齐量词，它表示存在一个无限的有向集团。这包含了拉姆齐量词的标准“无向版本”。首先观察到Ramsey量词与验证中的两个问题之间的有趣联系：（1）规则模型检验中Büchi和广义Büchi条件的可达性可以看作是传递自动图上的Ramsey量化（即，其边关系是传递的），（2）检查一元可分解性（a.k.a.可识别性）可以被看作是在共传递自动图上的Ramsey量化（即，其边关系是传递的补集）。我们提供了一个全面的复杂性景观拉姆齐量词在这三种情况下（一般，传递，共传递），所有NL和EXP之间。反过来，这产生了大量具有精确复杂性的新结果，例如，子树/扁平前缀重写的验证，以及树自动关系上的一元分解。我们还获得了相当简单的证明，例如，对于词自动关系上的一元可分解性的NL复杂度（由DFA给出）。
2023-02-13 cs.LO
On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
针对含任意量词交替的超属性验证难题，提出利用部分信息下的层级多人博弈方法，证明其可判定性，拓展了博弈法的适用范围。
2025-10-04 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
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
Symbol Elimination for Parametric Second-Order Entailment Problems (with Applications to Problems in Wireless Network Theory)
我们分析了含有参数-常数或函数的公式的二阶量词消去的可能性。为此，我们使用的约束解析演算从专门的层次叠加演算。如果饱和终止，我们分析的可能性，获得最弱的参数，保证满足性的约束。如果饱和不终止，我们确定的情况下，存在无限饱和集的有限表示。我们确定的情况下，使用二阶量化表示的公式之间的蕴涵可以有效地检查。我们说明了一系列的例子，从无线网络研究的想法。
2021-07-06 cs.LO
Statistical Verification of Quantitative Hyperproperties: Beyond Boolean Quantification
Chalmers University of Technology（查尔姆斯理工大学）；University of Gothenburg（哥德堡大学）
本文针对现有超性质形式体系无法处理系统定量特性的问题，提出定量超逻辑（QHL），开发其统计验证算法，结合统计方法为嵌套测度量词提供验证方案，在定量IFC基准上验证了方法的表达性与有效性。
2026-08-05 cs.LO
Generation Of A Complete Set Of Properties
形式化验证存在的问题之一是由于规格说明的不完备性而导致功能上不完备。一个满足不完整规范的实现可能仍然有很多bug。在测试中，通过将功能完整性替换为$\mathit{structural}$来解决此问题。后者是通过生成一组测试来探测设计实现的每一部分来实现的。我们表明，类似的方法可以用于形式化验证。这里的想法是生成一个在规范中没有暗示的实现的属性。找到这样的属性意味着规范是不完整的。如果这是一个$\mathit{unwanted}$属性，则该实现存在错误。否则，需要添加新的规范属性。生成与设计的不同部分相关的实现属性，然后添加新的规范属性，生成$\mathit{structurally}$ - $\mathit{complete\:specification}$。实现属性是由$\mathit{partial\: quantifier\:elimination}$构建的，这是一种仅将公式的一部分从限定符的范围中取出的技术。通过将部分量词消去应用于定义实现的“真值表“的公式来生成实现属性。我们展示了我们的方法是如何工作的组合和时序电路的规格。
2020-10-12 cs.LO
A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning
EPFL（洛桑联邦理工学院）；Microsoft Research（微软研究院）
本文指出SMT求解器中量词实例化的深度记账非合流导致结果不稳定，提出一种稳定的新记账方法，在Z3中实现，使Mariposa基准不稳定核心的结果不稳定性降低94%且无性能回退。
2026-11-06 cs.LO
Reducing the Complexity of Quantified Formulas via Variable Elimination
我们提出了一个通用的简化量化SMT公式使用变量消除。这种简化是基于对函数应用中作为参数出现的地面项的分析。我们使用这些信息来生成一组约束系统，然后求解该系统以计算每个变量的一组足够的基础项。普遍量化的变量与一组有限的足够的地面条款可以消除实例化他们与计算的地面条款。由此产生的SMT公式可能包含更少的量词，因此可能更容易求解。我们描述了一个令人满意的模型的结果公式可以被修改，以满足原始公式。我们的实验表明，在许多情况下，这种简化大大提高了求解时间，我们使用Z3和CVC 4的评估表明，这个想法并不特定于特定的求解器，但可以普遍应用。
2014-08-04 cs.LO
Tunable Automation in Automated Program Verification
New York University（纽约大学）；Microsoft Research（微软研究院）；MPI-SWS（德国马克斯·普朗克软件系统研究所）
本文提出了一种在自动程序验证中调节自动化的机制，通过细粒度控制量词事实的可用性，使开发者能够根据需求选择不同的自动化级别。
2025-12-03 cs.LO cs.PL cs.SE
Prophecy Variables for Hyperproperty Verification
像HyperLTL这样的超属性的时态逻辑使用跟踪量词来表达与多个系统运行相关的属性。在实践中，这种规范的验证大多限于没有量词交替的公式，其中验证可以减少到检查系统的自组成上的跟踪属性。像$\forall π. \exists π'. ϕ$这样的量词替换可以通过互补来解决，也可以解释为$\forall$ -玩家和$\exists$-玩家之间的双人游戏，$\forall$ -玩家递增地构建轨迹$π$，$\exists$ -玩家以这样的方式构建$π'$，即$π$和$π'$一起满足$ϕ$。基于游戏的方法明显便宜但不完整，因为$\exists$玩家不知道$\forall$玩家的未来移动。在本文中，我们建立了游戏为基础的方法，可以通过添加（$ω$定期）时间预言完成。我们的证明是建设性的，产生一个有效的算法生成一套完整的预言。
2022-06-03 cs.CR cs.LO
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
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
2016-05-06 cs.LO cs.PL
