LIUF理论量词公式的插值算法
Interpolation Algorithm for Quantifier Formulas in LIUF Theory
DOI: 10.12677/SEA.2015.46016, PDF, HTML, XML, 下载: 1,928  浏览: 4,989 
作者: 李千卉, 江建国, 刘文秀：辽宁师范大学数学学院，辽宁 大连
关键词: 理论插值；LIUF理论；量词消去；斯科拉姆化；Theory Interpolation； LIUF Theory； Eliminate Quantifier； Skolemization
摘要: 量词公式的插值是LIUF理论中一个未解决的问题。针对如何消去量词、消去量词后如何求出公式的插值等问题，提出了一种基于无量词公式理论插值的新算法。首先利用斯科拉姆化消去存在量词，并通过引入新变量消去全称量词，使量词公式变为无量词公式；然后运用已有的LIUF无量词理论公式插值算法求出变换后公式的插值；最后将插值中含有的新变量用存在量词或全称量词替换，从而得到LIUF理论中量词公式的插值。实例表明新算法可以解决LIUF理论中量词公式的插值问题。
Abstract: The problem of interpolation for quantifier formulas is still unsolved in LIUF theory. For the problems of how to eliminate quantifiers and compute the interpolation after eliminating the quantifiers, a new algorithm based on quantifier-free theory interpolation algorithm is proposed. First, the skolemization was used to eliminate existential quantifiers and universal quantifiers were instantiated with free individual variables to create quantifier-free formulas; Then, the quantifier-free theory interpolation algorithm was used to compute the formulas; Finally, the new variables were eliminated by quantifying universally or existentially, and interpolation for quantifier formulas was obtained. The algorithm example shows that the new interpolation algorithm can solve the problem of quantifier formulas in LIUF theory.
文章引用：李千卉, 江建国, 刘文秀. LIUF理论量词公式的插值算法[J]. 软件工程与应用, 2015, 4(6): 121-128. http://dx.doi.org/10.12677/SEA.2015.46016

参考文献

[1] Craig, W. (1957) Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. The Journal of Symbolic Logic, 22, 269-285.
http://dx.doi.org/10.2307/2963594
[2] McMillan, K.L. (2003) Interpolation and SAT-Based Model Checking. In: CAV 2003: 2003 Proceedings of the 15th Conference on Computer Aided Verification, Lecture Notes in Computer Science, Springer, Berlin, 1-13.
[3] Weissenbacher, G. (2010) Program Analysis with Interpolants. Magdalen College, Oxford University, Oxford, England, 277.
[4] Henzinger, T.A., Jhala, R., Majumdar, R., et al. (2004) Abstractions from Proofs. ACM SIGPLAN Notices, 39, 232- 244.
[5] Bruttomesso, R., Rollini, S.F., Sharygina, N., et al. (2010) Flexible Interpolation Generation in Satisfiability Modulo Theories. ICCAD 2010: 2010 Proceedings of the 14th International Conference on Computer-Aided Design, IEEE, Piscataway, 770-777.
[6] 陈祖希, 徐中伟, 霍伟伟, 等. 基于Craig插值的线性混成系统符号化模型检测[J]. 电子学报, 2014(7): 1338- 1346.
[7] McMillan, K.L., Ball, T. and Jones, R.B. (2006) Lazy Abstraction with Interpolations. In: CAV 2006: 2006 Proceedings of the 18th Conference on Computer Aided Verification, Springer, Berlin, 123-136.
[8] 屈婉霞, 李暾, 郭阳, 杨晓东. 模型检验中抽象技术研究综述[J]. 计算机工程与应用, 2006, 42(33): 15-19.
[9] Nieuwenhuis, R., Oliveras, A. and Tinelli, C. (2006) Solving SAT and SAT Modulo Theories: From an Abstract Davis- Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 53, 937-977.
[10] Pudlak, P. (1997) Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Mathematical Institute Academy of Sciences of Czech Republic, 62, 1-20.
http://dx.doi.org/10.2307/2275583
[11] Alberti, F., et al. (2014) An Extension of Lazy Abstraction with Interpolation of Programs with Arrays. Formal Methods in System Design, 45, 63-109.
http://dx.doi.org/10.1007/s10703-014-0209-9
[12] Lopes, N.P. and Monteiro, J. (2015) Automatic Equivalence Checking of Programs with Uninterpreted Functions and Integer Arithmetic. International Journal on Software Tools for Technology Transfer, Springer, Science, 1-16.
[13] Fitting, M. (1996) First-Order Logic and Automated Theorem Proving. Springer, Berlin.
http://dx.doi.org/10.1007/978-1-4612-2360-3

为你推荐