Goal—directed equation solving
Nachum Dershowitz, G. Sivakumar · National Conference on Artificial Intelligence · 1988
Solving equations in equational Horn-clause theories is a programming paradigm that combines logic programming and functional programming in a clean manner. Languages like EQLOG, SLOG and RITE, express programs as rewrite rules and use narrowing to solve goals expressed as equations. In this paper, we express equational goal solving by means of a logic program that simulates rewriting of terms. Our goal-directed equation solving procedure is based on directed goals, and combines narrowing with a more top-down approach. We also show how to incorporate a notion of operator derivability to prune some useless paths, while maintaining completeness of the method.