克雷格插值定理在Isabelle/HOL中得到正式化和机械化
摘要：应用于Isabelle/HOL的构造性、证明论证的形式化机械化把Craig的插值定理证明。我们正式和非正式地给出了所有的定义和引理陈述。我们还非正式地转录了正式的证明。我们详细说明了我们机械化的主要特点，如一阶公式的绑定的形式化。我们还给出了一些应用Craig的插值定理。
作者：Tom Ridge
论文ID：cs/0607058
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23