
doi: 10.1007/10721959_27
handle: 10854/1890
Although theoretically it is very powerful, the semantic path ordering (SPO) is not so udeful in practice, since its monotonicity has to be proved by hand for each concrete term rewrite system (TRS). In this paper we present a monotonic variation of SPO, called MSPO. It characterizes termination, i.e. a TRS is terminating if and only if ist rules are included in some MSPO. Hence MSPO is a complete termination method. On the practical side, it can be easily automated using as ingredients standard interpretations and general-purpose ordering like RPO. This is shown to be a sufficiently powerful way to handeke several non-trivial examples and to obtain methods like dummy elimination or dependency pairs (without the dependency graph refinement) as particular cases. Finally, we obtain some positive modularity results for termination based on MSPO.
Lògica matemàtica -- Congressos
Lògica matemàtica -- Congressos
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 23 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
