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

量词公式的插值是LIUF理论中一个未解决的问题。针对如何消去量词、消去量词后如何求出公式的插值等问题,提出了一种基于无量词公式理论插值的新算法。首先利用斯科拉姆化消去存在量词,并通过引入新变量消去全称量词,使量词公式变为无量词公式;然后运用已有的LIUF无量词理论公式插值算法求出变换后公式的插值;最后将插值中含有的新变量用存在量词或全称量词替换,从而得到LIUF理论中量词公式的插值。实例表明新算法可以解决LIUF理论中量词公式的插值问题。