﻿ LIUF理论量词公式的插值算法

LIUF理论量词公式的插值算法Interpolation Algorithm for Quantifier Formulas in LIUF Theory

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.

[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

Top