Coming to terms with quantified reasoning
Coming to terms with quantified reasoning
复制标题
接受量化推理
DOI：
10.1145/3009837.3009887
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
A. Voronkov
中科院分区：
文献类型：
--
作者：
L. Kovács;Simon Robillard;A. Voronkov
有限项代数理论提供了描述函数语言语义的自然框架。有效推理术语代数的能力对于通过归纳定义的数据类型（例如列表和树）自动进行功能性或命令性程序的程序分析和验证至关重要。然而，由于有限项代数理论不是有限公理化的，因此推理项代数的量化属性具有挑战性。在本文中，我们讨论了关于操作项代数的程序的属性的完整一阶推理，并描述了通过使用一阶定理证明来实现此目的的两种方法。我们的第一种方法是使用有限数量的语句对项代数理论进行保守扩展，而我们的第二种方法依赖于使用附加推理规则扩展一阶定理证明者的叠加微积分。我们在一阶定理证明器 Vampire 中实现了我们的工作，并根据大量归纳数据类型基准以及博弈论约束对其进行了评估。我们的实验结果表明，我们的方法能够为许多以前最先进的方法无法解决的难题找到证据。我们还表明，实施我们的方法的 Vampire 优于能够处理归纳数据类型的现有 SMT 求解器。
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or imperative programs over inductively defined data types such as lists and trees. However, as the theory of finite term algebras is not finitely axiomatizable, reasoning about quantified properties over term algebras is challenging. In this paper we address full first-order reasoning about properties of programs manipulating term algebras, and describe two approaches for doing so by using first-order theorem proving. Our first method is a conservative extension of the theory of term alge- bras using a finite number of statements, while our second method relies on extending the superposition calculus of first-order theorem provers with additional inference rules. We implemented our work in the first-order theorem prover Vampire and evaluated it on a large number of inductive datatype benchmarks, as well as game theory constraints. Our experimental results show that our methods are able to find proofs for many hard problems previously unsolved by state-of-the-art methods. We also show that Vampire implementing our methods outperforms existing SMT solvers able to deal with inductive data types.
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson