The Design And Implementation Of Nonrevision Reasoning System For Horn Clausal Beliefs

How to deal with inconsistencies between beliefs in the achieving common sense reasoning process is a key issue. Currently, belief revision, one of the methods that handle the inconsistent belief problems, has been widely studied between domestic and foreign scholars. This approach adjusted the information into the existing knowledge base by introducing a revision operator to obtain the consistent belief knowledge. However, some useful information may be lost during the revision process, and may be difficult to make a conclusion. While belief non-revision method can get consistent extension by limiting the reasoning process without changing the knowledge base, it can achieve an effective reasoning.In the first-order logic, the extension of the Horn clause-formed assumption has been proven to have several good mathematical properties. However, According to the current study, there are still some problems for reasoning and program on the computer. In order to applying the non-revision method in practical way easily, and after the analysis of the current study, we summarize several critical problems to be solved when constructing a belief non-revision reasoning system. This paper makes the following research:(1) The extension of the Horn clause-formed assumption is defined. This definition makes the extension of the assumption that consist of a limited number of Horn clause remain a finite set and hold that to be logically equivalence with the existing extension. And this property is proved. Because the credibility of belief needs to be portrayed, the concept of weights needs to be introduced in this article. By weight not only meet the rationality, but also meet the implementation.(2) The algorithm for computing extension of a given assumption is designed. The algorithm is based on the algorithm for computing prime implicates of a clause, and is also based on the deletion strategy and order resolution to confirm the feasibility of optimization. To make it easier to get a consistent extension of assumption, define derivation explained and built a clause graph to record of the detailed reasoning process between beliefs.(3) This paper proposes a model of the Horn clause-formed belief non-revision reasoning system, and gives an implementation. For problem description and design of each module, implement the model of Horn clause-formed belief non-revision reasoning system.Then we implement the functions of all modules by means of Java GUI. The experiment takes multiple assumptions as test cases and verified that the reasoning algorithm is correct and reliable. In terms of system interpretability, it gets a good performance.