Experiments on termination problems

General Information

Our termination tool employs the dependency pair method with cycle analysis of dependency graphs, reduction pairs, and rule removal by monotone reduction pairs.

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

• L ⊆ LL ⊇ LLL. The last reverse inclusion is due to timeouts.
• E1 ⊆ E1E1 ⊆ E2 ⊆ E3 ⊈ E4. The non-inclusion is due to timeouts. |E3 ∪ E4| = 585.
• S2 ⊈ S2S2 ⊇ S2S2S2; The non-inclusion and the reverse inclusion are simply due to timeouts. |S2 ∪ S2S2| = 623.
• |L ∪ E1| = 512 and |L ∪ E1 ∪ LE1 ∪ E1L| = |L ∪ E1 ∪ E1L| = 537.
• |L ∪ E1 ∪ S2| = 625.
• The union of all except AProVE amounts to 649, which is covered by LL ∪ E3 ∪ E4 ∪ S2 ∪ S2S2 ∪ E1L.
• The 649 contains 3 problems that AProVE missed but they are merely due to a parse error and efficiency reasons.