Summary of Performed Tests

Explanations

The following table summarizes the results of trying to prove cycle termination of different problem set.

The used techniques and tools are:
  • torpacyc is tested in two versions, where the version of 2014 includes match bounds, arctic and tropical matrix interpretations using type graphs, and the version of 2015 improves these techniques by more general matrix interpretations.
  • The transformations split, rotate and shift transform a cycle rewrite system into a string rewrite system without changing termination, s.t. the original system is cycle termination if and only if the transformed system is string terminating. After transforming the problem the termination prover AProVE or the termination prover TTT2 is applied to the problem.
  • The combination 1 first applies torpacyc (version 2015) to the problem. If no termination proof is found, then the output rewrite system of torpacyc is transformed by split into a string termination problem and put in the termination prover AProVE, or the termination prover TTT2, respectively.
  • The combination 2 first tries to disprove string termination of the problem, by applying AProVE or TTT2, respectively. If nontermination is proved, then the cycle rewrite system is nonterminating too. If no nontermination proof is found, combination 1 is used as a second step.

Download

Due to their large size not all termination proofs generated by termination provers are included on the corresponding websites, but they can be downloaded as a single compressed tar-archive [here] (compressed size ~1,2GB, uncompressed ~26GB)

Summarized Results


torpacyc SPLIT ROTATE SHIFT Combination 1 Combination 2 any tool
2014 2015 AProVE TTT2 AProVE TTT2 AProVE TTT2 AProVE TTT2 AProVE TTT2
SRS_Standard of the Termination Problem Data Base (timeout 60 sec., [details])
SUM YES 334640301061085555545463
SUM NO 00309168450650310161335173336
SUM MAYBE 128212699661117126013091240130795010999261088916
50 000 randomly generated SRS of size 12 (timeout 60 sec., [details])
SUM YES 46981 46929 47017 47073 36967 36260 37053 37027 47071 46967 47064 47015 47124
SUM NO 0 0 2331 2201 184 0 771 0 2328 2011 2334 2174 2339
SUM MAYBE 3019 3071 652 726 12849 13740 12176 12973 601 1022 602 811 537
Selected Problems (timeout 900 sec., [details])
SUM YES 3 9 8 9 1 1 1 2 10 9 9 9 10
SUM NO 0 0 1 1 1 0 1 1 1 1 0 1 1
SUM MAYBE 8 2 2 1 9 10 9 8 0 1 2 1 0
Navigation [+/-]