稳定模型一阶逻辑理论是非单调逻辑研究领域一个重要的研究分支，应用这一语言可以自然地对一类计算复杂度高的问题进行编码，但目前缺少基于上述语言的求解器。本项目研究如何将有限结构的稳定模型下的一阶逻辑理论转化为析取逻辑程序，在固定一个论域的情况下应用析取逻辑程序求解器进行推理的问题；其中一个关键问题是如何高效地消去稳定模型下一阶逻辑理论的存在量词。 本项目研究成果属于应用基础研究，针对目前研究仅对一类描述能力较弱的片段才能消去存在量词所存在的局限，研究在有限结构下通过引入新的辅助谓词，或者在允许序且不引入新的辅助谓词的情况下，消去所有存在量词的方法；以及面向特定领域特殊片段下的高效存在量词消去算法。通过将已有的析取逻辑程序求解器作为黑盒调用，可以实现稳定模型下一阶逻辑理论求解器。 对面向SOA服务组合进行检测与诊断可以保证业务流程的正确性、可用性与实效性，但其验证过程需要大量繁琐甚至复杂的人工操作。为了提高面向SOA服务组合流程形式化验证的自动化程度，本项目研究成果选用BPEL语言作为服务组合流程的描述语言，应用基于因果关系的动作理论给出BPEL语言活动语义，将SOA架构下的服务描述、组合、匹配与选择转化为基于值的溯因诊断模型Mrspoa，应用稳定模型下一阶逻辑理论求解器可以对服务组合和服务特征交互问题进行检测与诊断。