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

- 192 Downloads

## Abstract

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.

## 1 Introduction

*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:

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

^{1}an inference system \(\mathcal{I}(\mathcal{R})\) is obtained from the following generic inference system \(\mathfrak {I}_{\text {CTRS}}\)

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

### 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 Open image in new window and Open image in new window 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). Open image in new window 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, Open image in new window 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}\).^{2}

### Example 2

For \(\mathcal{R}\) in Example 1, we have Open image in new window and Open image in new window

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.
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.
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 Open image in new window) by just finding a model of

### Example 3

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

**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

*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]:

### Example 5

*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

^{3}According to [22], \(\mathcal{R}\) has a single dependency pair:

*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:

*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) andNote 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

*k*-ary symbol

*f*[12, Example 1]. \(\mathsf{DP}(\mathcal{R},\mu )\) consists of pairs

*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

or in our local benchmarks:http://group-mmm.org/termination/competitions/Y2019/caches/termination_33019.html

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

## 3 Termination Expert

*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.
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.Then, we obtain the corresponding dependency pairs, obtaining a CTRS, OS, CS, or DP problem. Then we perform the following steps repeatedly
- (a)
Decision point between processors for proving (operational) non-termination and the

*strongly connected component*(SCC) processor. - (b)
Subterm criterion processor.

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

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

- (e)
Transformation processors on rules, pairs and conditions: instantiation, forward instantiation, and narrowing.

- (a)

where the use of logical models is compared with the exclusive use ofhttp://zenon.dsic.upv.es/muterm/benchmarks/ijcar20/Comparison/benchmarks.html

*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.

## Footnotes

- 1.
Oriented CTRSs treat conditions \(s_i\approx t_i\) in rules as

*rewriting*goals \(\sigma (s_i)\rightarrow ^*\sigma (t_i)\) for appropriate substitutions \(\sigma \) [27, Definition 7.1.3]. - 2.
A third set of dependency pairs Open image in new window is used in [23]. For simplicity, in the examples of this paper, Open image in new window is empty and we pay no attention to it.

- 3.
Benchmarks available here: http://zenon.dsic.upv.es/muterm/benchmarks/benchmarks-ostrs/benchmarks.html.

## Notes

### Acknowledgments

We thank the anonymous referees for many remarks and suggestions that led to improve the paper.

## References

- 1.Alarcón, B., et al.: Improving context-sensitive dependency pairs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 636–651. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_44CrossRefGoogle Scholar
- 2.Alarcón, B., Gutiérrez, R., Lucas, S.: Context-sensitive dependency pairs. Inf. Comput.
**208**(8), 922–968 (2010). https://doi.org/10.1016/j.ic.2010.03.003MathSciNetCrossRefzbMATHGoogle Scholar - 3.Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-17796-5_12CrossRefGoogle Scholar
- 4.Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for \({A} \vee {C}\)-termination. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 35–51. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_4CrossRefGoogle Scholar
- 5.Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci.
**236**(1–2), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8MathSciNetCrossRefzbMATHGoogle Scholar - 6.Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1CrossRefzbMATHGoogle Scholar
- 7.Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reasoning
**40**(2–3), 195–220 (2008). https://doi.org/10.1007/s10817-007-9087-9MathSciNetCrossRefzbMATHGoogle Scholar - 8.Giesl, J., Arts, T.: Verification of erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput.
**12**(1/2), 39–72 (2001). https://doi.org/10.1007/s002000100063MathSciNetCrossRefzbMATHGoogle Scholar - 9.Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_12CrossRefzbMATHGoogle Scholar
- 10.Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning
**37**(3), 155–203 (2006). https://doi.org/10.1007/s10817-006-9057-7MathSciNetCrossRefzbMATHGoogle Scholar - 11.Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci.
**105**(2), 217–273 (1992). https://doi.org/10.1016/0304-3975(92)90302-VMathSciNetCrossRefzbMATHGoogle Scholar - 12.Gutiérrez, R., Lucas, S.: Function calls at frozen positions in termination of context-sensitive rewriting. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 311–330. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_15CrossRefzbMATHGoogle Scholar
- 13.Gutiérrez, R., Lucas, S.: Proving termination in the context-sensitive dependency pair framework. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 18–34. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_3CrossRefGoogle Scholar
- 14.Gutiérrez, R., Lucas, S.: Automatic generation of logical models with AGES. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 287–299. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_17CrossRefGoogle Scholar
- 15.Gutiérrez, R., Lucas, S.: Automatically proving and disproving feasibility conditions. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNAI, vol. 12167, pp. 416–435. Springer, Heidelberg (2020)Google Scholar
- 16.Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Log. Program.
**1998**(1), 1–61 (1998). http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html - 17.Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput.
**178**(1), 294–343 (2002). https://doi.org/10.1006/inco.2002.3176MathSciNetCrossRefzbMATHGoogle Scholar - 18.Lucas, S.: Proving semantic properties as first-order satisfiability. Artif. Intell.
**277**(2019). https://doi.org/10.1016/j.artint.2019.103174 - 19.Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reasoning
**60**(4), 465–501 (2017). https://doi.org/10.1007/s10817-017-9419-3MathSciNetCrossRefzbMATHGoogle Scholar - 20.Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett.
**136**, 90–95 (2018). https://doi.org/10.1016/j.ipl.2018.04.002MathSciNetCrossRefzbMATHGoogle Scholar - 21.Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett.
**95**(4), 446–453 (2005). https://doi.org/10.1016/j.ipl.2005.05.002MathSciNetCrossRefzbMATHGoogle Scholar - 22.Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Antoy, S., Albert, E. (eds.) Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 15–17 July 2008, Valencia, Spain, pp. 108–119. ACM (2008). https://doi.org/10.1145/1389449.1389463
- 23.Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebraic Methods Program.
**86**(1), 236–268 (2017). https://doi.org/10.1016/j.jlamp.2016.03.003MathSciNetCrossRefzbMATHGoogle Scholar - 24.Lucas, S., Meseguer, J., Gutiérrez, R.: The 2D dependency pair framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci.
**96**, 74–106 (2018). https://doi.org/10.1016/j.jcss.2018.04.002 - 25.Lucas, S., Meseguer, J., Gutiérrez, R.: The 2D dependency pair framework for conditional rewrite systems—part II: advanced processors and implementation techniques. J. Autom. Reasoning (2020). https://doi.org/10.1007/s10817-020-09542-3
- 26.McCune, W.: Prover9 & Mace4. Technical report (2005–2010). http://www.cs.unm.edu/~mccune/prover9/
- 27.Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002). https://doi.org/10.1007/978-1-4757-3661-8. http://www.springer.com/computer/swe/book/978-0-387-95250-5
- 28.Ölveczky, P.C., Lysne, O.: Order-sorted termination: the unsorted way. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 92–106. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61735-3_6CrossRefGoogle Scholar
- 29.Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput.
**17**(1), 23–50 (1994). https://doi.org/10.1006/jsco.1994.1003MathSciNetCrossRefzbMATHGoogle Scholar - 30.Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 172–186. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-62950-5_69CrossRefzbMATHGoogle Scholar