在归纳构造演算中构建判定过程
计算机科学中的逻辑
2007-07-10 v1
摘要
人们普遍认为，未来证明助手（proof assistants）的成功将依赖于其能够在演绎中融入计算的能力，从而模仿数学家将命题 P 的证明替换为通过可能复杂的计算从 P 获得的等价命题 P' 的证明。在本文中，我们研究了归纳构造演算（calculus of inductive constructions）的一个新版本，该版本通过演算的转换规则将任意判定过程融入演绎中。在归纳构造演算的语境下，该问题的新颖之处在于计算机制随证明检查而变化：目标连同当前上下文中可用的用户假设集一起被发送至判定过程。我们的主要结果表明，该对构造演算的扩展并未损害其主要性质：合流性、主体归约、强正规化和一致性均得以保持。
引用
@article{arxiv.0707.1266,
title = {Building Decision Procedures in the Calculus of Inductive Constructions},
author = {Frédéric Blanqui and Jean-Pierre Jouannaud and Pierre-Yves Strub},
journal= {arXiv preprint arXiv:0707.1266},
year = {2007}
}