Logic as Energy: a SAT-based Approach
PMV Lima, MMM Morveli-Espinoza… - Advances in Brain, Vision …, 2007 - Springer
Advances in Brain, Vision, and Artificial Intelligence: Second International …, 2007•Springer
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 sat yrus
platform. sat yrus' compiler takes as input the definition of a problem as a set of pseudo-
Boolean constraints and produces, as output, the Energy function of a higher-order artificial
neural network. This way, sat isfiability 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 …
reasoner, via the compilation of its specification into an exact formulation using the sat yrus
platform. sat yrus' compiler takes as input the definition of a problem as a set of pseudo-
Boolean constraints and produces, as output, the Energy function of a higher-order artificial
neural network. This way, sat isfiability 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 …
Abstract
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 pseudo-Boolean 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.
Springer