Narrowing Approximations as an Optimization for Equational Logic Programs

Abstract. Solving equations in equational theories is a relevant programming paradigm which integrates logic and equational programming into one unified framework. Efficient methods based on narrowing strategies to solve systems of equations have been devised. In this paper, we formulate a narrowing-based equation solving calculus which makes use of a top-down abstract interpretation strategy to control the branching of the search tree. We define a refined, but still complete, equation solving procedure which allows us to reduce the branching factor. Our main idea consists of building an abstract narrower for equational theories and executing the set of equations to be solved in the approximated narrower. We define a generic technique of loop detection to ensure termination of our method. We prove that the set of answers computed by ract narrower has the property that each concrete solution of the set of equations is an instance of one of the substitutions in the answer set. Thus w...

• Type: Conference
• Year: 1993
• Where: PLILP
• Authors: María Alpuente, Moreno Falaschi, María José Ramis, Germán Vidal
• Keywords: Automated Reasoning, Equation Solving, Equational Theories, Equations, PLILP 1993