Induction for SMT Solvers
Induction for SMT Solvers
复制标题
SMT 求解器的归纳
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Viktor Kunčak
中科院分区：
文献类型：
--
作者：
Andrew Reynolds;Viktor Kunčak
可满足性模理论求解器越来越多地用于求解整数和项代数等结构上的量化公式。在这种情况下，量词实例化与地面决策过程相结合，不足以证明许多感兴趣的公式。我们提出了一套技术，引入归纳推理到SMT求解算法，这是健全的SMT-LIB标准中的结构的解释。这些技术包括要证明的猜想的归纳加强，以及在归纳证明期间自动发现子目标的设施，其中子目标本身可以使用归纳来证明。该技术已在CVC 4中实现。我们的实验表明，所开发的技术具有良好的性能和覆盖范围的归纳推理问题。我们的实验还显示了自然数的不同表示和量词实例化技术对归纳推理性能的影响。我们的解决方案在CVC 4开发库中免费提供。除了其整体效率，它还具有接受SMT-LIB输入并与CVC 4的其他SMT解决技术集成的优势。
Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas of interest in such cases. We present a set of techniques that introduce inductive reasoning into SMT solving algorithms that is sound with respect to the interpretation of structures in SMT-LIB standard. The techniques include inductive strengthening of conjecture to be proven, as well as facility to automatically discover subgoals during an inductive proof, where subgoals themselves can be proven using induction. The techniques have been implemented in CVC4. Our experiments show that the developed techniques have good performance and coverage of a range of inductive reasoning problems. Our experiments also show the impact of different representations of natural numbers and quantifier instantiation techniques on the performance of inductive reasoning. Our solution is freely available in the CVC4 development repository. In addition its overall effectiveness, it has an advantage of accepting SMT-LIB input and being integrated with other SMT solving techniques of CVC4.
通过 LI UIF 求解无递归 Horn 子句
DOI：
10.1007/978-3-642-25318-8_16
发表时间：
2011
期刊：
影响因子：
--
作者：
Ashutosh Gupta;Corneliu Popeea;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko