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

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