A *signature* in rewriting logic is an equational
theory^{42} *(Sigma,E)*, where
*Sigma* is an equational signature and *E* is a set of *Sigma*-equations.
Rewriting will operate on equivalence classes of terms modulo *E*. In this
way, we free rewriting from the syntactic constraints of a term representation
and gain a much greater flexibility in deciding what counts as a *data
structure*; for example, string rewriting is obtained by imposing an
associativity axiom, and multiset rewriting by imposing associativity and
commutativity. Of course, standard term rewriting is obtained as the
particular case in which the set of equations *E* is empty. Techniques for
rewriting modulo equations have been studied extensively
[17] and can be used to implement rewriting modulo many
equational theories of interest. This is precisely what Maude does, using the
equational attributes given in operator declarations--such as associativity,
commutativity, identity, and idempotency--to rewrite modulo such axioms.

Given a signature *(Sigma,E)*, *sentences* of rewriting logic are
sequents of the form

where[t]_{E}--> [t']_{E},

Given a rewrite theory *R*, we say that *R* *entails* a
sentence *[t] --> [t']*, or that *[t] --> [t']* is a
*(concurrent) R-rewrite*, and write

**Reflexivity**. For each*[t]***e***T*,_{Sigma,E}(X)

.[t] --> [t] **Congruence**. For each*f***e***Sigma*,_{n}*n***e****N**

.[t _{1}] --> [t'_{1}] ... [t_{n}] --> [t'_{n}][f(t _{1},...,t_{n})] --> [f(t'_{1},...,t'_{n})]**Replacement**. For each rule*r: [t(x*in_{1},...,x_{n})] --> [t'(x_{1},...,x_{n})]*R*,

.[w _{1}] --> [w'_{1}] ... [w_{n}] --> [w'_{n}][t( | |**¯**w**¯***/*||**¯**x**¯***)] --> [t'(*||**¯**w'**¯***/*||**¯**x**¯***)]***Transitivity**

.[t _{1}] --> [t_{2}] [t_{2}] --> [t_{3}][t _{1}] --> [t_{3}]

Rewriting logic is a logic for reasoning correctly about *concurrent
systems* having *states*, and evolving by means of *transitions*.
The signature of a rewrite theory describes a particular structure for the
states of a system--e.g., multiset, binary tree, etc.--so that its states can
be distributed according to such a structure. The rewrite rules in the theory
describe which *elementary local transitions* are possible in the
distributed state by concurrent local transformations. The rules of rewriting
logic allow us to reason correctly about which *general* concurrent
transitions are possible in a system satisfying such a description. Thus,
computationally, each rewriting step is a parallel local transition in a
concurrent system.

Alternatively, however, we can adopt a logical viewpoint instead, and regard
the rules of rewriting logic as *metarules* for correct deduction in a
*logical system*. Logically, each rewriting step is a logical *entailment* in a formal system.

The computational and the logical viewpoints under which rewriting logic can be interpreted can be summarized in the following diagram of correspondences:

State<-> Term<-> PropositionTransition<-> Rewriting<-> DeductionDistributed Structure<-> Algebraic Structure<-> Propositional Structure

The last row of equivalences is actually quite important. Roughly speaking, it
expresses the fact that a state can be transformed in a concurrent way only if
it is nonatomic, that is, if it is *composed* out of smaller state
components that can be changed independently. In rewriting logic this
composition of a concurrent state is formalized by the *operations* of
the signature *Sigma* of the rewrite theory *R* that axiomatizes the
system. From the logical point of view such operations can naturally be
regarded as user-definable *propositional connectives* stating the
particular structure that a given state has. A subtle additional point about
the last row of equivalences is that the algebraic structure of a system also
involves *equations*. Such equations describe the system's global state
as a *concurrent data structure*; they can have a dramatic impact on the
amount of concurrency available in a system.

Note that it follows from this discussion that rewriting logic is primarily a
logic *of* change--in which the deduction directly corresponds to the
change--as opposed to a logic to talk *about* change in a more indirect
and global manner such as the different variants of modal and temporal logic.