# Algebraic data type - rewrite system

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)

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?

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( 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.

The answer to your question is yes. Unification modulo an ACU (associative, commutative, unital) operator is decidable. See Baader and Snyder's chapter "Unification Theory" in the Handbook of Automated Reasoning.