1 Introduction

mu-term is a tool that can be used to automatically verify termination properties of variants of Term Rewriting Systems (TRSs): termination and innermost termination of TRSs using the DP Framework for TRSs [10] (this framework is also used to prove termination of String Rewriting Systems); termination and innermost termination of context-sensitive rewriting [16, 17] using the Context-Sensitive DP Framework [2, 13]; termination of rewriting modulo associative/commutative theories using the A\(\vee \)C-DP Framework [4]; termination of order-sorted rewriting using the Order-Sorted DP Framework [22]; and operational termination of Conditional TRSs (CTRSs) using the 2D DP Framework [24, 25]. In this setting, describing different kinds of rewriting computations as proofs of goals \(s\rightarrow t\) and \(s\rightarrow ^*t\) with respect to an appropriate inference system is useful. Such an approach, exploiting the logic-based description of rewriting computations, involves the use of several techniques which have been recently investigated elsewhere: (i) the generation logical models and well-founded relations [19], (ii) modeling operational termination of CTRSs with conditional dependency pairs [23], (iii) the use of removal triples [24] generated by logical models [25], etc. Giving support to such techniques in termination proofs motivated the development of a new version of our tool, mu-term 6.0:

http://zenon.dsic.upv.es/muterm

We report on the new logic-based approach followed by mu-term 6.0, and also on the new features included since the last description of the system in 2010 [3].

2 New Features of mu-term

In the following, we enumerate the new features of mu-term 6.0 and illustrate them with some examples. Examples are intended to provide a better understanding of the techniques and often display solutions not necessarily obtained by an automatic proof with the tool, where the use of a specific proof strategy combining a sequence of several techniques (see Sect. 3) may dismiss the focused technique. Although we use some examples from other papers, all proofs of (operational) termination displayed here are new. For instance, the CTRS in Example 1 was proved operationally terminating in [25, Example 33], but the use of models in Example 3 below to show the absence of a link in the dependency graph is new. Examples 6 and 7 (of Order-Sorted TRSs) are discussed and proved here for the first time.

2.1 Logic-Based Representation of CTRSs

Given an oriented CTRS \(\mathcal{R}\), with rules \(\ell \rightarrow r\Leftarrow s_1\approx t_1,\ldots ,s_n\approx t_n\),Footnote 1 an inference system \(\mathcal{I}(\mathcal{R})\) is obtained from the following generic inference system \(\mathfrak {I}_{\text {CTRS}}\)

figure a

by specializing \((\text {C})_{f,i}\) for each k-ary symbol f in the signature \({\mathcal{F}}\) and \(1\le i\le k\), and \((\text {Rl})_\alpha \) for all conditional rules \(\alpha :\ell \rightarrow r\Leftarrow c\) in \(\mathcal{R}\). Rules \(\frac{B_1~\cdots ~B_n}{A}\) in \(\mathcal{I}(\mathcal{R})\) are schematic: they can be used under any instance \(\frac{\sigma (B_1)~\cdots ~\sigma (B_n)}{\sigma (A)}\) by a substitution \(\sigma \). We write \(s\rightarrow _\mathcal{R}t\) (\(s\rightarrow ^*_\mathcal{R}t\)) iff there is a proof tree for \(s\rightarrow t\) (\(s\rightarrow ^* t)\) using \(\mathcal{I}(\mathcal{R})\). Operational termination of \(\mathcal{R}\) is defined as the absence of infinite proof trees for goals \(s\rightarrow t\) and \(s\rightarrow ^*t\) in \(\mathcal{I}(\mathcal{R})\) [21]. In the analysis of computational properties of \(\mathcal{R}\), we use the first-order theory \(\overline{\mathcal{R}}\) obtained from \(\mathcal{I}(\mathcal{R})\) by translating the inference rules \((\rho )\frac{B_1~\cdots ~ B_n}{A}\) in \(\mathcal{I}(\mathcal{R})\) into sentences \(\overline{\rho }\) of the form \((\forall \mathbf {x})\,B_1\wedge \cdots \wedge B_n\Rightarrow A\), for \(\mathbf {x}\) the sequence of variables occurring in \(A,B_1,\ldots ,B_n\) [18, Sect. 4.5].

Example 1

For the following CTRS \(\mathcal{R}\) [27, Example 7.2.51]

$$\begin{aligned} \mathsf {h}(\mathsf {d})\rightarrow & {} \mathsf {c}(\mathsf {a})\end{aligned}$$
(1)
$$\begin{aligned} \mathsf {h}(\mathsf {d})\rightarrow & {} \mathsf {c}(\mathsf {b}) \end{aligned}$$
(2)
$$\begin{aligned} \mathsf {f}(\mathsf {k}(\mathsf {a}),\mathsf {k}(\mathsf {b}),x)\rightarrow & {} \mathsf {f}(x,x,x)\end{aligned}$$
(3)
$$\begin{aligned} \mathsf {g}(x)\rightarrow & {} \mathsf {k}(y) \Leftarrow \mathsf {h}(x) \approx \mathsf {d}, \mathsf {h}(x) \approx \mathsf {c}(y) \end{aligned}$$
(4)

the theory \(\overline{\mathcal{R}}\) is given in Fig. 1.

Fig. 1.
figure 1

First-order theory \(\overline{\mathcal{R}}\) for \(\mathcal{R}\) in Example 1 (all variables universally quantified)

Full size image

2.2 Operational Termination of Conditional Rewrite Systems

In [24, 25] a framework for automatically proving operational termination of (oriented) CTRSs using appropriate notions of dependency pairs (adapting the original notion for TRSs [5]) has been introduced: the 2D DP Framework.

Dependency Pairs for CTRSs. Given a CTRS \(\mathcal{R}\), two new CTRSs and are introduced to capture the two horizontal and vertical dimensions of operational termination of CTRSs [23]: the usual absence of infinite rewrite sequences (termination), and the absence of infinite ‘climbs’ on a proof tree when trying to prove a goal \(s\rightarrow t\) or \(s\rightarrow ^*t\) (called V-termination). consists of rules \(u\rightarrow v\Leftarrow c\) whose terms u and v capture the progress of infinite rewrite sequences involving rules \(\ell \rightarrow r\Leftarrow c\) with u and v marked versions of \(\ell \) and a subterm of r respectively (only the root symbol f is marked as \(f^\sharp \), or just capitalized: F). Similarly, consists of rules \(u\rightarrow v\Leftarrow d\) where v is a marked subterm of \(s_i\) for a condition \(s_i\approx t_i\) in c and d is \(s_1\approx t_1,\ldots ,s_{i-1}\approx t_{i-1}\).Footnote 2

Example 2

For \(\mathcal{R}\) in Example 1, we have and

As in [7, Sect. 5], we use a set of sorts \(S_{ DP }=\{{\textsc {s}},{\textsc {p}}\}\) so that symbols f are (automatically) given a rank \(f:{\textsc {s}}\cdots {\textsc {s}}\rightarrow {\textsc {s}}\) and marked symbols are given rank \(F:{\textsc {s}}\cdots {\textsc {s}}\rightarrow {\textsc {p}}\) [25, Sect. 4.3]. Variables of formulas in \(\overline{\mathcal{R}}\) (e.g., Fig. 1) are then assumed to be universally quantified on sort \({\textsc {s}}\).

The 2D DP Framework for CTRSs. The absence of infinite chains of 2D DPs (i.e., sequences of 2D DPs which model infinite branches in the proof trees for goals \(s\rightarrow t\) and \(s\rightarrow ^*t\)) characterizes operational termination of CTRSs [23]. This is proved using a divide-and-conquer strategy which successively decomposes operational termination problems into smaller and simpler ones. Processors \(\mathsf{P}\) are used for this purpose [24]. They simplify problems by decomposing or shrinking them. In particular, the appropriate estimation of graphs \(\mathcal{G}\) whose nodes are dependency pairs is useful to analyze the existence of such infinite chains as cycles in the graph. The absence of cycles implies operational termination. The presence of conditional rules and pairs introduces some particular issues which we enumerate, and discuss below.

  1. 1.

    Some pairs could be infeasible, i.e., unable to be used in any of the aforementioned chains. Then, we could remove them [24, Sect. 4]. Also, arcs in \(\mathcal{G}\) are defined by specific (often undecidable) sequences \(s_1\bowtie _1 t_1,\ldots ,s_n\bowtie _n t_n\) (called f-sequences [15]) where \(s_i\) and \(t_i\) are terms and \(\bowtie _i\) are predicates \(\rightarrow ^*_i\) that capture the possibility of having two nodes involved in a chain [20, Sect. 4.5] and must be proved feasible or infeasible (for some substitution \(\sigma \) which applies to terms \(s_i\) and \(t_i\)). A typical strategy is discarding arcs whose associated sequence is infeasible. We discuss this in paragraph Infeasibility in Termination Proofs below (see Examples 3 and 4).

  2. 2.

    Some pairs could be ‘harmless’, i.e., unable to be persistently used in any infinite chain. This can be shown if we prove a ‘decrease’ when such pairs are used in a chain. Again, we can remove them to obtain a simplification [25, Sect. 4.3]. We discuss this in paragraph Use of Well-Founded Relations below (see Example 5).

Infeasibility in Termination Proofs. Given a (C)TRS \(\mathcal{R}\) we say that a sequence \(s_1\rightarrow ^*t_1,\ldots ,s_n\rightarrow ^*t_n\) is \(\mathcal{R}\)-infeasible if there is no substitution \(\sigma \) such that \(\sigma (s_i)\rightarrow ^*_\mathcal{R}\sigma (t_i)\) holds for all \(1\le i\le n\). In [20] it is proved that a sequence \(s_1\rightarrow ^*t_1,\ldots ,s_n\rightarrow ^*t_n\) is \(\mathcal{R}\)-infeasible if there is a model of \(\overline{\mathcal{R}}\cup \{\lnot (\exists \mathbf {x})\,s_1\rightarrow ^*t_1,\ldots ,s_n\rightarrow ^*t_n\}\), where \(\mathbf {x}\) contains the variables in \(s_1,t_1,\ldots ,s_n,t_n\). In termination proofs, proving infeasibility is useful at different levels. As remarked above, when the conditional part c of a pair \(u\rightarrow v\Leftarrow c\) is proved infeasible, we can remove it. Also, the absence of an arc between two nodes (pairs) \(u\rightarrow v\Leftarrow c\) and \(u'\rightarrow v'\Leftarrow c'\) in the graph \(\mathcal{G}\) can be treated as the infeasibility of \(v\rightarrow ^*u'\) (where, as usual, we assume that v and \(u'\) share no variable). For instance, for \(\mathcal{R}\) in Example 1, it is possible to prove that there is no arc in the ‘horizontal’ graph which consists of a single node \(\mathsf {F}(\mathsf {k}(\mathsf {a}),\mathsf {k}(\mathsf {b}),x) \rightarrow \mathsf {F}(x,x,x)\) (the only dependency pair in ) by just finding a model of

$$\begin{aligned} \overline{\mathcal{R}}\cup \{\lnot (\exists x,y:{\textsc {s}})\,\mathsf {F}(x,x,x)\rightarrow ^*\mathsf {F}(\mathsf {k}(\mathsf {a}),\mathsf {k}(\mathsf {b}),y)\} \end{aligned}$$
(5)

For this purpose, model generators AGES [14] and Mace4 [26] are used by mu-term.

Example 3

We obtain a model \(\mathcal{A}\) of (5) with Mace4. The domain is \(\mathcal{A}=\{0,1\}\) (Mace4 does not support sorts; thus, both \({\textsc {s}}\) and \({\textsc {p}}\) are merged into a single sort). Function and predicate symbols are interpreted as follows:

Discarding the arc would not be possible by the usual unification-based technique in [9]. With regard to infeasibility of pairs, consider the following well-known example.

Example 4

Consider the following CTRS \(\mathcal{R}\) [8, p. 46]:

$$\begin{aligned} \mathsf {a}\rightarrow & {} \mathsf {b}\end{aligned}$$
(6)
$$\begin{aligned} \mathsf {f}(\mathsf {a})\rightarrow & {} \mathsf {b} \end{aligned}$$
(7)
$$\begin{aligned} \mathsf {g}(x)\rightarrow & {} \mathsf {g}(\mathsf {a}) \Leftarrow \mathsf {f}(x) \approx x \end{aligned}$$
(8)

where . Both pairs in are \(\mathcal{R}\)-infeasible: no substitution \(\sigma \) makes \(\sigma (\mathsf {f}(x))\rightarrow ^*\sigma (x)\) true. We can prove it if a model \(\mathcal{A}\) of \(\overline{\mathcal{R}}\cup \{\lnot (\exists x)\,\mathsf {f}(x)\rightarrow ^* x\}\) can be found. We obtain a model with AGES. The domain is \(\mathcal{A}=\mathbb {N}-\{0\}\) (since no marked symbol is involved, we can use a single interpretation domain); for function and predicate symbols:

We can safely remove both pairs. Thus no infinite chain of pairs in exists.

Use of Well-Founded Relations. The removal triple processor [24, Def. 70] implements the use of removal triples \((\gtrsim ,\succeq ,\sqsupset )\), including a well-founded relation \(\sqsupset \) to remove pairs from, and hence simplify, termination problems. For instance, as shown in [25, Sect. 4.3], \(\mathcal{R}\) in Example 1 is operationally terminating if we find a model \(\mathcal{A}\) of

$$\begin{aligned} \mathcal{S}^{ RT }_\mathcal{R}\cup \{(\forall x:{\textsc {s}})\, \mathsf {F}(\mathsf {k}(\mathsf {a}),\mathsf {k}(\mathsf {b}),x)\,\pi _\sqsupset \,\mathsf {F}(x,x,x)\} \end{aligned}$$
(9)

where \(\pi _\sqsupset \) (a new predicate symbol representing \(\sqsupset \)) is interpreted as a well-founded relation \(\pi _\sqsupset ^\mathcal{A}\), and \(\mathcal{S}^{ RT }_\mathcal{R}\) extends \(\overline{\mathcal{R}}\) with the following additional requirements to apply the processor [24, Definitions 68 and 69]:

$$\begin{aligned} (\forall x,y:{\textsc {p}})&x\,\pi _\gtrsim \,y \wedge y\,\pi _\sqsupset \,z \Rightarrow x\,\pi _\sqsupset \,z\end{aligned}$$
(10)
$$\begin{aligned} (\forall x,y:{\textsc {p}})&x\rightarrow y \Rightarrow x\,\pi _\gtrsim \,y \end{aligned}$$
(11)

No predicate \(\pi _\succeq \) is necessary in this example (where a single pair is considered).

Example 5

We obtain a model \(\mathcal{A}\) of (9) with AGES. Domains are \(\mathcal{A}_{\textsc {p}}=\{-1,0,1\}\) and \(\mathcal{A}_{\textsc {s}}=\{0,1\}\). With regard to function and predicate symbols:

where, as in the semantic approach in [25, Sect. 4.3], \(\rightarrow \) and \(\rightarrow ^*\) are overloaded for sorts \({\textsc {p}}\) and \({\textsc {s}}\); thus, \((\rightarrow )^\mathcal{A}_{\textsc {p}}\), \((\rightarrow ^*)^\mathcal{A}_{\textsc {p}}\), \((\rightarrow )^\mathcal{A}_{\textsc {s}}\), and \((\rightarrow ^*)^\mathcal{A}_{\textsc {s}}\) are the corresponding interpretations. Note that \(\pi _\sqsupset ^\mathcal{A}=\{(x,y)\mid x,y\in \mathcal{A}_{\textsc {p}},6x\ge 1+6y\}=\{(0,-1),(1,-1),(1,0)\}\) is well-founded on \(\mathcal{A}_{\textsc {p}}\). Thus, we conclude operational termination of \(\mathcal{R}\).

2.3 Termination of Order-Sorted Rewriting

Sorts are often used to reinforce program termination. Order-sorted dependency pairs were introduced in [22] for proving termination of order-sorted TRSs.

Example 6

The following many-sorted TRS \(\mathcal{R}\) in [29, Sect. 3.3] (in the hopefully self-explained Maude format [6]) is a terminating version of Toyama’s example, which is nonterminating as a TRS (i.e., without sort information):

figure b

The 2010 version of mu-term could not prove it terminating.Footnote 3 According to [22], \(\mathcal{R}\) has a single dependency pair:

$$\begin{aligned} \mathsf {F}(\mathsf {a},\mathsf {b},x) \rightarrow \mathsf {F}(x,x,x) \end{aligned}$$
(12)

where \(\mathsf {F}\) has rank \(\mathtt {S1}\; \mathtt {S1}\; \mathtt {S1} \rightarrow \mathtt {P}\) for a new sort \(\mathtt {P}\) [22, Sect. 3.2] and x has sort \( \mathtt {S1}\). We can prove that the dependency graph consisting of this single pair has no cycle. With AGES we can compute a model of \(\overline{\mathcal{R}}\cup \{\lnot (\exists x,y: \mathtt {S1})\,\mathsf {F}(x,x,x)\rightarrow ^*\mathsf {F}(\mathsf {a},\mathsf {b},y)\}\) which is as follows: \(\mathcal{A}_{\mathtt {S1}}=\{0,1\}\), \(\mathcal{A}_{\mathtt {S2}}=\{1\}\), \(\mathcal{A}_{\mathtt {P}}=-\mathbb {N}\) (i.e., the set of nonpositive integers), and functions and predicates interpreted as follows:

The crucial point to obtain the proof in Example 6 is the ability to provide different interpretations to different sorts. The following example from [28] could not be handled by the 2010 version of mu-term because orderings were generated without paying attention to sorts (see [22, Sect. 6]).

Example 7

The following OS-TRS \(\mathcal{R}\) [28, Example 11] is nonterminating as a TRS:

figure c

There is a single OS-DP for \(\mathcal{R}\): \(\mathsf {F}(x) \rightarrow \mathsf {F}(\mathsf {h}(x))\), where \(\mathsf {F}\) has rank \(\mathtt {S} \rightarrow \mathtt {P}\) for a new sort \(\mathtt {P}\) and x has sort \(\mathtt {S1}\). We can prove termination of \(\mathcal{R}\) by finding a removal triple \((\gtrsim ,\succeq ,\sqsupset )\) such that the rules of \(\mathcal{R}\) are compatible with \(\gtrsim \), and \(\mathsf {F}(x) \sqsupset \mathsf {F}(\mathsf {h}(x))\) holds whenever x ranges on terms of sort \(\mathtt {S1}\). With AGES we obtain an interpretation \(\mathcal{A}\) as follows: sorts are interpreted as \(\mathcal{A}_{\mathtt {S}}=\{-1,0,1\}\), \(\mathcal{A}_{\mathtt {S1}}=\{-1\}\), \(\mathcal{A}_{\mathtt {S2}}=\{-1,0\}\), \(\mathcal{A}_{\mathtt {S3}}=\{-1\}\), \(\mathcal{A}_{\mathtt {S4}}=\{-1,0\}\), and \(\mathcal{A}_{\mathtt {P}}=\mathbb {N}\cup \{-1\}\). Functions and predicates are interpreted as follows:

(where different overloaded versions of g use the input sort as a subindex) and

Note that the interpretation of the ‘original’ rewrite relation concerns sort \(\text{ S }\) only because it is the top sort of the full sort hierarchy.

2.4 Termination of Context-Sensitive Rewriting

In context-sensitive rewriting (CSR [16]), a replacement map \(\mu \) is used to restrict the arguments \(\mu (f)\subseteq \{1,\ldots ,k\}\) which can be rewritten for each k-ary symbol f. The restriction on arguments is top-down propagated to positions of terms t, which are called active positions of t. We write \(s\hookrightarrow t\) if an active subterm of s can be rewritten so that \(s\rightarrow t\). In the dependency pair approach for proving termination of CSR [2], rules of the form \(f(\ell _1,\ldots ,\ell _k)\rightarrow r\) are given dependency pairs \(f^\sharp (\ell _1,\ldots ,\ell _k)\rightarrow g^\sharp (s_1,\ldots ,s_m)\), for \(s=g(s_1,\ldots ,s_m)\) a replacing subterm of \(r\) (i.e., a subterm \(s=r|_p\) occurring at an active position p of r) and g a defined symbol. The notation \(f^\sharp \) means that f is marked (capital letters F are often used instead of \(f^\sharp \)). However, due to rules \(\ell \rightarrow r\in \mathcal{R}\) with migrating variables \(x\in \mathcal{V}ar^\mu (r) {\setminus } \mathcal{V}ar^\mu (\ell )\) (that are frozen, i.e., not active, in \(\ell \) but become active in \(r\), possibly ‘awaking’ infinite rewrite sequences), we also need collapsing dependency pairs \(\ell ^\sharp \rightarrow x\) where x is a migrating variable of the rule.

Example 8

For the following TRS \(\mathcal{R}\) in [30, Introduction]

figure d

and \(\mu \) given by \(\mu (\mathsf {if})=\{1\}\) and \(\mu (f)=\{1,\ldots ,k\}\) for any other k-ary symbol f [12, Example 1]. \(\mathsf{DP}(\mathcal{R},\mu )\) consists of pairs

Collapsing pairs capture a kind of recursion which is hidden below frozen parts of the terms involved in infinite context-sensitive rewrite sequences until a migrating variable within a rule \(\ell \rightarrow r\) shows them up. The hidden terms of a TRS \(\mathcal{R}\) are defined subterms occurring at frozen positions in the rhs of some rule of \(\mathcal{R}\) [2]. Hiding contexts are contexts where hidden terms can occur at active positions within a context-sensitive rewrite sequence [1, 13]. There, hidden terms can restart a delayed recursive call after the application of a rule with migrating variables (see [12] for a detailed analysis). For \(\mathcal{R}\) and \(\mu \) in Example 8, the only rule with hidden terms is \(\mathsf {fact}(x) \rightarrow \mathsf {if}(\mathsf {zero}(x),\mathsf {s}(\mathsf {0}),\mathsf {fact}(\mathsf {p}(x))\times x)\). Symbols \(\mathsf {fact}\) and ‘\(\times \)’ hide position 1 because \(\mathsf {p}(x)\) is rooted by a defined symbol. Symbol ‘\(\times \)’ does not hide position 2. Symbol \(\mathsf {p}\) hides no position. The refinements introduced in [12] have led to a more precise notion of hidden terms and contexts, enabling a better analysis of the connections between them. This has greatly improved the ability of mu-term to prove termination of CSR. For instance, the proof of termination of \(\mathcal{R}\) and \(\mu \) in Example 8, which could not be obtained with the 2010 version of mu-term, is now possible with mu-term 6.0, see the proof of CSR_04/ExIntrod_Zan97.xml in the 2019 Termination Competition

http://group-mmm.org/termination/competitions/Y2019/caches/termination_33019.html

or in our local benchmarks:

http://zenon.dsic.upv.es/muterm/benchmarks/ijcar20/TRS_Contextsensitive/benchmarks.html

3 Termination Expert

The arbitrary application of processors can generate a huge search space. Furthermore, proofs usually proceed under some timeout. For this reason, we need to choose a fixed strategy where fast processors that reduce the number of rules are first used, and slow processors, or processors that increase the number of rules, are used when fast processors fail. Hence, the frequency of use for the different processors depends on the chosen strategy. With small differences depending on the particular kind of problem, we do the following:

  1. 1.

    If \(\mathcal{R}\) is a TRS or a CS-TRS, we check whether the system is innermost equivalent [3, Sect. 2.2]. If it is true, then we transform the problem into an innermost one.

  2. 2.

    Then, we obtain the corresponding dependency pairs, obtaining a CTRS, OS, CS, or DP problem. Then we perform the following steps repeatedly

    1. (a)

      Decision point between processors for proving (operational) non-termination and the strongly connected component (SCC) processor.

    2. (b)

      Subterm criterion processor.

    3. (c)

      Removal triple processor generating models with AGES (we try different configurations, from simpler to more complex).

    4. (d)

      If \(\mathcal{R}\) is a CTRS, we apply simplification and removal processors on the conditions (using AGES when a model is necessary).

    5. (e)

      Transformation processors on rules, pairs and conditions: instantiation, forward instantiation, and narrowing.

Full explanations of the processors can be found in [4, 12, 13, 19, 20, 24, 25]. The mu-term 6.0 logic-based approach has led to dramatic improvements, as reported here:

http://zenon.dsic.upv.es/muterm/benchmarks/ijcar20/Comparison/benchmarks.html

where the use of logical models is compared with the exclusive use of polynomial interpretations (as in mu-term 5.0). Polynomial interpretations are strictly less powerful in terms of solved examples (as every proof using polynomial interpretations can be obtained using the new logic-based approach). However, we keep them in mu-term 6.0 as they lead to faster proofs. We use polynomial interpretations as part of mu-term 6.0 strategy (via the removal triple processor).

mu-term 6.0 consists of more than 30000 lines of Haskell code. In the web-based interface, besides the fully automatic use of the termination expert, we can also use specific techniques like polynomial orderings, matrix interpretations, (context-sensitive) recursive path ordering, etc., which we have found useful for teaching purposes.

4 Experimental Evaluation

Since 2014, mu-term has proven to be the most powerful tool for proving operational termination of conditional rewriting and termination of context-sensitive rewriting, each year winning the corresponding subcategory of the annual International Competition of Termination Tools, see http://zenon.dsic.upv.es/muterm/?page_id=82 for an historical account. In the CSR subcategory, since 2014 mu-term is able to prove all the examples proved by any other participating tool (thanks to the results in [12]).

The benchmarks web page of mu-term reports on specific experiments comparing the 2010 and 2020 versions. First, the 2010 version did not support CTRSs. For CS-TRSs, three new examples can be proved now (and all the examples handled by the 2010 version are also handled now). As for OS-TRSs, mu-term 6.0 is able to prove or disprove termination of all the OS-TRSs in the 2010 benchmark suite (except a non-sort-decreasing OS-TRS, not covered by the theory in [22], where sort-decreasingness [11] is required). The 2010 version could not disprove termination of OS-TRSs.