We present a simple neural model that given a formula and a property tries to answer the question whether the formula has the given property, for example whether a propositional formula is always true. The structure of the formula is captured by a feedforward neural network recursively built for the given formula in a top-down manner. The results of this network are then processed by two recurrent neural networks. One of the interesting aspects of our model is how propositional atoms are treated. For example, the model is insensitive to their names, it only matters whether they are the same or distinct.
A top-down approach how to recursively represent propositional formulae by neural networks is presented. This paper provides a new neural-net model of logical formulae that gathers information about a given formula by traversing its parse tree top-down. The paper pursues the path of a tree-structured network isomorphic to the parse tree of a propositional-calculus formula, but by passing information top-down rather than bottom-up.