Experiments on relative termination problems

General Information

Our termination tool employs the dependency pair method by Iborra et al. (2017) with cycle analysis of dependency graphs, reduction pairs, and rule removal by monotone reduction pairs. Note that usable rules are not used due to a soundness reason. The problem set is taken from the TRS Relative category of the Termination Problem Database.

d

applicability of the dependency pair method by Iborra et al. (2017) (R dominates S and S is non-duplicating)

L

lexicographic path orders (LPO) with argument filtering

Ed

echelon-form matrix interpretations on N^d with 0,1-matrix coefficients, equipped with the lexicographic order (Section 5)

Sd

matrix interpretations on N^d with 0,1-matrix coefficients, equipped with the standard order (by Endrullis et al. 2008)

AProVE

AProVE 2024

For instances, E1L stands for the lexicographic combination of E1 and L. Note that E1 and S1 are identical. Concerning heterogeneous combinations, (e.g.) E1 ⊆ E1L does not hold in general, as weak orientation by E1 does not guarantee weak orientation by L.

Note

• The 57 problems where d is labeled YES are the targets of our experiments.
• L ⊆ LL ⊆ LLL.
• E1 ⊆ E1E1 ⊆ E2 ⊆ E3 ⊆ E4.
• S2 ⊆ S2S2 ⊆ S2S2S2.
• On the 57 problems where the The union of all methods (including AProVE) on amounts to 50, which is covered by LL ∪ E4.