数组理论的无量词插值
计算机科学中的逻辑
2015-07-01 v5
摘要
插值在模型检验中的应用正成为实现硬件和软件快速鲁棒验证的关键技术。然而，基于数组理论的编码应用受到一般无法推导出无量词插值的限制。在本文中，我们证明对于外延数组理论的Skolem化版本，可以获得无量词插值。我们通过两种方式证明：(1) 非构造性地，使用模型论中的融合概念，已知对于全称理论，融合等价于承认无量词插值；(2) 构造性地，通过设计一个基于求解数组更新之间方程的插值过程。（有趣的是，重写技术被用于求解器的关键步骤及其正确性证明。）据我们所知，这是首次成功计算具有外延性的数组理论变体的无量词插值。
引用
@article{arxiv.1204.2386,
title = {Quantifier-Free Interpolation of a Theory of Arrays},
author = {Roberto Bruttomesso and Silvio Ghilardi and Silvio Ranise},
journal= {arXiv preprint arXiv:1204.2386},
year = {2015}
}