中文摘要：

计算机基础理论的研究直接推动着程序设计的技术、语言及其语义学的发展。形式推演系统的可判定性，判定效率及其自动证明一直是国际上该领域的研究热点之一。最近，法国国家自动化研究中心高级研究员、著名的école polytechnique计算机科学实验室G. Dowk教授与本项目申请人蒋颖的合作研究工作在该方面取得了一些积极的结果。本项目申请基于G. Dowek教授与蒋颖的最近的研究结果。拟将对该研究结果中所提出的简单而且易实现的包封法(bracketing)进行深入的研究，进而将其一般化，建立相应的扩展形式推演系统, 证明其可判定性, 研究该系统与其它已知推演系统的的关系, 比较相应的判定效果及效率。其结果可用于证明一些重要形式推演系统的可判定性，及其定理证明的自动生成。

结论摘要：

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