A kind of resolution based on fuzzy neural network

The resolution principle that is included in theorem proving is a single rule of inference for a test of unsatisfiability. It is based on conjunctive normal form (in short CNF), also called the clause set. Many modified resolution methods have been raised. Generally, for every resolution method, a time-consuming problem or "combination explosion" is involved in the processing of resolution. That is, if there is a great many clauses in the clause set, then the number of new clauses, which are obtained by resolution, is exponential. For this reason, even a good resolution method probably cannot be used in the application. Many applications have proved that fuzzy neural networks have the advantage of the expression of human language, learning and parallel computing. The paper tries to use the fuzzy neural network (FNN) to implement the resolution of propositional calculus. The paper mainly contains: (1) A "numerals system" is constructed, and proved there is an isomorphism between the numerals system and propositional calculus. Some conclusion about resolution in the numerals system is given. (2) The clause set is transformed into a fuzzy neural network. (3) The construction of the neural network is explained, and the learning algorithm of the neural network is given. (4) The soundness theorem and completeness theorem of the learning algorithm is proved.