Equational rules for rewriting logic

In addition to equations and rules, we introduce equational rules that are oriented while having an equational interpretation. Correspondence between operational behavior and intended semantics is guaranteed by a property of coherence, which can be checked by examination of critical pairs and linearity conditions. We present applications of this theory to three examples where the rewrite relation is interpreted, respectively, as equality, transition and deduction.