二阶逻辑的表达能力与计算复杂性

Gabbay、Ohlbach等人认为表达能力是逻辑系统的最重要的性质之一。表达能力的研究和比较可以使我们对各种逻辑系统有更深刻地认识，为在实际应用选取"最好"的表示系统提供帮助。逻辑系统之间的表达能力关系与计算复杂性理论中的重要猜想有着密不可分的联系，因此，表达能力的研究也具有重要的理论意义。然而表达能力研究被认为是具有挑战性的课题。本项目一方面以申请者提出的模型等价归约为工具研究二阶命题逻辑(即QBF)的表达能力及其与计算复杂性的关系。另一方面，提出Henkin二阶量词，推广比例量词，并研究带有这些二阶量词谓词逻辑，提出有穷模型等价归约，进而研究各种谓词逻辑的表达能力。本项目的就是进一步探讨逻辑系统表达能力的强弱与计复杂性理论中的重要猜想之间的联系。

本项目主要研究二阶逻辑的表达能力与计算复杂性，实现了主要预期目标。主要工作如下：（1）提出并研究NP逻辑系统，以模型等价归约为标准研究了其表达能力与计算复杂性的联系。（2）提出了量化布尔电路（QCIRC），建立了各类QCIRC之间的多项式时间的等价归约。（3）面向“是否存在刻画PTIME的逻辑”这一重大开问题，提出了二阶HORN逻辑（SO-HORN）的多种扩充，研究了它们的描述复杂性，解决了20年前Graedel提出的一个问题。（4）提出了建立面向规划验证的证明系统的思想，提出了不完全知识下规划的谨慎语义，建立了相应的Hoare型证明系统。. 本项目共发表论文15篇（含已接受论文和会议报告）。其中期刊论文发表在Theoretical Computer Science（已接受），Mathematical Logic Quarterly（已接受）JCST，Science China Information Science (已接受)，Minds and Machines（DOI 10.1007/s11023-012-9288-9）上。会议文章主要发表在相关领域最好的国际会议论文集上(如 SAT11、SAT12)。. 在本项目资助下，已有两位博士生（金继伟、冯世光）获得博士学位。其中，金继伟在中国科学院软件所做博士后，冯世光受聘在德国莱比锡大学计算机系工作。