Hmm. The article says it's not really an algorithm, because one of the steps requires checking if an expression is equivalent to zero, a problem that isn't today known to be decidable. Anyone here knowledgeable enough to supply details?

Edit: found the details in amichail's link. Yes, it's true; the algorithm isn't complete as of today.