mu-term: Verify Termination Properties Automatically (System Description)

We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems. We follow a unified, logic-based approach to describe rewriting computations. The automatic generation of logical models for suitable first-order theories and formulas provides a common basis to implement the proofs.