Technical Report Number
This chapter considers the problems of expressing logic and constructing proofs in fault tolerant connectionist networks that are based on energy minimalism. Given a first-order-logic knowledge base and a bound k, a symmetric network is constructed (like a Boltzman machine or a Hopfield network) that searches for a proof for a given query. If a resolution-based proof of length no longer than k exists, then the global minima of the energy function that is associated with the network represent such proofs. If no proof exist then the global minima indicate the lack of a proof. The network that is generated is of size polynomial in the bound k and the knowledge size. There are no restrictions on the type of logic formulas that can be represented. Most of the chapter discusses the representation of propositional formulas and proofs; however, an extension is presented that allows the representation of unrestricted first-order logic formulas (predicate calculus). Fault tolerance is obtained using a binding technique that dynamically assigns symbolic roles to winner takes all units.
Pinkas, Gadi, "A Fault Tolerant Connectionist Architecture for Construction of Logic Proofs" Report Number: WUCS-93-10 (1993). All Computer Science and Engineering Research.