Combining Rewrite Tools for Equational Logic Programming

Introducing equality into standard Horn clauses leads to a programming paradigm known as Equational Logic Programming. We propose here a scheme for the evaluation of such equational logic programs combining two powerful operational techniques : directed narrowing for the equational part and linear completion for the logical part. Thus we provide a goal-oriented solving procedure, keeping the well-known advantages of Linear Completion (a reduced search space with a loop avoiding effect and the possibility to finitely synthesize an infinite set of answers) and of Directed Narrowing (search space pruning). 1 Introduction The combination of logic and functional programming arouse much interest since the beginning of the last decade and different techniques have been proposed to merge these two features (see [4] for a survey). Equations allow to represent functional programs while Horn clauses are suited for logic programs. The mix of these two formalisms leads to a language known as Equat..