An implementation of a theorem prover in symmetric neural networks

Pinkas defined (1991, 1992) a bi-directional mapping between propositional logic formulas and energy functions of symmetric neural networks. He showed that determining whether a propositional logic formula is satisfiable is equivalent to finding whether the global minimum of its associated energy function is equal to zero. He also defined how to transform a first-order resolution-based theorem proof of a formula (query Q) from a given set of formulas (knowledge base KB) into a set of constraints described by a set of propositional logic formulas C. Then he showed that the satisfaction of C is sound and complete with respect to a first-order resolution-based proof of Q from KB. Therefore finding that the global minimum of the energy function associated to C is equal to zero is sound and complete with respect to a first-order resolution-based proof of Q from KB. The proof itself could be extracted from the state of the neurons when the network stops in the global minimum. Pinkas did not implement his system. In this work we point out some adjustments to C and we present an implementation of the revised system. We also show some experimental results and point out some future works