Goal-Directed Equation Solving

Nachum Dershowitz, G. Sivakumar

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.