证明策略及其有效性问题

incaps(interactivcomputer-aidedprovingsystem)是一个面向时序逻辑的交互式计算机辅助证明系统。本文简要介绍了其证明策略(tactics,tacticals)的类别、结构,并在引入证明策略的层次数、函数树及树上b函数等新概念前提下,深入探讨和证明了in-caps证明策略的有效性问题。