科创中国

生物产业,制造业

本项目研究成果在理论研究上，(1) 研究在有限结构下通过引入新的辅助谓词，或者在允许序且不引入新的辅助谓词的情况下，消去所有存在量词的方法；(2) 根据基于模型的程序诊断这一特定领域的特点研究特殊片段下的高效存在量词消去算法。稳定模型一阶逻辑理论是非单调逻辑研究领域一个重要的研究分支，应用这一语言可以自然地对一类计算复杂度高的问题进行编码，但目前缺少基于上述语言的求解器。本项目研究如何将有限结构的稳定模型下的一阶逻辑理论转化为析取逻辑程序，在固定一个论域的情况下应用已有的析取逻辑程序求解器进行推理的问题；在该计算过程中，一个关键问题是在转化为析取逻辑程序时如何高效地消去稳定模型下一阶逻辑理论的存在量词，这样才能在固定一个论域时完成例化的工作。现有研究工作仅能对一类描述能力较弱的片段消去存在量词（如不能消去辖域内涵谓词的存在量词等），导致无法对一大类计算复杂度高的问题进行求解。本项目成果属于应用基础研究，针对现有研究局限，研究在有限结构下通过引入新的辅助谓词，或者在允许序且不引入新的辅助谓词的情况下，消去所有存在量词的方法；以及面向特定领域特殊片段下的高效存在量词消去算法；将已有的析取逻辑程序求解器作为黑盒调用，可以实现稳定模型下一阶逻辑理论求解器，并将此求解器应用于对服务组合和服务特征交互问题进行检测与诊断。在应用研究上，(1) 本成果可以将面向SOA程序诊断问题描述为基于值的溯因诊断模型（动态分片），并针对求解subset minimal溯因诊断问题，通过简化求解过程实现优化求解。(2) 将已有的析取逻辑程序求解器作为黑盒调用，可以实现稳定模型下一阶逻辑理论求解器和特殊片段的优化求解器，应用此求解器对SOA架构下的服务描述、组合、匹配与选择转化为基于值的溯因诊断模型，可以对服务组合和服务特征交互问题进行检测与诊断。