在无归纳的情况下求解归纳数据类型上的 Horn 子句
计算机科学中的逻辑
2018-10-23 v1 编程语言
摘要
我们处理基于归纳定义的数据结构（如列表与树）理论的约束 Horn 子句（CHCs）可满足性验证问题。我们提出一种变换技术，其目标是从这些 CHCs 中移除这些数据结构，从而将其可满足性归约为整数与布尔值上 CHCs 的可满足性问题。我们提出一种变换算法，并识别出一类总能使其成功的子句。我们还考虑了该算法的一种扩展，将子句变换与整数约束上的推理相结合。通过实验评估，我们表明我们的技术极大提升了 Z3 求解器处理 CHCs 的有效性。我们还表明，我们基于 CHC 变换随后进行 CHC 求解的验证技术，相对于扩展了归纳的 CHC 求解器具有竞争力。本文正在考虑接受于 TPLP。
引用
@article{arxiv.1804.09007,
title = {Solving Horn Clauses on Inductive Data Types Without Induction},
author = {Emanuele De Angelis and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
journal= {arXiv preprint arXiv:1804.09007},
year = {2018}
}
备注
Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018. 22 pages, LaTeX