Craig 插值定理在 Isabelle/HOL 中的形式化与机械化
计算机科学中的逻辑
2007-05-23 v1
摘要
我们在 Isabelle/HOL 中对 Craig 插值定理进行形式化与机械化。我们既形式化又非形式化地给出所有定义与引理陈述。我们还非形式化地转录形式化证明。我们详细描述了机械化方案的主要特征，如对一阶公式绑定的形式化。我们还给出了 Craig 插值定理的一些应用。
关键词
引用
@article{arxiv.cs/0607058,
title = {Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL},
author = {Tom Ridge},
journal= {arXiv preprint arXiv:cs/0607058},
year = {2007}
}