命题与模态逻辑的扩展规则推理与混合推理方法研究

Compared with the existing reasoning methods, new kinds of reasoning methods will be popular because of their performance advantages and usability when processing practical problems. As a kind of new reasoning methods proposed in 2003, extension rule-based reasoning methods have been acknowledged by domestic and foreign researchers. This project will focus on extension rule-based and hybrid reasoning methods in propositional and modal logics. The research contexts mainly include: 1) to improve reasoning ability and solving efficiency of extension rule-based reasoning methods by means of heuristic functions, selection functions and incremental solving techniques, etc. 2) to analyze adaptability of extension rule-based reasoning methods and resolution methods with regard to different problem benchmark domains; to design knowledge compilation strategies for corresponding knowledge bases; to design and implement extension rule-based hybrid reasoning methods with stronger reasoning abilities combined with resolution rules, tableaux and knowledge compilation techniques, etc. 3) to design and implement sound and complete extension rule-based reasoning methods in modal logics with destructive rules, semantic translation, semantic-syntactic mixed translation and knowledge compilation techniques, etc. 4) to infer and demonstrate the properties of the above reasoning methods, and propose an ideal and tradeoff reasoning framework which can consider all required characteristics adequately. The above research will promote robustness and availability of extension rule-based and hybrid reasoning methods, and also be uesd to mine reasoning methods' performance advantages and usability. Furthermore, it will provide theoretical foundations for related applications and popularization.

相对于现有推理方法，新型推理方法的性能优势与适用性，是其在现实问题处理中得以应用与推广的基础。扩展规则推理方法是2003年提出的一类新型推理方法，得到了国内外同行的认可。本课题将深入研究命题与模态逻辑的扩展规则推理与混合推理方法，主要包括：1）利用启发函数、选择函数和增量求解等提高扩展规则推理方法的推理能力和求解效率；2）分析扩展规则与归结方法对于不同问题域的适应性，构建相应的知识编译策略，结合扩展规则、归结、表推演和知识编译等设计并实现推理能力较强的混合推理方法；3）利用破坏性规则、语义转换、语义语法混合转换和知识编译等设计并实现可靠完全的模态逻辑扩展规则推理方法；4）推断和证明各类方法满足的特性，提出兼顾所需特性的较为理想的折中方案。上述研究将有助于提高扩展规则推理和混合推理方法的健壮性和可用性，更好地挖掘扩展规则推理的性能优势和适用性，为其在相关领域的应用与推广奠定理论基础。

相对于现有推理方法，新型推理方法的性能优势与适用性，是其在现实问题处理中得以应用与推广的基础。扩展规则推理方法是2003年提出的一类新型推理方法，得到了国内外同行的认可。本课题组针对命题和模态逻辑的扩展规则推理方法做了较为深入、细致的研究，并取得了较为满意的成果，主要包括：.1）深入研究了命题逻辑中已有的完备推理方法和不完备推理方法，结合扩展规则方法的特点，设计并实现了新的完备扩展规则推理方法和不完备扩展规则推理方法，极大地提高了扩展规则在命题逻辑中的推理效率。.2）对比分析了现有EPCCL理论编译算法的优势与不足，充分挖掘子句集的结构信息以及子句间的关联关系，设计了有效的编译加速策略，并基于超扩展规则提出了三种新的基于不同编译框架的EPCCL理论编译算法，提高了EPCCL理论的编译质量和编译效率。.3）基于超扩展规则设计了EPCCL理论的并行求交合并操作和并行求并合并操作，基于此实现了IKCHER和UKCHER编译算法的并行化，提高了该两种编译算法的效率，验证了并行知识编译的可行性。.4）深入研究了扩展规则推理方法的特性，设计了基于扩展规则推理算法的冗余性判定算法，并提出了用于加速判定过程的有效启发式策略和冗余性判定算法的并行化策略，进一步提高了基于扩展规则推理方法的冗余性判定算法的效率。.5）深入研究了模态逻辑S5公理系统的特性，结合扩展规则推理方法的特点，设计了命题模态逻辑推理算法，同时将模态逻辑中的Tableau方法推广到模糊命题模态逻辑中。.上述研究提高了扩展规则推理方法的健壮性和可用性，更好地挖掘了扩展规则推理的性能优势和适用性，并成功地将其应用到知识冗余性判定、知识约简等领域中，达到了扩展规则推理方法研究领域的领先水平，进一步推动了命题逻辑和模态逻辑扩展规则推理方法研究的发展。