A perceptron network theorem prover for the propositional calculus

Abstract

In this paper a short introduction to neural networks and a design for a perceptron network theorem prover for the propositional calculus are presented. The theorem prover is a representation of a variant of the semantic tableau method, called the parallel tableau method, by a network of perceptrons. The parallel tableau method is designed to enable determination of the counter-examples of a formula (if any) concurrently. It is proven that the parallel method is complete, and that the operation of a network of perceptions that represents the parallel tableau method is as specified in virtue of the parallel tableau method. The states of all neurons in the network are updated simultaneously. An updated neuron reflects the outcome of a comparison of a weighted sum over the states of the neurons a neuron is connected with, and a threshold value. A network representing a theorem prover that can evaluate the validity of formulas with a maximum length of n atom occurrences, will do so in 2n +3 updates of al( neurons of such a network. The size of the network grows exponentially with increasing n. This is thought to be of limited importance, because it does not seem very probable that the validity of very long formulas will have to be evaluated.