论插值算法的完备性
On the Completeness of Interpolation Algorithms
AI总结：
该研究聚焦插值算法可得到的插值元范围问题，定义了插值算法的完备性概念，并针对多类逻辑的标准消解与相继式演算算法，得出了不完备性及不同类型的完备性结果。
摘要：
Craig插值是经典逻辑与非经典逻辑的一项基本性质，在从哲学逻辑到计算机辅助验证的诸多领域有着广泛应用。哪些插值元可通过插值算法得到这一问题具有极为重要的意义。受该问题启发，我们开展了插值算法完备性性质的研究。若对于蕴含式A→B的每一个语义上可行的插值元C，都存在A→B的一个证明P，使得C与$\boldsymbol{\u2113}(P)$逻辑等价，则称插值算法$\boldsymbol{\u2113}$是“完备的”。我们针对命题逻辑、模态逻辑和一阶逻辑的消解算法与相继式演算的若干标准算法，得出了不完备性结论以及不同类型的完备性结果。
英文摘要：
Craig interpolation is a fundamental property of classical and non-classic 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 $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
