Logic as Energy: A SAT-Based Approach

This paper presents the implementation of ARQ-PROP II, a limited-depth propositional reasoner, via the compilation of its specification into an exact formulation using the satyrus platform. satyrus’ compiler takes as input the definition of a problem as a set of pseudoBoolean constraints and produces, as output, the Energy function of a higher-order artificial neural network. This way, satisfiability of a formula can be associated to global optima. In the case of ARQ-PROP II, global optima is associated to Resolution-based refutation, in such a way that allows for simplified abduction and prediction to be unified with deduction. Besides experimental results on deduction with ARQ-PROP II, this work also corrects the mapping of satisfiability into Energy minima originally proposed by Gadi Pinkas. Key words: ARQ-PROP II, higher-order neural networks, propositional reasoner, satisfiability, satyrus.

• Type: Conference
• Year: 2007
• Where: BVAI
• Authors: Priscila Machado Vieira Lima, M. Mariela Morveli-Espinoza, Felipe M. G. França
• Keywords: ARQ-PROP II, Artificial Intelligence, BVAI 2007, Global Optima, Propositional Reasoner