Abstract:INCAPS (INteractive Computer-Aided Proving System) is a proof system of temporal logic. This paper outlines its proof strategies (tactics, tacticals) variety and structure. The kernel of it is to discuss the validity of tactics and tacticals. After introducing several new concepts: proof strategies level number, function tree and B function defined on it, we show that INCAPS proof strategies are valid.