Automated Reasoning and Equation Solving with the Characteristic Set Method

A brief introduction to the characteristic set method is given forsolving algebraic equation systems and then the method is extended toalgebraic difference systems. The method can be used to decompose thezero set for a difference polynomial set in general form to the union ofdifference polynomial sets in triangular form. Based on thecharacteristic set method, a decision procedure for the first ordertheory over an algebraically closed field and a procedure to provecertain difference identities are proposed.