扩展规则推理方法研究

归结方法和表推演方法是自动推理领域最著名、应用最广泛的两种方法。我们新提出的扩展规则方法，被国际上著名的自动推理专家Davis称为与归结"互补"的推理方法；我们建立的基于扩展规则的知识编译方法得到了NC归结的提出人Murray教授的高度评价。本课题申请将深入研究一阶逻辑、模态逻辑和多值逻辑的扩展规则推理方法和知识编译方法，完善高效的基于扩展规则的推理算法；同时探索将扩展规则方法用于智能规划问题求解、安全协议验证和软件验证的模型检测理论和方法；设计实现基于扩展规则、归结规则和表推演的混合推理系统、规划求解器和模型检测器；以期获得在国际上有我们自己特色的、应用前景广阔的、成体系的自动推理理论、方法和技术。