| 摘要: |
| INCAPS(INteractiv Computer-Aided Proving System)是一个面向时序逻辑的交互式计算机辅助证明系统。本文简要介绍了其证明策略(tactics,tacticals)的类别、结构,并在引入证明策略的层次数、函数树及树上B函数等新概念前提下,深入探讨和证明了IN-CAPS证明策略的有效性问题。 |
| 关键词: |
| DOI： |
| 分类号: |
| 基金项目:国家自然科学基金 |
|
| PROOF STRATEGIES AND VALIDITY |
|
He Pei
|
| Abstract: |
| 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. |
| Key words: |
