析取逻辑程序，命题缺省逻辑及其它相同复杂度问题的研究

析取逻辑程序和命题缺省逻辑是非单调推理领域的两个重要分支。基于析取逻辑程序回答集语义和基于命题缺省逻辑扩充的推理问题的计算复杂度都处在复杂度的多项式分层的第二层。与上述问题的计算复杂度相同的标准逻辑问题是2QBF。.本项目计划研究析取逻辑程序，命题缺省逻辑以及2QBF问题之间的联系，以此为基础研究析取逻辑程序和命题缺省逻辑的求解和计算，并进一步考虑这些结果在人工智能和知识表示与推理领域的其它相同复杂度的问题中的应用。

我们研究了回答集逻辑程序，命题析取逻辑等相关问题。这些问题的复杂度都处于复杂性多项式分层的第二层。..从包含聚集函数的回答集程序出发，我们定义了凸聚集函数。我们证明了包含凸聚集函数的回答集逻辑程序的复杂度仍然在NP/coNP，而对于任何非凸聚集函数，都存在一个包含这个函数的逻辑程序，其复杂度提升到了第二层。因此我们找到了聚集函数将逻辑程序从$NP/coNP$提升到更高层次的精确界限。基于这些理论结果，我们实现了一个基于有序完备集的回答集求解器GROCv2。这部分结果发表在人工智能领域的权威杂志《Artificial Intelligence》上。..有关命题缺省逻辑的研究，我们从应用问题出发，考虑了在结论部分可以出现析取和包含权重的缺省逻辑。我们实现了一个这样的缺省逻辑求解器，除了计算扩充，还可以计算最大/最小扩成。我们以此为基础用来解决选举问题中的Judgment Aggregation Rules的计算。同时我们还研究了基于回答集程序的Banks选举和Slater选举问题的求解。这部分结果发表在国内的核心期刊上。..我们研究了析取逻辑程序的求解问题。一方面是研究析取逻辑程序和2QBF的关系，然后通过求解2QBF实现析取逻辑程序的求解；另一方面是研究析取逻辑程序和SMT的关系，然后通过已有的SMT求解器加以求解。在研究过程中，我们发现由于析取逻辑程序的计算复杂度限制，求解过程中难以避免通过交替的猜想和验证过程得到结果，其中猜想和验证过程的复杂度都是NP/coNP的。我们实现了一个析取逻辑程序的初步的系统，但是目前的求解效率尚不及已有的高效的系统。由于实验的结果没有说服力，目前有关求解器的成果还没有相关的论文发表。