NARROWER: a new algorithm for unification and its application to logic programming. (English) Zbl 0576.68002

Rety, Pierre; Kirchner, Claude; Kirchner, Hélène; Lescanne, Pierre

Rewriting techniques and applications, 1st Int. Conf., Dijon/France 1985, Lect. Notes Comput. Sci. 202, 141-157 (1985).

Summary: [For the entire collection see Zbl 0568.00022.]
In this paper, an algorithm for solving equations in equational theories is proposed. Its correctness and its completeness are proved and an implementation called NARROWER is described. It is made by extending the software REVE. Some experiments are also presented. The algorithm and its implementation have the nice property that when the set of solutions is infinite, it can detect regularity and describes the solutions. We also try to show the connection of such an algorithm with the design of a logic programming language, the purpose of which is to solve equations.

MSC:

68N01	General topics in the theory of software
68Q65	Abstract data types; algebraic specification
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

algorithm for solving equations in equational theories; correctness; completeness

Citations:

Zbl 0568.00022

Software:

NARROWER; REVE