Termination of Rewriting with Right-Flat Rules Modulo Permutative Theories
我们提出了可判定性的结果终止类的长期重写系统模置换理论。终端和最里面的终止模置换理论被证明是可判定的长期重写系统（TRS），其右手边的条款被限制为浅（变量发生在深度最多一个）和线性（每个变量发生在最多一次）。最内层终止模置换理论也被证明是可判定的浅TRS。我们首先表明，一个浅TRS可以转化为一个平面（只有变量和常数发生在深度1）TRS，同时保持终止和最内层终止。然后证明了可判定性的结果表明：（a）右平坦右线性（平坦）TRS，非终止（分别，最内非终止）意味着从平坦项开始的非终止，和（b）右平坦TRS，从给定项开始的非终止导子的存在是可判定的。在消极的一面，我们显示PSPACE-硬的终止和最内终止浅右线性TRS，和undecidability终止平坦的TRS。
2010-08-25 cs.LO
Separation Logic Modulo Theories
关于程序数据的逻辑推理通常需要处理堆结构以及标量数据类型。可满足性模块化理论（SMT）的最新进展已经提供了处理标量的有效程序，但它们缺乏对处理堆结构的任何支持。在本文中，我们提出了一种方法，集成了分离逻辑-一个突出的逻辑推理表段的堆-和SMT。我们遵循基于模型的方法，在SMT求解器和分离逻辑推理部分之间的堆单元之间传递别名。使用Z3求解器的实验评估表明，我们的方法可以有效地把工作的SMT处理堆结构的进步。这是分离逻辑与SMT理论相结合的第一个决策过程。
2013-03-11 cs.LO
Temporal Stream Logic modulo Theories (Full Version)
时态流逻辑（TSL）在任意函数项上通过更新和谓词扩展LTL。这允许指定LTL表达能力不足的数据密集型系统。在TSL的语义中，函数和谓词是不解释的。在本文中，我们扩展TSL与一阶理论，使我们能够指定系统使用解释功能和谓词，如增量或相等。我们调查的可满足性问题TSL模的标准基础理论的未解释的功能，以及相对于Presburger算法和理论的平等：对于所有这三个理论，TSL可满足性是高度不可判定的。然而，我们确定了三个片段的TSL的可满足性问题是（半）不可判定的理论解释的功能。尽管高的不可判定性，我们提出了一种算法-这是不保证终止-用于检查可满足性的TSL公式在理论的未解释的功能和评估：它的规模以及能够验证假设在现实世界中的系统设计。
2022-01-25 cs.LO
Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
针对OMT中完全真值指派枚举易过度限制搜索空间的问题，提出利用部分指派枚举的指派约简技术，在OptiMathSAT中实现并经基准测试验证，可提升最优求解效率与随时求解的解质量。
2025-05-18 cs.LO
Tableaux Modulo Theories Using Superdeduction
我们提出了一种方法，使我们能够开发tableaux模理论使用的原则superdeduction，其中理论是用来丰富的演绎系统与新的演绎规则。该方法是在Zenon自动定理证明器的框架中提出的，并应用于B方法的集合论。这使得我们可以为Atelier B提供另一个证明器，它可以用来验证B的证明规则。我们还提出了一些基准测试，在这个证明是能够自动验证的一部分规则来自西门子IC-MOL维护的数据库。最后，我们描述了另一个扩展的Zenon与superdeduction，这是能够处理任何一阶理论，并提供了一个基准来自TPTP库，其中包含了大量的一阶问题。
2015-01-06 cs.LO
A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
本研究提出将线性时序逻辑模理论LTL-MT规约为符号数据字自动机SDWAs的新方法，可转化为约束霍恩子句求解，适用于模型检测等场景，实验表现不逊于现有定制方案。
2024-08-16 cs.LO
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
针对SMT重要子集SMMT缺乏高效不可满足性证明生成方法的问题，提出基于理论谓词命题定义生成紧致Horn近似以得到DRAT证明的方法，开销低且可处理此前难处理的问题。
2024-04-18 cs.LO
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
循环数据结构，如循环列表，在函数式编程中由于其循环性而难以处理。本文研究了循环数据集的范畴、代数和计算基础。我们的循环数据库框架是基于Fiore等人的二阶代数理论，其给出了用于描述和推理循环数据集的语法、类型和计算规则的统一设置。我们从Bloom和Esik的迭代范畴的范畴语义中提取“折叠”计算规则。因此，规则通过构造是正确的。我们证明了强规范化使用一般模式标准的二阶计算规则。而不是不动点定律，我们特别选择Bekic定律进行计算，这是获得强归一化的关键。我们还证明了计算规则的“Church-Rosser模互模拟”性质。综合这些结果，我们得到了循环资料方程理论与褶曲的显著判别结果。
2017-11-14 cs.LO
On Optimization Modulo Theories, MaxSMT and Sorting Networks
优化模理论（OMT）是SMT的扩展，它允许找到优化给定目标的模型。（部分加权）MaxSMT -或等效的OMT与伪布尔目标函数，OMT+PB-是OMT的一个非常相关的严格子情况。我们将现有的MaxSMT或OMT+PB方法分为两组：基于MaxSAT的方法利用了最先进的MAXSAT求解器的效率，但它们是专用的，并不总是适用的;基于OMT的方法是通用的，但它们在MaxSMT/OMT+PB问题上存在固有的效率低下。我们确定了这种低效率的一个主要来源，我们解决它通过增强OMT的双向排序网络。我们在OptiMathSAT OMT求解器上实现了这个想法。我们对各种问题进行了广泛的实证评估，比较了基于MaxSAT和基于OMT的技术，使用和不使用排序网络，在OptiMathSAT和νZ上实现。结果支持这一想法的有效性，并提供了有关不同方法的有趣见解。
2017-02-08 cs.LO
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
我们报告的工作进展自动程序证明性能的程序写在高阶函数语言。我们的方法编码高阶程序直接作为一阶SMT问题的霍恩条款。将一阶程序的Hoare式验证简化为Horn子句的可满足性是很直接的。闭包的存在带来了一些挑战：相对完整的证明系统必须考虑闭包;在实践中，搜索过程的有效性取决于编码策略和底层求解器的能力。我们在这里使用代数数据类型来编码闭包，并依赖于支持代数数据类型的求解器。该方法的可行性进行检查使用的例子从文献中高阶程序验证。
2013-06-21 cs.LO
Local Search For Satisfiability Modulo Integer Arithmetic Theories
开发了首个直接操作变量的SMT(IA)局部搜索算法LS-IA，设计针对整数算术的操作符、评分函数和两级选择启发式，实验证明其与Z3组合提升了SMT-LIB可满足基准集上的现有水平。
2023-05-17 cs.LO
Generalized Optimization Modulo Theories
本文提出广义优化模理论（OMT），引入基于偏序集目标函数的抽象演算，统一单/多目标优化并支持与理论无关的求解，为OMT方法建立理论基础。
2024-04-29 cs.LO
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
在过去的十年中，我们已经目睹了一个令人印象深刻的进步，表现力和效率的可满足性模理论（SMT）解决技术。这给最先进的SMT求解器带来了以前难以解决的问题，特别是在软件和硬件验证领域。然而，许多感兴趣的SMT编码问题，也需要找到最佳wrt模型的能力。一些成本函数。在以前的工作中，即“优化模理论与线性有理成本函数- OMT（LAR UT）”，我们利用SMT解决处理成本函数的线性算术的最小化的理由，通过SMT和LP最小化技术的组合。在本文中，我们沿着三个方向推进了OMT方法：首先，我们通过SMT、LP和ILP最小化技术的组合，将其扩展到混合整数/有理数域上的线性运算;其次，我们开发了一个多目标版本的OMT，以便同时处理多个成本函数;第三，我们开发了一个OMT的增量版本，以便利用一些OMT可编码问题的增量性。OMT编码的验证问题上进行的实证评估表明，这些扩展的有用性和效率。
2015-01-16 cs.LO
Axiomatic constraint systems for proof search modulo theories
一阶逻辑中的目标导向证明搜索使用元变量来延迟证人的选择;当关闭证明树分支时，使用一阶统一或特定于理论的背景推理器来产生这些变量的替换。本文探讨了这样的机制，从而产生理论特定的约束，而不是替代的概括。为了设计模块化的证明搜索过程中，这样的机制，我们提供了一个元变量，抽象地操纵这样的约束条件的微积分。证明微积分的可靠性和完备性导致了一个公理化，它确定了抽象约束可以以与统一器通常相同的方式生成和传播的条件。然后，我们提取我们的抽象框架的组件接口和规范的具体实现的背景推理。
2015-09-03 cs.LO
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers
优化模理论（OMT）是SMT的一个重要扩展，它允许找到优化给定目标函数的模型，通常包括线性算术或伪布尔项。然而，许多SMT和OMT应用，特别是来自SW和HW验证的应用，需要处理数字的位精确表示，这在SMT中分别借助于用于整数的位向量（BV）理论和用于实数的浮点数（FP）理论来处理。尽管Nadel和Ryvchin已经提出了一种用于OMT（无符号）BV的方法，但不幸的是，我们不知道任何现有的用于OMT FP的方法。在本文中，我们填补了这一空白。我们提出了一种新的OMT方法，基于吸引子和动态吸引子的新概念，将Nadel和Ryvchin的工作扩展到签名BV，最重要的是，FP。我们已经实现了一些OMT（BV）和OMT（FP）的OptiMathSAT程序，并测试了后者从SMT-LIB库修改后的问题。实证结果支持了新方法的有效性和可行性。
2019-05-07 cs.LO
From MiniZinc to Optimization Modulo Theories, and Back (Extended Version)
优化模理论（Optimization Modulo Theories，OMT）是SMT的一个扩展，它允许找到优化目标函数的模型。在本文中，我们的目标是弥合之间的差距约束编程（CP）和OMT，在两个方向。首先，我们用FlatZinc接口扩展了OMT求解器OptiMathSAT，它也可以用作其他OMT求解器的FlatZinc到OMT编码器。这使得OMT工具可以与mzn 2fzn结合使用，解决来自MiniZinc社区的大量CP问题。其次，我们介绍了一个工具，用于将线性算术和位向量理论上的SMT和OMT问题转换为MiniZinc。这使得MiniZinc求解器可以用于大量的SMT/OMT问题。我们已经讨论了我们必须在两个方向上处理的主要问题。我们已经进行了广泛的实证评估，比较了三种最先进的基于OMT的工具与许多最先进的CP工具（i）来自MiniZinc挑战的CP问题，以及（ii）主要来自形式化验证的OMT问题。这种分析还使我们能够确定一些关键，在效率和正确性方面，一个人必须应付时，解决CP问题与OMT工具，反之亦然。
2020-02-17 cs.LO
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
AC-完成有效地处理等式模关联和交换函数符号。当输入接地时，程序终止并提供单词问题的判定算法。本文给出了基AC-完备化的一个模扩展，用于将等式理论与用户定义的AC符号、未解释符号和任意签名不相交的Shostak理论X相结合来判定公式.我们的算法，称为AC（X），是通过在一个模块化的方式增加地面AC完成与规范和求解器目前的理论X。这种整合依赖于规范化重写，这是一种新的关系，让人想起规范化重写，在重写步骤中整合规范。AC（X）被证明是可靠的，完整的和终止的，并实现扩展Alt-Ergo定理证明器的核心。
2012-09-13 cs.LO
Complete Trigger Selection in Satisfiability modulo first-order Theories
本文证明在SMT求解器中，当触发器函数与文字选择函数一致时，量词实例化对饱和子句集是完备的，并给出停机条件及Horn或2SAT情形的多项式时间求解。
2023-06-21 cs.LO
Reactive Synthesis Modulo Theories Using Abstraction Refinement
反应式合成从作为时序逻辑公式给出的规范构建系统。传统上，无功综合定义为具有布尔输入和输出变量的系统。最近，新的理论和技术已经被提出来扩展反应合成的数据域，这是需要更复杂的程序。特别是，时间流逻辑（TSL）（Finkbeiner et al. 2019）通过状态变量、更新和未解释的函数扩展了LTL，并被创建用于合成。本文给出了TSL（T）的一个综合方法，它是TSL的理论推广。使用反例引导合成循环和LTL合成程序进行合成。我们的方法翻译TSL（T）规格LTL和提取系统，如果合成成功。另外，分析了与理论不一致的对策。如果反策略是理论一致的，则证明该规范是不可实现的。否则，我们将时间假设和布尔谓词添加到TSL（T）规范中，并开始循环的下一次迭代。我们证明了TSL（T）的综合问题是不可判定的。然而，我们的方法可以成功地合成或显示几个非布尔的例子的不可实现性。
2021-07-30 cs.LO
Computing Tropical Prevarieties with Satisfiability Modulo Theories (SMT) Solvers
一种新的方法，使用SMT（可满足性模理论）求解器来计算热带前变（分别）。平衡）的多项式系统。新的方法是基准对一个天真的方法，使用纯粹的多面体的方法。事实证明，SMT方法比多面体方法更快，否则需要一分钟以上的计算时间，在许多情况下是60倍或更多，在最坏的情况下只是慢了两倍。此外，新的方法是一个随时算法，从而提供了一种方法来计算部分的解决方案时，多面体的方法是不可行的。
2020-06-26 cs.CG cs.LO
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
Free University of Bozen-Bolzano（博尔扎诺自由大学）
本文研究有限迹上的线性时态逻辑（LTLf），其中命题字母被替换为任意理论上的一阶公式，其思想是可满足性模理论。由此产生的逻辑，称为LTLf模理论（LTLfMT），是半可判定的。尽管如此，它的高表现力在许多用例中非常有用，例如数据感知流程的模型检查和数据感知规划。尽管这些问题通常是不可判定的，但能够解决可满足的实例是一个值得研究的折衷方案。在激励和描述这样的用例之后，我们提供了一个基于单通道树形tableau系统的SMT编码的LTLfMT的健全和完整的半决策过程。该算法在BLACK可满足性检查工具中实现，并在新的基准测试上进行了实验评估，结果表明了该方法的可行性。
2022-05-24 cs.AI cs.LO
Optimization Modulo Theories with Linear Rational Costs
在自动推理（AR）和形式化验证（FV）的背景下，重要的决策问题被有效地编码到可满足性模理论（SMT）。在过去的十年中，已经为几种实际感兴趣的理论开发了有效的SMT求解器（例如，线性算术、数组、位向量）。令人惊讶的是，几乎没有工作已经做了扩展SMT处理优化问题，特别是，我们不知道任何以前的工作SMT求解器能够产生的解决方案，最大限度地减少成本函数的算术变量。这是不幸的，因为一些感兴趣的问题需要这个功能。在本文所描述的工作中，我们开始填补这一空白。我们提出并讨论了两个一般程序，利用SMT处理线性有理成本函数的最小化，SMT与标准的最小化技术相结合。我们已经在MathSAT SMT求解器中实现了这些程序。由于在AR，FV和SMT领域的竞争对手的情况下，我们已经通过实验评估了我们的实现对国家的最先进的工具，线性广义析取编程（LGDP），这是最接近的精神，我们的域，在一组问题，以前已经提出了后者的工具作为基准。结果表明，我们的工具是非常有竞争力的，往往优于这些工具对这些问题，清楚地表明了该方法的潜力。
2014-10-22 cs.LO
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
我们介绍了一种方法，旨在结合使用的可满足性模理论（SMT）求解器的组合逻辑合成器（CL）的框架。(CL)S是一种用于从用户指定的存储库自动组合软件组件的工具。该框架产生一个树语法，其中包含符合目标类型的所有组合术语。（CL）S的类型规范基于具有交集类型的组合逻辑。我们的方法将树语法转换为SMT功能，这允许考虑额外的特定于域的约束。我们证明了我们的方法在几个实验中的实用性。
2019-08-26 cs.FL cs.LO
Satisfiability.jl: Satisfiability Modulo Theories in Julia
本文介绍 Julia 开源包 Satisfiability.jl，通过高级接口连接兼容 SMT-LIB 的求解器，以便更便捷地编写复杂 SMT 公式并支持形式化验证。
2023-12-16 cs.LO cs.MS
Grammatical Inference as a Satisfiability Modulo Theories Problem
Institute for Computing；Information Sciences Radboud University Nijmegen, The Netherlands Email
从可满足性模理论的角度研究了从一组标记符号序列中学习最小一致模型的问题。我们提出了两种编码确定性有限自动机和扩展这些Moore和Mealy机之一。我们的实验结果表明，这些编码提高了国家的最先进的，是有用的，在实践中学习小模型。
2017-05-30 cs.FL cs.LG cs.LO
Instantiation of SMT problems modulo Integers
SMT问题的许多决策过程或多或少地隐含地依赖于所考虑的理论的公理的实例化，并且通过利用每个理论的附加属性而有所不同，以提高效率。我们提出了一种新的技术，设计完整的实例化计划的SMT问题的线性算术与另一个理论T。该方法首先对公式的算术部分进行实例化，然后通过使用对T是完备的实例化策略来去除问题中的剩余变量。我们提供的例子证明，这种技术不仅是通用的（在这个意义上说，它适用于广泛的理论），但它也是有效的，即使是最先进的实例化计划的具体理论相比。
2010-06-15 cs.LO
Satisfiability Modulo Theories for Verifying MILP Certificates
针对MILP求解器结果正确性问题，提出基于SMT-LIB的VIPR证书验证方法，通过编码推理规则并使用Why3框架形式化验证，实现了求解器无关的证书检查。
2025-10-12 cs.LO
What is a Theory ?
本文提出极化演绎模，通过限制规则在正负出现处的使用扩展演绎模，并证明命题演算中所有理论均可表达且切割可消除。
2023-05-25 cs.LO
Probabilistic Inference Modulo Theories
SRI International（SRI国际研究所）；U. of Texas at Dallas（德克萨斯大学达拉斯分校）；U. of California, Irvine（加州大学欧文分校）
我们提出了SGDPLL（T），一个算法，解决了（在许多其他问题中）概率推理模理论，即通过提供作为参数的逻辑理论定义的概率模型上的推理问题（目前，命题，离散排序上的等式，以及不等式，更具体地说，有界整数上的差分运算）。虽然已经提出了对逻辑表示的概率推理的许多解决方案，但SGDPLL（T）同时（1）提升，（2）精确和（3）模理论，即，由背景逻辑理论参数化。这为将其扩展到丰富的逻辑语言（如数据结构和关系数据）提供了基础。所谓提升，我们指的是在域大小（变量可以取值的数量）上具有恒定复杂度的算法。我们还详细介绍了一个求解器的求和差分算法，并显示实验结果的情况下，SGDPLL（T）是比一个国家的最先进的概率求解器快得多。
2016-05-27 cs.AI cs.LO
Representing Hybrid Automata by Action Language Modulo Theories
Arizona State University（亚利桑那州立大学）；Houzz Inc.（Houzz 公司）
混合自动机和动作语言都是描述动态系统演化的形式化方法。本文建立了它们之间的正式关系。我们展示了如何简洁地表示混合自动机的动作语言，这反过来又被定义为一个高层次的符号的答案集编程模理论（ASPMT）-一个扩展的答案集程序的一阶水平类似的方式可满足性模理论（SMT）扩展命题可满足性（SAT）。首先，我们展示了如何表示线性混合自动机的凸不变量的行为语言模理论。进一步翻译成SMT允许使用支持实数运算的SMT求解器来计算它们。接下来，我们将表示扩展到一般类的非线性混合自动机，甚至允许非凸不变量。我们表示它们的动作语言模ODE（常微分方程），它可以被编译成可满足模ODE。我们开发了一个原型系统cplus 2aspmt的基础上，这些翻译，它允许一个简洁的表示的混合过渡系统，可以有效地计算的最先进的SMT求解器dReal。
2017-07-25 cs.AI cs.FL cs.LO
Boolean Abstractions for Realizability Modulo Theories (Extended version)
本文提出将含算术等理论的规范通过文字替换与额外布尔依赖需求转换为纯布尔规范，并结合 SAT/SMT 求解实现非布尔 LTL 可实现性判定，在 Z3-Python 中实现并完成工业案例评估。
2023-10-26 cs.LO
Advances in Symmetry Breaking for SAT Modulo Theories
对称破缺是一种常用的技术，它利用公式中变量和子句的对称性来减少SAT求解的搜索空间。其关键思想是首先确定属于同一对称类的赋值集，然后施加排序约束，称为对称性破坏谓词（SBP），使得这些赋值中只有一个（或一个小子集）被允许是原始SAT公式的解。虽然这项技术已被广泛利用在SAT文献，有很少的工作使用对称性破缺SAT模理论（SMT）。在SMT中，SAT理论中的逻辑约束与定义在非布尔变量（如整数、实数等）上的另一组理论运算相结合。SMT求解器通常使用SAT求解技术的组合，并通过调用理论求解器来增强。在这项工作中，我们采取了SAT对称性破缺的进展，并将其应用到域的SMT。我们的关键技术贡献是制定对称性破缺的布尔骨架变量，这是占位符的实际理论操作SMT解决。然后，这些SBP应用于SMT求解器的SAT求解部分。我们在最先进的SMT求解器CVC 4之上实现SBP理念。与最先进的方法相比，我们的方法可以在几个基准问题上获得更快的解决方案。我们的最终求解器是原始CVC 4求解器和基于SBP的求解器的混合体，与该类别中表现最好的CVC 4相比，在2018年和2019年SMT基准的QF_NIA类别中，分别可以解决高达3.8%和3.1%的问题。
2020-01-16 cs.LO
Design Space Exploration via Answer Set Programming Modulo Theories
Institute of Computer Science（计算机科学研究所）
广泛应用于移动设备和汽车的嵌入式系统的设计正变得越来越复杂，因此有效的系统级设计方法变得至关重要。我的研究旨在开发系统，帮助设计师以声明的方式表达复杂的设计问题，并探索设计空间，以获得具有理想属性的解决方案。为此，我们利用ASP的知识表示和推理能力，结合背景理论。因此，第一次，我们提出了一个复杂的方法，允许直接集成到ASP的非线性目标的多目标优化。这包括独特的结果，不同的子问题涵盖在几个出版物，我将在这项工作中提出。
2019-05-07 cs.AI cs.LO
Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata (Extended Version)
本文首次研究带理论数据感知进程（DMTs）的线性时间验证，消除了现有方法对特定数据类型和安全性验证的限制，提出结合自动机理论和覆盖计算技术的半判定过程，并给出保证有限状态抽象的语义条件及实验评估。
2023-10-17 cs.LO
Threat Repair with Optimization Modulo Theories
我们提出了一个基于模型的程序，使用正式的模型自动防止安全威胁。我们将系统模型和潜在威胁编码为可满足性模理论（SMT）公式。该模型允许我们将安全问题作为可满足性查询。我们制定威胁预防作为一个优化问题，在相同的公式。我们的威胁预防过程的结果是一个建议的模型属性修复，消除威胁。每当威胁预防失败时，我们就会自动解释威胁发生的原因。我们使用最先进的Z3 SMT求解器实现我们的方法，并将其与威胁分析工具THREATGET相结合。我们证明了我们的程序的价值，在两个案例研究，从汽车和灵巧家庭领域，包括一个工业强度的例子。
2022-10-06 cs.CR cs.FL cs.LO
ASPMT(QS): Non-Monotonic Spatial Reasoning with Answer Set Programming Modulo Theories
University of Warsaw（华沙大学）；University of Bremen（不来梅大学）
\emph{dynamic spatial systems} [9]的系统建模是广泛应用领域的关键要求，例如常识认知机器人、计算机辅助建筑设计、动态地理信息系统。我们提出了ASPMT（QS），一种新的方法和完全实现的原型非单调空间推理--动态空间系统内的一个关键要求-基于答案集编程模理论（ASPMT）。ASPMT（QS）包括一个（定性）空间表示模块（QS）和一种方法，用于将紧密的ASPMT实例转换为SAT模理论（SMT）实例，以便通过SMT求解器计算稳定的模型。我们正式和实施的默认空间推理和空间框架公理的概念，使用选择公式。空间推理是通过将空间关系编码为多项式约束系统，并利用实非线性算法理论通过SMT求解来实现的。我们经验评估ASPMT（QS）与其他著名的当代空间推理系统相比。我们的研究结果表明，ASPMT（QS）是唯一现有的系统，能够推理的间接空间效应（即解决分歧的问题），并整合几何和定性空间信息的非单调空间推理上下文。
2015-06-16 cs.AI cs.LO
Dedukti: a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory
本文介绍逻辑框架Dedukti，它基于模理论的$\lambda$$\Pi$-演算，能表达多种逻辑理论并检查其他证明系统（如Zenon、HOL Light等）的大型证明库。
2023-11-13 cs.LO
ILP Modulo Data
每天生成和捕获的大量数据导致迫切需要工具和流程来组织，分析和关联这些数据。具有数据固有支持的自动推理和优化工具可以在各种背景下实现进步，从数据支持的决策到数据密集型科学研究。为此，我们引入了一个可判定的逻辑，旨在数据库分析。我们的逻辑使用关系代数中的运算符（例如选择和叉积）扩展了无量化符的线性整数算术。我们提供了一个可扩展的决策过程，它是基于ILP模理论的BC（T）架构。我们的决策程序利用数据库技术。我们还实验评估我们的方法，并讨论潜在的应用。
2014-09-15 cs.LO
Decidable Fragments of LTLf Modulo Theories (Extended Version)
University of Udine（乌迪内大学）；Free University of Bozen-Bolzano（博尔扎诺自由大学）
本文研究有限迹上的线性时序逻辑模理论（LTLfMT），提出可靠完备的剪枝规则，证明满足“有限记忆”条件的公式其 tableau 可终止，并由此确立多个 LTLfMT 片段可满足性的新可判定性结果。
2023-07-31 cs.AI cs.LO
On completeness of reducibility candidates as a semantics of strong normalization
本文定义了一个健全的和完整的语义标准，基于reductioncandidates，强规范化的理论表示在最小的演绎模LA咖喱。使用咖喱风格的证明条款允许建立这一标准的经典概念前海廷代数，并使该标准涉及所有的理论表示最小的演绎模。与使用Church风格的证明项相比，该方法提供了更简单的准则定义和更简单的完备性证明。
2012-02-15 cs.LO
Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories
我们定义了一类排序树自动机TABG，它推广了Bogaert和Tison（1992）兄弟之间的局部测试树自动机和Filiot等人（2007）的全局等式和不等式约束（TAGED）。TABG可以测试兄弟子项之间以及位置由计算期间达到的状态定义的子项之间的给定平坦方程理论的相等性和不等性。特别地，TABG可以检查到达给定状态的所有子项是否不同。此约束与XML文档的一元键约束有关，这意味着给定类型的每两个不同位置具有不同的值。我们证明了TABG的空性问题的可判定性。这特别解决了TAGED的空性的可判定性的公开问题。我们进一步扩展我们的结果，允许全局算术约束计数的出现次数的一些状态或不同的等价类的子项（模一个给定的平面方程理论）达到一些状态在计算过程中的数量。我们还调整模型，以无序有序的条款。作为我们的结果TABG的后果，我们证明了一元二阶逻辑的一个片段的可判定性扩展与谓词之间的平等和不平等的子树，和基数的树。
2013-04-01 cs.FL cs.LO
IC3 Modulo Theories via Implicit Predicate Abstraction
我们提出了一种新的方法来推广的IC3算法不变检查从有限状态到无限状态的过渡系统，表示在一些背景理论。该过程是基于IC3与隐式（谓词）抽象的紧密集成，隐式（谓词）抽象是一种表示抽象转换而不显式计算抽象系统的技术，并且相对于谓词的增加是增量的。在这种情况下，IC3只在抽象状态空间的布尔级别上操作，发现抽象谓词上的归纳子句。理论推理被限制在底层SMT求解器中，并在执行可满足性检查时透明地应用。当当前的抽象允许一个虚假的反例时，它通过发现和添加足够的新谓词集来改进。重要的是，这可以以完全增量的方式完成，而不会丢弃在前一次搜索中找到的子句。所提出的方法有两个关键优点。首先，与IC 3当前的SMT泛化不同，它允许处理广泛的背景理论，而不依赖于临时扩展，例如量词消去或特定于理论的从句泛化程序，这些程序可能并不总是可用的，而且可能效率低下。其次，与直接探索具体的转换系统相比，使用抽象可以显著提高性能，正如我们的实验所证明的那样。
2013-10-25 cs.LO cs.SE
Shield Synthesis for LTL Modulo Theories
IMDEA Software Institute（IMDEA软件研究所）；Cornell University（康奈尔大学）；University of California, Irvine（加州大学欧文分校）；The Hebrew University of Jerusalem（耶路撒冷希伯来大学）
针对机器学习模型在安全关键系统中存在的不安全行为问题，本研究提出一种基于LTL模理论的屏蔽合成方法，解决现有屏蔽技术仅适用于命题逻辑的局限，实现更丰富逻辑下的安全保障。
2025-02-14 cs.AI cs.LG cs.LO
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Karlsruhe Institute of Technology (KIT)（卡尔斯鲁厄理工学院）
针对多语言系统性质验证难题，本文提出异构动态逻辑(HDL)框架，通过提升与组合操作模块化整合不同程序逻辑，形式化证明推理规则可靠性与相对完备性，并借由汽车控制器案例展示跨语言推理的实用价值。
2026-04-14 cs.LO cs.PL
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
University of California, Berkeley（加利福尼亚大学伯克利分校）
针对现有SMT求解器处理代数数据类型（ADTs）时因惰性方法导致扩展性差的问题，提出一种急切方法，将ADT查询归约为未解释函数（UF）理论，并证明了该方法的可靠性、完备性及优于现有方法的性能。
2023-10-18 cs.AI cs.LO cs.PL
Model Counting Modulo Theories
本文主要研究软件安全性的定量评估问题。更具体地说，它解决了有效计算信道容量的问题，即软件泄露的最大机密信息量，以香农熵或雷尼最小熵测量。大多数计算信道容量的方法要么是有效的，只返回（可能非常宽松）上限，或者效率低下，但精确;很少有目标现实的程序。在这篇论文中，我们提出了一个新的方法来解决这个问题，通过减少它的模型计数问题的一阶逻辑，我们命名为模型计数模理论或#SMT。对于数量安全，我们的贡献是双重的。首先，在理论方面，我们建立了测量机密性泄漏和基本验证算法（如符号执行，SMT求解器和DPLL）之间的联系。其次，利用这些连接，我们开发了新的基于#SMT的技术来计算信道容量，实现了准确性和效率。这些技术可扩展到现实世界的程序，并说明性的案例研究包括C程序从Linux内核，Java程序从欧洲项目和匿名协议。对于形式化验证，我们的贡献也是双重的。首先，我们介绍和研究了一个新的研究问题，即#SMT，它有其他潜在的应用程序以外的计算信道容量，如返回多个反例有界模型检验或自动测试生成。其次，我们提出了一种替代方法，有界模型检验使用经典的符号执行，它可以并行化，以利用现代多核和分布式架构。
2015-04-10 cs.CR cs.LO
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
FBK-IRST（布鲁诺·凯斯勒基金会-材料与微系统研究所）
寻找SAT公式的小不可满足核的问题最近受到了广泛的关注，主要是因为它在形式化验证中的应用。然而，命题逻辑往往是不够的表达，表示许多有趣的验证问题，这可以更自然地解决的框架可满足性模理论，SMT。令人惊讶的是，在SMT中找到不可满足的核心的问题在文献中很少受到关注。在本文中，我们提出了一种新的方法来解决这个问题，称为引理提升方法。其主要思想是将SMT求解器与外部命题核心提取器相结合。SMT求解器产生在搜索期间发现的理论引理，动态地将适量的理论信息提升到布尔级别。核心提取器，然后调用原始SMT问题和理论引理的布尔抽象。这将导致一个不可满足的核心，为原来的SMT问题，一旦剩余的理论引理被删除。这种方法在概念上很有趣，在实践中有几个优点。事实上，它的实现和更新非常简单，并且它可以以即插即用的方式与每个命题核心提取器接口，以便免费受益于已经或将要提供的所有未饱和核心还原技术。我们已经评估了我们的算法与一个非常广泛的实证测试SMT-LIB基准，这证实了这种方法的有效性和潜力。
2014-01-16 cs.AI cs.LO
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
University of Trento（特伦托大学）；Rice University（莱斯大学）
提出一种将d-DNNF编译与查询扩展到SMT层面的通用技术，通过结合预计算的理论引理，使得SMT查询可归约为命题查询，支持多时间查询。
2026-05-24 cs.LO
Bitwuzla at the SMT-COMP 2020
在本文中，我们提出Bitwuzla，我们的可满足性模理论（SMT）求解器的理论位向量，浮点，数组和未解释的功能及其组合。我们讨论了选定的功能，并提供了其配置和参加2020年年度SMT竞赛的详细信息。
2020-05-30 cs.LO
Equational Anti-Unification over Absorption Theories
本文提出一种基于规则的算法，解决纯吸收理论下的反合一问题，该问题为无穷的，但算法终止并给出最小完备解集的有限表示，且线性变体是有限的。
2023-10-17 cs.LO cs.SE
Language and Proofs for Higher-Order SMT (Work in Progress)
可满足性模理论（SMT）求解器多年来已经能够处理从基础逻辑到完全一阶逻辑模理论的越来越多的表达公式。然而，SMT中的高阶逻辑仍然很少被探索。Matryoshka项目于2017年3月启动，其主要目标之一是将SMT求解器和其他自动证明器的推理能力扩展到一阶逻辑之外。在这份初步报告中，我们报告了SMT-LIB语言的扩展，SMT求解器的标准输入格式，以处理高阶结构。我们还讨论了如何增强SMT求解器veriT的证明格式，以适应这些新的构造和它们所需的求解技术。
2017-12-05 cs.LO
Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
IMDEA Software Institute（IMDEA软件研究所）；Universidad Politécnica de Madrid（马德里理工大学）；CIFASIS
该研究提出首个针对LTLt的完整静态反应式综合方法，结合布尔抽象与函数综合生成确定性控制器，兼具可预测性、高效性及输出优化能力。
2024-07-12 cs.AI cs.LO cs.SE
System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
School of Computing, Informatics, and Decision Systems Engineering（计算、信息与决策系统工程学院）；Arizona State University（亚利桑那州立大学）
本研究提出实现ASPMT紧片段到SMT转换的编译器aspsmt2smt，结合gringo部分基化与z3求解变量，可有效处理实数计算以支持连续变化推理。
2025-06-12 cs.AI cs.LO
Learning Quantitative Automata Modulo Theories
University of Texas at Austin（德克萨斯大学奥斯汀分校）
本文提出从输入序列赋值上的约束集合中学习确定性定量自动机的问题，并提出了主动学习算法 QUINTIC，通过演绎推理在自动机空间上执行完整搜索，保证最小化和正确终止，评估表明其能有效学习多种定量自动机。
2024-11-15 cs.FL cs.LG cs.LO
