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

Interpolation Algorithm for Quantifier Formulas in LIUF Theory

作　　者：李千卉 江建国[1] 刘文秀 

机构地区：[1]辽宁师范大学数学学院,辽宁大连

出　　处：《软件工程与应用》2015年第6期121-128,共8页Software Engineering and Applications

摘　　要：量词公式的插值是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.

关 键 词：理论插值 LIUF理论 量词消去 斯科拉姆化 

分 类 号：G6[文化科学—教育学]