通过消去边界点消除量词
计算机科学中的逻辑
2012-06-06 v2 离散数学
摘要
我们考虑从布尔 CNF 公式中消去存在量词的问题。我们的方法基于以下观察：通过添加消去边界点的 F 的归结子句，可以消除量化 CNF 公式 F 对一组变量的依赖。该方法类似于 [9] 中描述的量词消去方法。本文所述方法的不同之处有两点：{\bullet} 分支仅在量化变量上进行，{\bullet} 通过调用 SAT 求解器显式搜索边界点。尽管我们在本文之前发表了论文 [9]，但从时间顺序上看，本报告的方法是首先发展起来的。该方法的初步报告已在 [10]、[11] 中给出。由于准备专利申请 [8]，我们推迟了该方法的发表。
引用
@article{arxiv.1204.1746,
title = {Removal of Quantifiers by Elimination of Boundary Points},
author = {Eugene Goldberg and Panagiotis Manolios},
journal= {arXiv preprint arXiv:1204.1746},
year = {2012}
}
备注
The only change with respect to the previous version is a modification of the acknowledgement section