A KIND OF RESOLUTION BASED ON NEURAL NETWORK

Resolution principle is a single rule of inference for a test of unsatisfiability. It is based on conjunctive normal form (in shortly CNF), also called as clause set (atomic formulae or their negations is called a literal, disjunction of literal is called a clause, conjunction of clause is consider as a clause set). Many modified resolution method have been raised, such as semantic resolution, ordered linear resolution, binary resolution, locking restriction resolution, the generalized resolution and fuzzy resolution, etc. They are based on this ideal: beginning with a clause, then use continually result of resolution, at last, get a conclusion of inference. If the conclusion is an empty clause, then the clause set is unsatisfiable; if the conclusion is not an empty clause, then the clause set is satisfiable. Soft computing is coined by Lotfi A. Zadeh. It includes fuzzy logic, neural network, evolution computing, etc. In general, the strong points of neural networks are their learning capabilities and their distributed structure that allows for highly parallel software or hardware implementations. Currently, soft computing is especially concerned with combinations of these methodologies. Such as fuzzy-neural network is the most visible approach to such combinations. It has the advantage of expression of human language, learning algorithms and parallel computing. In this paper, we will consider the following ideal: one hand, we discuss the classical resolution, and point out that a DNF equal a neural network (a DNF is transformed from a CNF by using distributive law of Ú to Ù). On the other hand, once a clause set S be transformed a neural network, we can construct algorithm, and implement resolution by using the neural network. 1