论文部分内容阅读
INCAPS(INteractiv Computer-Aided Proving System)是一个面向时序逻辑的交互式计算机辅助证明系统。本文简要介绍了其证明策略(tactics,tacticals)的类别、结构,并在引入证明策略的层次数、函数树及树上B函数等新概念前提下,深入探讨和证明了IN-CAPS证明策略的有效性问题。