  Term rewriting is a Turing complete model of computation. When taught to
students of computer science, key properties of computation as well as
techniques to analyze programs on an abstract level are conveyed. This paper
gives a swift introduction to term rewriting and presents several automatic
tools to analyze term rewrite systems which were developed by the Computational
Logic Group at the University of Innsbruck. These include the termination tool
TTT2, the confluence prover CSI, the completion tools mkbTT and KBCV, the
complexity tool TcT, the strategy tool AutoStrat, as well as FORT, an
implementation of the decision procedure for the first-order theory for a
decidable class of rewrite systems. Besides its applications in research, this
software pool has also proved invaluable for teaching, e.g., in multiple
editions of the International Summer School on Rewriting.
