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
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
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
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
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
Extending a system in the calculus of structures with a self-dual quantifier
我们回顾SBV，一个证明系统下开发的深推理的方法，扩展乘法线性逻辑与自对偶非交换逻辑算子Seq。我们引入SBVQ，通过添加自对偶量词Sdq来扩展SBV。系统SBVQ是相容的，因为我们证明了割消（的类似）对它成立，它的新逻辑算子Sdq在操作上表现为一个binder，在某种程度上，Seq，和Sdq之间的相互作用可以模拟SBVQ的无割子系统BVQ内部线性λ-演算的β-约化。长期目标是继续开发一个程序，其目标是通过SBV的最小和增量扩展，在证明搜索作为计算类比下给出计算原语的纯逻辑帐户。
2012-12-18 cs.LO
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
2000-06-05 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
Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall
Charles University（查理大学）；Institute of Computer Science, Academy of Sciences of the Czech Republic（捷克科学院计算机科学研究所）
本文提出一种结合区间技术与保守线性规划近似的算法，高效求解存在-全称量化前缀的量化约束问题，支持更通用的布尔结构并提升求解效率。
2014-06-24 cs.DS cs.LO cs.NA
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
我们提出了一个组合SMT为基础的算法的安全程序，考虑到堆以及。现有的基于SMT的方法要么在很大程度上限于处理线性算术运算和属性，或者是非组合的。我们使用约束角子句（CHCs）来表示验证条件，其中使用阵列的扩展理论（ARR）的内存操作建模。首先，我们描述了一个指数时间量词消去（QE）算法的ARR，它可以引入新的量词的索引和值排序。其次，我们适应QE算法，以有效地获得下近似使用模型，从而在多项式时间基于模型的投影（MBP）算法。第三，我们集成的MBP算法的框架中的组合推理的过程性程序使用的可能和必须的摘要，我们最近提出的。我们对CHC的解决方案目前仅限于无量词公式。最后，我们描述了我们的实践经验，在SV-COMP'15基准测试中使用的工具SPACER的实现。
2015-08-06 cs.LO cs.PL cs.SE
