This project proposes to use matrix formalism for the verification of rule-based systems. The matrix operation is one of the mathematical foundations of Petri Nets. This approach is different from directed hypergraphs and Predicate/Transition net (Pr/T net) in rule-based systems verification. The errors in rule-based systems fall into two parts. One is the syntactic error; the other one is the semantic error. This project will focus on semantic errors. Typical semantic errors in a rule-based system consist of four types. They are redundancy, inconsistency, circularity, and incompleteness. This project presents a tool implemented in JAVA to verify these semantic errors. The program consists of the following phases. First, the program will normalize the rules into Horn clauses and rearrange these normalized rules. Then, it will transform these rules into matrix form and the verify matrix to find semantic errors. This paper also describes how to build a diagnosis system and use a verification tool to verify the rule base. This diagnosis system will diagnose liver diseases using Chinese Traditional Medicine (CTM). In this paper, chapter one outlines the general concepts of expert systems. Chapter two describes the knowledge base verification. Chapter three discusses more details about semantic errors. The different approaches to verify rule-based systems are described in chapter four. Chapter five describes the matrix approach for rule-based systems. Illustrations are shown in Chapter six. Finally, Chapter seven gives the conclusion.