Algebraic data type - rewrite system
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.