标题:
LIUF理论量词公式的插值算法Interpolation Algorithm for Quantifier Formulas in LIUF Theory
作者:
李千卉, 江建国, 刘文秀
关键字:
理论插值, LIUF理论, 量词消去, 斯科拉姆化Theory Interpolation, LIUF Theory, Eliminate Quantifier, Skolemization
期刊名称:
《Software Engineering and Applications》, Vol.4 No.6, 2015-12-28
摘要:
量词公式的插值是LIUF理论中一个未解决的问题。针对如何消去量词、消去量词后如何求出公式的插值等问题，提出了一种基于无量词公式理论插值的新算法。首先利用斯科拉姆化消去存在量词，并通过引入新变量消去全称量词，使量词公式变为无量词公式；然后运用已有的LIUF无量词理论公式插值算法求出变换后公式的插值；最后将插值中含有的新变量用存在量词或全称量词替换，从而得到LIUF理论中量词公式的插值。实例表明新算法可以解决LIUF理论中量词公式的插值问题。
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.