论文标题
克雷格（Craig
Craig Interpolation with Clausal First-Order Tableaux
论文作者
论文摘要
我们开发用于计算两个给定公式的Craig-lyndon插值，并具有构造clausal tableaux的一阶定理掠夺者。可以以这种方式理解的掠夺者包括基于两个家族的计算的有效面向机器的系统：以目标为导向的模型消除和连接方法，以及诸如Hypertableau cyculus之类的自下而上。我们提出了以封闭式tableaux表示的一阶证明的第一种插值方法，该方法分为两个阶段，类似于已知的插值方法用于解决方案。第一阶段是对Tableau结构的诱导，足以计算命题插值。我们表明，这可以线性模拟不同的突出命题插值方法，这些插值方法是通过在分辨率扣除树上诱导运行的。在第二阶段，介绍了插入式提升，量化的变量，将变量替代某些术语（常数和复合项）。我们根据Herbrand的定理和要提起的公式的不同表征与文献相比，我们为interpolant举重的正确性（对于没有内在平等的情况）合理。此外，我们讨论了与基于可靠的tableaux的一阶插值的研究和实际实现有关的各个微妙方面。
We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient machine-oriented systems based on calculi of two families: goal-oriented such as model elimination and the connection method, and bottom-up such as the hypertableau calculus. We present the first interpolation method for first-order proofs represented by closed tableaux that proceeds in two stages, similar to known interpolation methods for resolution proofs. The first stage is an induction on the tableau structure, which is sufficient to compute propositional interpolants. We show that this can linearly simulate different prominent propositional interpolation methods that operate by an induction on a resolution deduction tree. In the second stage, interpolant lifting, quantified variables that replace certain terms (constants and compound terms) by variables are introduced. We justify the correctness of interpolant lifting (for the case without built-in equality) abstractly on the basis of Herbrand's theorem and for a different characterization of the formulas to be lifted than in the literature. In addition, we discuss various subtle aspects that are relevant for the investigation and practical realization of first-order interpolation based on clausal tableaux.
