This paper investigates how to define and construct a Lyapunov function for Boolean networks, and presents a number of new results based on the semi-tensor product of matrices. A proper form of pseudo-Boolean functions is found, and the concept of (strict-)Lyapunov functions is thus given. It is shown that a pseudo-Boolean function in the proper form can play the role of Lyapunov functions for Boolean networks, based on which some Lyapunov-based stability results are obtained. Then, we study how to construct a Lyapunov function for Boolean networks, and propose a definition-based method. The study of illustrative examples shows that the new results/method presented in this paper work very well.