Abstract:Deductive reasoning is an important method in formal verification, which can address programs in infinite state systems. In this paper, a proof system is studied and implemented, where infinite proof trees transform into finite ones. Firstly, a saturation algorithm is implemented based on iterative convergence, and the completion of the saturated system is implemented using Full Permutation Algorithm; Secondly, an optimization of proof search is carried out by inductive method; At last, the proof tree is visualized in 3D space using visualization technology.