构建归纳构造演算的决策程序
摘要：未来证明助手的成功将依赖于它们能够在推导过程中融入计算，以模拟数学家在用复杂计算替换命题P的证明时的行为。在本文中，我们研究了归纳构造演算的一个新版本，该版本通过归纳构造演算的转换规则将任意决策过程纳入推导中。在归纳构造演算的背景下，该问题的创新之处在于计算机制在证明检查过程中会发生变化：目标会与当前上下文中可用的用户假设集一起发送给决策过程。我们的主要结果表明，这种构造演算的扩展不会损害其主要特性：会保留合流性、主题约简性、强标准化性和一致性。
作者：Fr''ed''eric Blanqui (INRIA Lorraine - LORIA), Jean-Pierre Jouannaud (INRIA Futurs), Pierre-Yves Strub (INRIA Futurs)
论文ID：0707.1266
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-07-10