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.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy