Model Finding for Recursive Functions in SMT
Model Finding for Recursive Functions in SMT
复制标题
SMT 中递归函数的模型查找
DOI：
10.1007/978-3-319-40229-1_10
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
C. Tinelli
中科院分区：
文献类型：
--
作者：
Andrew Reynolds;J. Blanchette;Simon Cruanes;C. Tinelli
最近，SMT求解器已扩展使用，以在某些有限的一阶逻辑片段中查找普遍量化公式的模型。本文介绍了一项翻译，该翻译简化了公理，指定了包括终止功能在内的大量递归函数（包括终止功能）的普遍量化公式，这些公式适用于这些公式。评估证实，该方法改善了三个来源的基准基准上现有求解器的性能。该翻译是在CVC4求解器中的预处理程序和名为Nunchaku的新的高阶模型查找器中实现的。
SMT solvers have recently been extended with techniques for finding models of universally quantified formulas in some restricted fragments of first-order logic. This paper introduces a translation that reduces axioms specifying a large class of recursive functions, including terminating functions, to universally quantified formulas for which these techniques are applicable. An evaluation confirms that the approach improves the performance of existing solvers on benchmarks from three sources. The translation is implemented as a preprocessor in the CVC4 solver and in a new higher-order model finder called Nunchaku.
登录
查看更多内容
具有保护递归的高效协同编程
影响因子：
--
作者：
Atkey R
通讯作者：
Atkey R
（共）归纳谓词、（共）代数数据类型和（共）递归函数的关系分析
影响因子：
1.9
作者：
Jasmin Christian Blanchette
通讯作者：
Jasmin Christian Blanchette
使用 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
DOI：
10.1007/s10817-011-9234-1
发表时间：
2011
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Alexander Krauss
通讯作者：
Alexander Krauss
基础可扩展核心递归：证明助理的观点
DOI：
10.1145/2784731.2784732
发表时间：
2015
期刊：
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Jasmin Christian Blanchette;Andrei Popescu;Dmitriy Traytel
通讯作者：
Dmitriy Traytel