Application Of Petri Nets In Predicate Logic Reasoning

Logical reasoning is the basis of artificial intelligence, the first-order predicate logic belonging to logic is a knowledge representation widely used, therefore,it is a meaningful task to study the reasoning problem of first-order predicate logic. On the basis of the former study,it is the jumping-off place of our study in the thesis to seek new methods for first-order predicate logical reasoning and to open up a whole new world in first-order predicate logical reasoning of artificial intelligence by predicate/transition(Pr/T) net of Petri nets. The major contributions of this dissertation are as follows:1) A direct modeling method for first-order predicate expression is presented in the thesis directing at the present modeling methods that are inconvenient to carried out by a computer and whose modeling processes have uncertainties and many possibilities. The introduced method can model directly for any first-order predicate expression which is removed quantifiers only. The modeling process is more shorter and clearer and the method overcomes the shortcomings of prior methods.2) A method that can reduce the Pr/T net system of first-order predicate expression is presented,by this method,we can, delete the transitions worthless to reasoning before we reason or prove first-order predicate logic by Pr/T net system in order to speed up the reasoning or proving process.3) A method that can construct directly the incidence matrix of first-order predicate expression is presented,the middle process constructing the Pr/T net system of first-order predicate expression is omitted.4) A sufficient condition for two first-order predicate expressions to be equivalent is found and then an algorithm that can partly judge the equivalence between two first-order predicate expressions is presented in the thesis. In addition, for a class of first-order predicate expression namely first-order predicate expression without free variable and with one quantifier, a necessary and sufficient condition for such first-order predicate expressions to be equivalent and a corresponding judging algorithm are come up with.5) Two graphical methods used in first-order predicate logical reasoning,that is goal-guiding graphical reasoning method and transition frame graphical reasoning method,are presented.6) By dint of the incidence matrix of Pr/T net system,a method called incidence matrix elementary transformation method is presented for first-order predicate logical reasoning.7) In the thesis,the two graphical methods and the incidence matrix elementary transformation method introduced are not only used in proving the correctness of reasoning result of first-order predicate logic,but also used in extracting answers of practical questions and seeking feasible schemes of goal realizing,thus we can extend the utilization of these reasoning methods.