证明策略及其有效性问题

PROOF STRATEGIES AND VALIDITY

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

INCAPS (INteractive Computer-Aided Proving System) is a proof system of temporal logic. This paper outlines its proof strategies' (tactics, tacticals) variety and structure. The kernel of it is to discuss the validity of tactics and tacticals. After introducing several new concepts: proof strategies' level number, function tree and B function defined on it, we show that INCAPS' proof strategies are valid.