We willintroducethe theory and classical algorithms in the mechanical proofs of combinatorial identities, among which the reduction based algorithms have gained the most attention. In this talk, we will also introduce the (q-)polynomial reduction and applications in the automatically proof of π-series and congruences.