The Study Of Automated Resolution Reasoning Based On Model Of Petri Net

There is no denying that representation, reference and application of knowledge are key questions in artificial intelligence. In recent years, automated deduction based on non-classical logics, which speed up the development of artificial intelligence, has attracted many researcher's attention. In order to deal with inference of different information, people has proposed and developed many mathematical theories, methods and tools, such as theory of resolution, classical logic, fuzzy logic, lattice- valued logic, Rough logic, Petri net and so on. These theories and methods play an important role in providing support for automated deduction. This paper further develops these theories and method, studies resolution inference based on the Petri net, and achieves the following research results:1. The matrix representation of base clause set is presented and the method of simplification for matrix is discussed according to single literal rule and pure rule. Furthermore, based on T- invariant and the completeness of input resolution, unit resolution and supporting resolution, we give the definition of elementary transformation for matrix, discuss its properties, provide many methods of matrix inference and prove the completeness.2. Models of Petri net are given for base Horn clause set, general base clause set, and one-order Horn clause set. Then, based on the flowing rule of token in Petri net and theory of resolution, the canceling algorithms and their completeness are presented. After that, we have got important conclusions by comparing T-invariant algorithm with the canceling algorithm. For example, we have got the facts that the T-invariant algorithm is simple but has limited range for application, the process of inference is not visualized, and the canceling algorithm can be widely and efficiently applied with its visualized process and brief structure. All these results are efficient and helpful for the automated inference based on Petri net.3. We first provide the system of operator proposition logic. Then, λ -resolution and λ -resolved deduction are given. Also, their properties are discussed and...