Z3 and similar tools use a combination of canonicalization followed by brute force search. The canonicalization uses techniques similar to what the OP describes. (+ a (+ b c)) and (+ c (+ b a)) are both rewritten as (+ a b c). These rewrites rely on pattern matching.

At this point, if the query is syntactically solvable, we are done. Often queries are not, so the solver uses a symbolic decision procedure. The specific decision procedure depends on the formula. For example, Linear Integer Arithmetic (which allows addition of variables and multiplication by only constants) can be solved using Simplex.

Solving the problem of "recognizing when two arithmetic expressions are equivalent" is indeed ideal for an approach like Prolog or a SAT/SMT solver. In fact SMTLIB2 has a standardized expression for asserting if two expressions are identical. Conversely, many APIs make testing that sort of claim easy (and even emjoy tactics for things like synthesize new expressions w/ respect to some 'cost' function for each sub-expression, etc)

With that said, the author of this article seems to be interested in some sort of other question entirely.

I think the difficulty is in defining the relation, rather than proving it. The problems are so small that it probably doesn't matter how you actually prove equivalence, once you've defined it.

It might be useful to find solutions in the first place. This article was about defining when two expressions are "essentially the same", though, and Z3 isn't going to help you construct a definition :-).

This isn't really an interesting question from the point of view of automated reasoning. The obvious canonical form for such an expression (with variables) is to represent it as a polynomial or rational polynomial, and I don't see why you'd ever do something like what the author of this blog post is doing.