Abstract:Based on algebra and recursive function theory, a key concept of algebraicrecursive predicates is defined in this paper. Based on mathematical induction, a backwardreduction method and its corresponding algorithm reduction are given for proving the universal truth of algebraic recursive predicates. Because the method is reduction based, theefficiency of theorem-proving is improved greatly.