Production rules are a fundamental computational paradigm in artificial intelligence, perhaps being best known as the basis for expert systems. However, to this point there has been little formal study of their properties as a method of deduction. In this paper we initiate such a study by presenting a rewrite semantics for production rule systems. Such a formalization is both interesting per se as a paradigm for deduction and also useful in providing a formal framework for analyzing properties of production rule systems. We show how to represent production rules as rewrite rules operating on collections of atoms, thereby allowing us to import techniques from equational reasoning (confluence checking and completion, critical pair criteria, termination orderings, etc.). An interesting feature of this representation is the use of symbolic constraints to represent the negation-as-failure interpretation of negative conditions in production rules. Practical applications of this theory provide for the development of a comprehensive environment for verifying and validating the correctness of production rule systems, as well as the development of convergent production rule systems for special applications such as parallel evaluation and real-time control.