一句话：首次系统研究插值算法的完备性，证明若干归结与相继式演算标准插值算法的不完备性及多种完备性。
克雷格插值在哲学逻辑与计算机辅助验证中有广泛应用，但一个插值算法能否生成所有可能的插值尚不清楚。本文首次提出插值算法完备性的研究框架：若对任意蕴含 A→B 的任意插值 C，都存在 A→B 的证明 P，使得 I(P) 与 C 逻辑等价，则称算法 I 完备。作者针对命题、模态与一阶逻辑的归结和相继式演算，分析若干标准插值算法的完备性，得到不完备性结果以及不同强度的完备性定理，从而刻画这些算法可产生插值的范围。
Craig interpolation is a fundamental property of logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm ℐ is complete if, for every interpolant C of an implication A → B, there is a proof P of A → B such that C is logically equivalent to ℐ(P). We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.