  Inductive and coinductive specifications are widely used in formalizing
computational systems. Such specifications have a natural rendition in logics
that support fixed-point definitions. Another useful formalization device is
that of recursive specifications. These specifications are not directly
complemented by fixed-point reasoning techniques and, correspondingly, do not
have to satisfy strong monotonicity restrictions. We show how to incorporate a
rewriting capability into logics of fixed-point definitions towards
additionally supporting recursive specifications. In particular, we describe a
natural deduction calculus that adds a form of "closed-world" equality - a key
ingredient to supporting fixed-point definitions - to deduction modulo, a
framework for extending a logic with a rewriting layer operating on formulas.
We show that our calculus enjoys strong normalizability when the rewrite system
satisfies general properties and we demonstrate its usefulness in specifying
and reasoning about syntax-based descriptions. The integration of closed-world
equality into deduction modulo leads us to reconfigure the elimination
principle for this form of equality in a way that, for the first time, resolves
issues regarding the stability of finite proofs under reduction.
