LIUF和LDEs理论是理论插值中的两个热点研究理论。以这两种理论为背景理论的插值在可满足性模理论(SMT)问题上有十分重要的应用。LIUF和LDEs理论插值能扩大SMT的应用范围,同时缩减可满足性问题的判定时间,提高判定效率。但现有的插值算法仍存在一些问题,如:LIUF理论中无法求出量化公式的插值,LDEs理论中无法消去插值中非公有变量等。本文就从此处入手,提出了两种新的插值算法。在LIUF理论中,量化公式的插值是一个未解决的问题。在某些情况下,无量词公式插值是不存在的,这时就需要引入量词,但带有量词的公式很难求出插值,因为在消去量词的过程中必定会引入新的变量,新变量的引入就会使问题变得复杂化。针对该问题,本文提出了LIUF理论量化公式插值算法。该算法能有效解决引入的新变量问题,并能快速求出量化公式插值。在LDEs理论中,求解插值和消去插值中非公有变量一直是所面临的问题。在很多情况下,所求的插值中仍含有非公有变量,这时的插值并不是所要求的插值。针对此问题,本文提出了LDEs理论插值算法。该算法能快速判断出LDEs理论是否存在插值,并能有效解决插值中的非公有变量问题。