This chapter introduces term rewriting and some of its applications from different points of view. Rewriting is first presented as an abstract relation on a set, and properties of such relations, mainly confluence and well-foundedness, are introduced. A more concrete notion of rewriting is then defined on first-order terms. Several examples of rewriting relations on terms or equivalence classes of terms are given, including rewriting modulo axioms and conditional rewriting. The rewriting logic is defined and is shown to be especially suited to describing concurrent computations. It also provides a logical framework in which other logics can be represented, and a semantic framework for the specification of languages and systems. The rest of the chapter is concerned with applications of rewriting to proofs of various program properties. It first addresses the issue of automatically building, for an equational theory, an equivalent convergent rewrite system, when one exists. This is solved via a completion process that turns equalities into rewrite rules, computes new derived equalities and reduces them. Several generalisations of this completion mechanism, based on superposition and simplification, are also surveyed. Then the completion technique is generalised in the context of order-sorted equational specifications. There, rewriting is used not only to evaluate but also to compute the types of terms during evaluation. Eventually, in the context of many-sorted conditional specifications, rewrite techniques are used to prove inductive properties in the initial model and completeness of function definitions.