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

NaTT

NaTT (termCOMP 2024 version)

For instance, 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.
• |E1L or E2L or E3L or E4L| = 568
• The union of Ed, L, and their combinations amounts to 592.
• The union of all except AProVE and NaTT 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.
• The 649 contains 8 problems that NaTT missed. Here 3 problems can be shown by S2 and L, but the remaining 5 problems are handled by E3, E4, or S2S2:
  AG01_3.40, Transformed_CSR_04_Ex4_DLMMU04_iGM, Transformed_CSR_04_LengthOfFiniteLists_nokinds_noand_C, and Transformed_CSR_04_PEANO_nokinds_noand_C.