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

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