[00132953]包封法及推理系统的可判定性

主要进行了下述方面的研究：1、软件正确性方法的研究。这方面的研究集中在自动推理方法及其复杂性和模型检测方法的研究。(1)与G.Dowek（法）合作，建立了一个带包封的矢列式演算LJB，证明了对正公式而言LJB的可判定性，以及LJB相对于Gentzen矢列式演算的可靠性与完备性。由此给出了一个适用于F系统和简单类型理论等有意义的理论中正公式类的可判定性的一般方法。并用Ocaml语言予以了实现。(2)在逻辑证明的结构和引理的复杂度方面，阐述了引理消除可能引起的不同逻辑证明结构之间的变换，获得了对引理在不同类型逻辑证明结构中的作用的新认识。(3)在降低模型检测空间复杂性方面，扩展了之前提出的一种结合程序静态分析将一个性质分解成多个性质进行验证的方法的适用性。在方法和工具方面，初步完成一个基于SAT的ACTL性质的验证工具。其它研究包括对自动机转换方法的分析以减少转换后自动机的状态空间。2、程序语义学研究。与张国强（美）合作，完全解决了90年代初欧洲域论专家所提出的由meet-cpos和稳定函数所构成的笛卡儿闭范畴的最大子范畴这一公开问题的第一个子问题，并部分解决了另一个子问题。