"Dependency Triples for Improving Termination Analysis of Logic Programs with Cut" - Experiments and Proofs

In very recent work (see Automated Termination Analysis for Logic Programs with Cut), we introduced a non-termination preserving transformation from logic programs with cut to definite logic programs. While that approach allows us to prove termination of a large class of logic programs with cut automatically, in several cases the transformation results in a non-terminating definite logic program. In the paper Dependency Triples for Improving Termination Analysis of Logic Programs with Cut we extend the transformation such that logic programs with cut are no longer transformed into definite logic programs, but into dependency triple problems. In our experiments, we want to assess the power of our improved transformation on a large set of examples.

A full version of our paper including all proofs is available here.

A formal proof on the correspondenc of our inference rules to the semantics of the Prolog ISO standard can be found in the diploma thesis of Thomas Ströder.


Implementation in AProVE

We integrated the pre-processing in the termination tool AProVE which is already one of the most powerful termination tools for definite logic programs. It can be accessed via a custom web interface.


Settings

We compare the new version of AProVE that uses the transformation to dependency triples both with a version that uses the transformation to definite logic programs and with a version that ignores cuts.

Examples

We ran the tools on all 402 examples for logic programs from the Termination Problem Data Base used for the international Termination Competition. These examples have been collected from a large number of sources including several papers, entries for programming contests, and freely available Prolog programs.


Experiments & Discussion

The three versions of AProVE were run on a 2.67 GHz Intel Core i7 and as in the Termination Competition, we used a timeout of 60 seconds for each example.

In the first table, for all versions we give the number of examples which could be proved terminating (denoted "Successes"), the number of examples where termination could not be shown ("Failures"), the number of examples for which the timeout of 60 seconds was reached ("Timeouts"), and the total runtime ("Total") in seconds on all 402 examples of the TPDB. For those examples where termination could be proved, we indicate how many of them contain cuts

ToolAProVE DirectAProVE CutAProVE DT
Successes
- with cut
- without cut
243
10
233
259
78
181
315
82
233
Failures14412977
Timeouts151410
Total2485.73288.02311.6

The table shows that the new transformation (column "AProVE DT") significantly increases the number of examples that can be proved terminating. In particular, we obtain additional 56 proofs of termination compared to the transformation to definite logic programs (column "Cut"). And indeed, whenever the transformation to definite logic programs succeeds, our new transformation to dependency triples succeeds, too. Note that while our previous work is very successful on examples with cut, its performance is significantly worse than that of "AProVE Direct" on the other examples of the TPDB.

In addition to being more powerful, the version using dependency triples is also more efficient than any of the two other versions resulting in fewer timeouts and a total runtime that is less than the one of the direct version and only 70% of the version using the previous transformation.

The second table allows access to the detailed proof output of the respective tools. By clicking on the time for a given example and tool, you can see all the proof steps that the tool performed on this example. This detailed table also allows to load each individual example into our web interface.

ExampleAProVE DirectAProVE CutAProVE DT
YES1.87MAYBE3.6YES2.18
YES1.15YES2.74YES2.85
YES2.13YES3.21YES3.23
YES1.93YES3.32YES2.41
YES1.49YES2.5YES2.04
MAYBE13.64MAYBE30.06MAYBE28.93
YES2.23YES5.58YES3.25
YES2.2YES3.68YES3.88
YES1.29YES3.47YES3.27
YES1.31YES3.61YES4.74
YES2.19MAYBE14.83YES4.34
MAYBE19.06MAYBE11.03MAYBE10.48
YES2.03MAYBE6.08YES4.6
YES1.41YES4.05YES3.94
MAYBE2.58MAYBE2.74MAYBE2.4
YES1.53YES3.09YES3.31
YES1.54YES3.22YES2.91
YES1.48YES2.78YES2.82
MAYBE8.43MAYBE6.08MAYBE5.34
MAYBE2.3MAYBE3.22MAYBE3.93
YES2.0MAYBE4.07YES1.9
MAYBE9.55MAYBE8.29MAYBE4.4
MAYBE2.66MAYBE2.38MAYBE2.04
MAYBE12.95MAYBE21.51MAYBE20.29
YES1.98YES1.88YES1.78
YES1.66MAYBE3.27YES1.73
MAYBE8.52MAYBE7.54MAYBE3.6
YES1.85YES2.04YES2.01
YES2.3YES2.63YES2.12
MAYBE13.53MAYBE20.95MAYBE20.36
YES1.58YES2.75YES2.62
YES1.68YES3.8YES2.32
YES1.21YES4.15YES4.01
YES1.49YES2.74YES2.68
YES1.37YES2.76YES3.03
YES1.55YES3.0YES3.8
YES1.41YES2.71YES2.4
YES1.47YES2.22YES2.49
YES1.89YES1.43YES1.26
YES1.48YES1.33YES1.89
YES1.58YES3.5YES4.12
MAYBE2.09MAYBE3.81MAYBE3.63
YES1.27YES3.05YES3.28
MAYBE18.26MAYBE17.15MAYBE12.2
YES1.18YES3.1YES3.55
MAYBE1.68MAYBE4.96MAYBE3.69
YES1.65YES1.51YES1.32
YES1.51MAYBE2.32YES1.37
MAYBE2.08MAYBE3.03MAYBE2.3
YES2.14YES2.99YES2.75
YES1.92YES3.67YES3.67
YES1.64YES1.69YES1.31
YES1.93YES5.47YES3.13
YES1.38YES5.56YES4.36
YES1.92YES1.78YES1.88
MAYBE2.1MAYBE5.59MAYBE6.26
YES2.78MAYBE30.52YES3.28
YES2.41YES8.05YES6.87
YES2.03YES2.64YES2.33
YES1.53YES2.86YES2.57
YES2.17MAYBE14.38YES3.55
MAYBE19.89MAYBE22.56MAYBE13.06
YES1.78YES2.21YES1.35
MAYBE2.19MAYBE2.84MAYBE1.62
YES1.5YES2.04YES1.68
MAYBE2.26MAYBE4.18MAYBE3.79
YES1.22YES4.12YES3.67
YES1.65YES3.05YES3.45
YES2.17YES1.63YES1.6
YES2.17MAYBE4.87YES1.75
MAYBE2.62MAYBE3.12MAYBE2.73
MAYBE2.41MAYBE3.61MAYBE3.51
YES1.27YES3.0YES2.83
MAYBE2.19MAYBE4.22MAYBE4.01
MAYBE10.71MAYBE11.48MAYBE10.79
MAYBE1.93MAYBE3.76MAYBE3.33
YES1.2YES2.42YES2.42
YES1.19YES3.34YES2.7
YES1.51YES4.58YES3.11
YES1.57YES2.09YES2.12
YES2.21YES5.12YES4.49
YES1.84YES4.76YES4.58
YES1.78YES5.69YES5.65
MAYBE1.87MAYBE2.29MAYBE2.42
YES2.11YES5.47YES5.01
YES1.58YES2.85YES3.23
MAYBE2.7MAYBE4.71MAYBE2.71
YES1.56MAYBE3.46YES1.68
YES1.78YES2.01YES1.3
YES1.39YES1.49YES1.7
MAYBE2.33MAYBE3.9MAYBE3.03
YES1.51YES3.2YES2.15
MAYBE2.67MAYBE17.81MAYBE15.07
YES1.57YES17.31YES15.11
KILLED60MAYBE24.99MAYBE24.13
MAYBE3.34MAYBE6.8MAYBE4.4
YES2.98MAYBE11.62YES5.1
YES2.87MAYBE16.89YES3.37
YES1.68MAYBE3.38YES1.84
YES1.32YES2.42YES2.77
YES1.99YES1.8YES1.85
YES1.71YES3.58YES3.57
YES1.61YES1.45YES1.32
YES1.69YES2.06YES1.53
KILLED60KILLED60KILLED60
YES1.32YES4.25YES5.26
YES1.43YES3.79YES3.38
YES2.83YES1.99YES1.61
YES1.85YES2.01YES1.87
YES1.56YES1.6YES1.89
YES2.03MAYBE6.76YES2.68
YES8.13YES11.27YES14.65
YES1.7MAYBE7.19YES2.48
YES1.7MAYBE2.74YES1.9
YES1.39YES5.14YES4.75
MAYBE15.25KILLED60KILLED60
KILLED60KILLED60KILLED60
YES2.24YES12.56YES12.31
YES1.36YES3.02YES2.94
YES1.97MAYBE5.52YES4.76
YES2.34YES2.16YES3.71
YES1.75YES4.42YES4.38
YES1.45MAYBE9.29YES4.3
YES1.79YES3.87YES3.48
YES2.5YES4.57YES4.07
MAYBE18.8MAYBE20.07MAYBE16.13
YES1.85YES2.23YES1.36
YES1.7YES2.62YES2.75
MAYBE1.93YES2.18YES2.77
YES1.53YES2.01YES2.53
YES1.69MAYBE2.76YES1.64
YES1.45YES4.73YES4.41
YES1.68YES4.33YES3.97
KILLED60MAYBE24.93MAYBE24.19
YES1.89MAYBE3.44YES2.21
YES2.18YES3.25YES3.03
YES2.04YES3.43YES3.32
YES2.2YES4.37YES3.34
YES2.25YES1.45YES1.56
YES1.2YES3.33YES2.68
YES2.55MAYBE32.3YES3.54
YES2.6YES7.97YES7.63
YES1.44YES3.59YES3.67
YES1.42YES3.02YES2.65
YES1.4YES3.78YES3.89
YES2.04MAYBE16.79YES13.62
MAYBE2.11MAYBE3.25MAYBE2.98
KILLED60YES7.05YES6.13
YES2.04YES2.42YES2.38
YES1.93KILLED60YES2.67
YES1.96YES5.03YES5.17
YES2.49MAYBE11.01YES4.88
MAYBE15.92KILLED60KILLED60
YES1.74MAYBE17.39YES3.44
YES1.59YES2.86YES2.38
YES1.66YES1.95YES2.04
MAYBE2.01MAYBE6.19MAYBE6.29
YES2.23YES7.78YES4.57
YES2.2KILLED60KILLED60
YES1.68YES3.73YES3.34
YES1.32YES3.08YES3.15
YES1.87YES2.54YES2.84
YES1.25YES3.87YES4.45
YES1.27YES2.6YES2.56
YES1.31YES2.71YES2.85
YES1.63YES2.96YES3.12
YES2.9MAYBE54.82YES6.26
YES2.86MAYBE7.63YES5.34
MAYBE2.19MAYBE3.28MAYBE1.89
YES1.32MAYBE2.39YES1.79
YES1.56YES4.29YES4.23
YES1.54YES4.13YES3.01
YES2.52YES2.47YES1.71
MAYBE34.42MAYBE43.22MAYBE32.32
YES2.63MAYBE27.71YES3.18
YES1.46YES3.93YES3.8
YES1.49YES3.59YES3.45
KILLED60MAYBE24.32MAYBE24.17
KILLED60MAYBE24.3MAYBE23.67
KILLED60MAYBE24.58MAYBE23.59
MAYBE11.11MAYBE10.85MAYBE10.75
YES1.79YES3.63YES3.56
YES1.25YES2.79YES3.42
YES1.18YES4.12YES2.87
YES1.62YES4.35YES4.54
YES1.74YES1.5YES1.42
YES1.89YES3.03YES2.68
YES2.83YES3.16YES2.33
YES1.33YES4.45YES4.49
YES1.19YES3.38YES3.72
YES1.92YES3.0YES4.24
YES2.33YES3.57YES2.92
YES1.61YES3.91YES3.49
YES1.45MAYBE3.8YES2.14
MAYBE2.29MAYBE5.95MAYBE5.49
YES1.6MAYBE3.15YES1.68
MAYBE2.63MAYBE5.91MAYBE5.43
YES1.7YES4.85YES4.96
YES2.47MAYBE7.86YES6.49
YES2.77MAYBE8.03YES3.84
YES1.74YES6.04YES7.11
YES2.26YES2.5YES2.64
YES1.29YES2.52YES2.75
YES2.43MAYBE28.04YES3.79
YES2.02KILLED60YES4.93
YES1.68YES1.53YES1.72
YES1.34YES4.52YES4.43
YES1.6YES4.61YES4.99
YES1.68YES3.12YES3.59
YES1.38YES4.35YES4.7
YES1.39YES4.61YES4.53
YES2.04KILLED60KILLED60
YES4.44MAYBE6.44YES3.22
MAYBE1.91MAYBE4.61MAYBE3.87
YES1.63YES1.88YES2.25
YES2.13YES1.75YES1.79
YES1.33YES2.85YES2.64
MAYBE5.34MAYBE4.1MAYBE3.63
YES2.11YES2.46YES2.51
MAYBE2.96MAYBE5.08MAYBE3.93
MAYBE2.66MAYBE4.93MAYBE4.41
YES1.27YES4.32YES3.94
YES1.88YES2.8YES2.02
YES1.38MAYBE2.83YES1.35
MAYBE2.86MAYBE29.38MAYBE5.44
MAYBE1.81MAYBE3.24MAYBE3.15
MAYBE2.27MAYBE3.85MAYBE3.73
MAYBE2.34MAYBE3.6MAYBE3.89
KILLED60KILLED60KILLED60
YES2.23MAYBE22.27YES3.48
YES1.63MAYBE2.12YES1.94
MAYBE12.58MAYBE17.84MAYBE17.36
MAYBE36.0MAYBE41.71MAYBE42.26
YES2.44YES2.44YES1.91
YES2.84MAYBE7.28YES3.78
YES4.03MAYBE7.99YES3.73
YES2.66MAYBE14.24YES3.73
KILLED60MAYBE14.34KILLED60
YES1.19YES2.41YES2.51
YES1.96KILLED60YES28.14
YES1.27YES3.77YES3.25
YES2.08YES2.5YES3.0
YES2.23MAYBE4.97YES2.27
MAYBE5.58MAYBE7.35MAYBE4.99
YES2.38YES3.02YES2.19
YES1.8YES3.8YES4.27
YES2.02MAYBE5.94YES2.05
YES1.37YES2.65YES2.87
MAYBE2.23MAYBE2.98MAYBE2.55
YES1.88YES2.05YES2.24
YES1.8YES4.47YES4.72
YES2.72YES4.07YES2.29
YES1.76MAYBE3.13YES2.03
YES1.89YES4.0YES3.9
YES1.59YES1.87YES1.58
YES2.27YES1.58YES2.45
YES1.62YES3.82YES3.94
YES2.83MAYBE16.05YES3.7
YES2.67YES5.35YES4.91
YES1.8YES4.61YES5.43
YES1.39YES2.87YES2.66
MAYBE2.66MAYBE2.93MAYBE1.97
YES1.64YES2.06YES1.79
YES1.4YES4.16YES4.46
YES3.24YES10.04YES8.73
YES1.2YES3.52YES3.18
YES1.35YES3.74YES2.55
YES1.27YES2.53YES2.56
YES2.23MAYBE15.15YES3.17
YES1.88YES1.62YES2.01
YES1.3YES2.6YES2.55
YES1.58MAYBE3.17YES1.72
YES1.55YES5.67YES5.46
YES2.23YES1.35YES1.43
YES1.59YES2.34YES1.47
YES2.01YES3.45YES3.26
YES1.57YES4.06YES4.23
YES1.95YES2.61YES1.93
YES1.39YES2.69YES2.83
YES3.78MAYBE6.27YES4.46
YES1.68MAYBE3.31YES2.1
YES1.32YES3.85YES4.21
YES1.43YES3.93YES3.58
MAYBE3.85MAYBE16.61MAYBE13.2
YES1.76YES10.77YES10.99
YES1.24MAYBE2.71YES1.56
YES1.76YES2.84YES2.79
YES1.84YES1.97YES1.72
YES1.45YES3.66YES3.78
YES2.22YES2.25YES2.35
YES2.3YES4.33YES4.3
YES1.82YES4.53YES4.6
YES1.71YES4.68YES4.29
MAYBE2.53MAYBE5.39MAYBE5.79
YES2.13YES4.13YES4.14
MAYBE11.13MAYBE10.34MAYBE10.93
YES1.58YES3.74YES3.24
YES1.74YES11.89YES11.56
MAYBE2.12MAYBE2.1MAYBE3.2
MAYBE13.85YES2.59YES1.57
MAYBE4.32YES1.79YES5.17
MAYBE12.78YES1.39YES1.27
MAYBE13.4YES2.11YES1.73
MAYBE13.94YES1.9YES1.55
MAYBE1.8YES1.28YES2.8
MAYBE13.13YES1.58YES3.83
MAYBE7.2YES1.24YES4.18
MAYBE7.34YES1.59YES2.89
YES1.47YES1.28YES5.22
MAYBE1.93MAYBE1.74MAYBE2.58
YES2.07YES2.05YES3.96
MAYBE7.23MAYBE2.08MAYBE4.2
KILLED60MAYBE32.26KILLED60
MAYBE7.24YES1.51YES4.62
YES1.57YES9.75YES4.75
MAYBE12.99YES1.86YES2.91
MAYBE1.82MAYBE1.89MAYBE2.63
YES1.45YES1.45YES4.34
MAYBE2.23MAYBE1.98MAYBE3.82
MAYBE2.34MAYBE2.28YES2.45
YES1.73YES1.4YES1.83
YES1.89YES3.8YES2.25
MAYBE5.78YES1.96YES4.32
YES1.6YES1.83YES5.28
MAYBE2.17KILLED60MAYBE3.49
MAYBE2.34YES1.57YES2.87
MAYBE5.27YES1.76YES2.78
MAYBE5.3MAYBE2.33MAYBE3.93
MAYBE1.16YES1.61YES4.9
MAYBE9.86YES1.25YES3.04
MAYBE10.14MAYBE2.19MAYBE5.64
MAYBE1.37YES1.44YES5.25
MAYBE15.05MAYBE3.06MAYBE2.87
MAYBE29.35MAYBE34.5MAYBE3.15
MAYBE11.48YES2.33YES1.43
MAYBE1.1YES1.53YES1.36
MAYBE9.37YES1.47YES1.24
MAYBE15.95MAYBE4.35MAYBE2.54
MAYBE17.47MAYBE6.31MAYBE4.52
MAYBE1.68YES2.03YES2.22
MAYBE21.22YES2.03YES1.44
KILLED60YES2.27YES1.43
MAYBE21.8KILLED60YES1.81
MAYBE1.37YES2.18YES1.64
MAYBE16.04YES1.85YES7.04
MAYBE1.94YES1.58YES2.07
MAYBE3.01MAYBE2.36MAYBE2.75
MAYBE1.5YES1.7YES1.55
MAYBE26.09YES2.1YES2.09
MAYBE1.13YES2.06YES2.52
MAYBE1.43YES3.43YES1.76
MAYBE5.12YES3.75YES4.78
MAYBE7.73YES1.21YES3.36
MAYBE1.68YES1.44YES5.03
MAYBE3.16YES1.4YES3.27
MAYBE8.27YES1.14YES3.19
MAYBE22.47MAYBE2.34MAYBE1.85
YES2.0YES1.3YES4.86
MAYBE1.75YES1.47YES1.28
MAYBE29.21YES1.65YES5.49
MAYBE25.43MAYBE12.58YES4.18
MAYBE8.61YES1.65YES1.41
MAYBE1.1YES1.61YES1.36
YES1.67YES2.81YES1.92
MAYBE1.79YES1.4YES4.55
MAYBE7.0YES2.39YES2.81
MAYBE23.26MAYBE14.06MAYBE5.81
MAYBE1.74YES1.58YES1.35
MAYBE1.75YES1.13YES3.46
MAYBE7.25YES1.35YES2.46
MAYBE2.17YES1.35YES2.1
MAYBE1.65YES1.59YES3.43
MAYBE8.56YES1.29YES3.33
MAYBE8.59MAYBE2.98YES1.39
MAYBE1.83YES2.03YES3.45
MAYBE5.18YES1.24YES2.63
MAYBE19.32MAYBE3.28MAYBE2.79
MAYBE1.18YES2.78YES1.66
MAYBE19.86YES2.29YES2.17
MAYBE7.53YES1.45YES5.31
MAYBE1.31YES1.58YES1.72
MAYBE3.49MAYBE2.23MAYBE3.38
MAYBE2.31YES2.7YES2.7
MAYBE2.53YES1.58YES2.99
MAYBE2.46YES1.56YES2.87
MAYBE41.17YES2.05YES7.25
KILLED60KILLED60KILLED60
YES4.86YES9.53YES5.8
MAYBE1.26YES6.07YES4.49
MAYBE1.15YES2.58YES1.53
MAYBE14.56YES2.06YES1.5
MAYBE10.07YES1.26YES3.75
MAYBE1.8YES1.79YES1.71
MAYBE22.44KILLED60MAYBE19.47
MAYBE6.69MAYBE14.09MAYBE7.59
KILLED60YES14.21YES7.13
MAYBE1.73YES1.42YES5.12
MAYBE32.25YES1.41YES3.23
MAYBE1.31YES1.37YES2.53
MAYBE2.3YES1.66YES2.21
MAYBE1.4YES1.34YES3.62
KILLED60MAYBE20.7MAYBE13.87