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
| Tool | AProVE Direct | AProVE Cut | AProVE DT |
|---|
Successes
- with cut
- without cut | 243
10
233 | 259
78
181 | 315
82
233 |
| Failures | 144 | 129 | 77 |
| Timeouts | 15 | 14 | 10 |
| Total | 2485.7 | 3288.0 | 2311.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.