CafeOBJ is a term rewriting system which is based on equational logic. Using CafeOBJ, this report aims to study the possibility of realization of the method of M. Finger and D. Gabbay [see D. M. Gabbay, I. Hodkinson and M. Reynolds, Temporal logic. Vol. 1. Mathematical foundations and computational aspects (Oxford Logic Guides 28) (Clarendon Press, Oxford) (1994; Zbl 0921.03023), Chapter 14: Adding a temporal dimension to a logic system], and gives a concrete automated theorem-prover for some modal logics (S4 and S5). We will adopt the Beth tableau proof as the basis of the automated theorem-prover.