Automated Termination Analysis for Term Rewriting
Nao Hirokawa · 2006
variable, 66 algebra, 16 weakly monotone, 16 well-founded, 16 argument filtering, 26 reverse, 71 arity, 10 assignment, 16 carrier, 16 collapsing, 13 compatible, 50 constant, 10 context, 11 closed under, 12 cycle, 21 defined symbol, 12 dependency graph, 21 approximation, 37 estimated, 37 estimated*, 38 dependency pair, 20 symbol, 20 domain, 11, 49 duplicating, 13 η-saturation, 74 evaluation, 16 extension, 49 function strictly monotone, 16 weakly monotone, 16 function symbol, 10 ground, 11 ground term existence condition, 74 head variable instantiation, 74 hole, 11 induced algebra, 58 innermost dependency graph, 22 estimated innermost, 38 estimated* innermost, 38 innermost rewrite relation, 12 innermost terminating, 12 interpretation, 16, 30 KBO, 15 Knuth-Bendix order, 15 lexicographic path order, 14 with quasi-precedence, 15 linear, 11 linearization, 63 LPO, 14 mgu, 12 minimal non-terminating term, 19 MPO, 14 multiset, 13 multiset extension, 14 multiset path order, 14 natural polynomial interpretation, 57 non-overlapping, 13 normal form, 12