Algebraic data type - rewrite system Let's define the integer ADT.

It has, as generators, the constant 0 (a generator) and the succ operation.
Moreover, it also contains the add operation defined by the (usual) axioms


  add (0, x) = x (where x is a variable of type integer)
  add (succ(x), y) = succ(add(x,y)).


Let's assume that I have two terms: add(x, succ(succ(succ(succ(0))))) and succ(succ(succ(succ(succ(succ(0)))))).

Is there an algorithm that finds all the substitutions allowing the first term to be rewritten to the second term?

Thanks in advance,
Ayroles
You could encode these into Horn Clauses (= Prolog) and use resolution (= Prolog's implementation technique).

More explicitly, your Prolog code file will look like the following:

add( 0,    N, N ).
add( succ(N), M, succ(Sum) ) :- add( N, M, Sum ).


Asking the following query at the command prompt in a prolog interpreter will give you an answer for X:

add( X, succ(succ(succ(succ(0)))), succ(succ(succ(succ(succ(succ(0))))))).


Which is:

X = succ(succ(0)) .


Using tracing within the Prolog interpreter will give you the series of substitutions used.

Fill all the gaps in yourself, and you will learn a lot.