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 SMT

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.