INCAPS:一个交互式计算机辅助定理证明系统

INCAPS: AN INTERACTIVE COMPUTER-AIDED THEOREM-PROVING SYSTEM

本文提出了一个具有自然演绎特色的一阶时序逻辑系统——FOTL系统,并且已用ML语言表示出F0TL系统,从而得到了一个在证明风格和实现技术上类似于Edinburgh LCF的计算机辅助定理证明系统——INCAPS系统.INCAPS系统与Edinbursh LCF的区别主要在于它们所支持的逻辑不同:FOTL系统不含有高阶类型的项,而PPλ中没有时序连接词。INCAPS系统主要可用于程序及动态信息系统的描述与验证。

A natural deduction system of first-order temporal logic (FOTL logic) is presented, and mechanized in standard ML programming language into an interactive computer-aided therem proving system (INCAPS system). INCAPS system is quite similar to Edinburgh LCF but different from it in logics they support. The difference between FOTL and PPλ lies in that the terms of higher-order types are not allowed in FOLT as in PPλ and the temporal logic connectives are not included in PPX as in FOTL. INCAPS system can be used for specification and verfication of programs and dynamic information systems.