基于分离的局部信念修正研究及其软件诊断应用

Belief revision is one of the most important research areas in Artificial Intelligence, Databases and Philosophical Logic. Developing highly effective and efficient algorithms for belief revision operations is a key issue in the research of belief revision and its applications. One of the most efficient approach to reduce computational complexity of belief revision operations is computational localisation. In recent years, the techniques of splitting-based localisation have received considerable attention from the researchers in Artificial Intelligence. Through a process of finest splitting on propositional formulas, irrelevant atoms in a belief set can be effectively separated from the belief set. As a consequence, the computation of belief revision operations can be localised. This approach has been successfully applied to other domains of knowledge base maintenance. This project aims to develop a systematic theory of computational localisation in first-order logic. We will first establish a theory of splitting in Horn belief revision based on the finest splitting technique on Horn clauses. We then extend the theory to the first-order Horn logic. We will investigate the existence and uniqueness of finest splitting on first-order formulas and develop algorithms to calculate the finest splitting of first-order formulas with specific syntax. Based on the research outcomes, we will introduce as the first time the language splitting techniques into Reiter's theory of software diagnosis in order to implement computational localisation of diagnosis reasoning. Such an approach may effectively reduce the possibility of widely-existed combinatorial exposure in diagnosis reasoning, and therefore provides a new solution to the computational problem in Reiter's first-order diagnosis theory.

信念修正是人工智能、数据库理论以及哲学逻辑研究的热点问题。寻找高速有效的算法一直是信念修正研究及其应用的重点。降低信念修正计算复杂性的最有效的方法之一是将计算问题局部化。近年来，基于分离的局部化技术受到研究者们高度重视。通过对命题公式的最细划分, 信念集中非相关原子可被有效的分离出去，从而实现信念修正操作的局部化。该方法亦成功应用于其它相关知识库维护领域。本项目从Horn子句集的最细分离出发，提出一整套基于Horn逻辑的局部信念修正理论,进而将这一理论从命题逻辑推广到一阶Horn逻辑，并探讨一阶逻辑公式集最细分离的存在唯一性，以及计算一阶逻辑及部分特殊公式集最细分离算法。基于这一系统化研究成果，将在Reiter诊断理论中引入基于分离的局部化技术，以实现诊断推理的局部化，从而降低诊断推理过程中几乎无法避免的组合爆炸，以便为解决Reiter一阶诊断理论中的计算复杂性问题提供一种全新的解决途径。

本项目紧紧围绕信念修正局部化及应用这一主题，采用信念修正背景知识，从机器人知识库更新、协商的信念更新、协商策略推理、序贯协商、协商机制设计等方面展开研究，获取了一系列成果。主要工作概括如下：.（一）提出带两个优先算子（可表示博弈策略组合等性质）的模态逻辑，便于形式化表示策略和策略推理，该成果已发表在著名国际权威逻辑刊物《Journal of Philosophical Logic》上；.（二）提出基于回答集编程的序贯协商逻辑框架及推理机制设计，该成果分别发表在第12届国际逻辑程序与非单调推理会议和国际期刊《Frontiers of Computer Science》上；.（三）提出基于回答集逻辑程序的有限理性协商机制，并已开发一个系统实现该机制。