Wanda experiments for ESOP 2019

These experiments were done for the paper A static higher-order dependency pair framework, published in the proceedings for ESOP 2019. All experiments were performed with Wanda version 2.1, on a 60 second timeout.

We performed two series of experiments. In the first, we compared the static DP framework to the alternatives implemented in Wanda: no dependency pairs (so only rule removal using reduction orderings) and dynamic dependency pairs following [KopRaa12]. We compared both the power if only techniques discussed in the paper are used, if an additional delegation to a first-order prover is used, and if the methods are combined. This gives the following results:

Note that the non-termination processor has not yet been implemented in Wanda; non-termination verification is done exclusively through basic checks outside the DP frameworks, and by verifying the NO results of first-order delegation within the DP framework (see also our paper at FroCoS'11). This is why there are no NO results when only the techniques in the paper are enabled.

The second set of experiments aimed to assess the power of individual techniques within the static DP framework. To this end, we have run Wanda with only the techniques from the current paper five more times, each with one technique disabled. This gives the following result:

Note that, with the exception of reduction triples, none of the techniques seem to give much power when compared to the whole: it appears that for most benchmarks, several different techniques are feasible. This is emphasised by the following table, where we tested the power of Wanda when the use of a first-order tool was enabled. In this setting, we may even surrender the use of reduction triples without losing much power:

To further assess the strength of the individual methods, we have also run Wanda with only one or two techniques: either the subterm criterion or reduction triples, each coupled with nothing, the dependency graph, usable rules or formative rules. This provides the following results:

This reinforces the point that all techniques seem to add something, although the boost depends on what other techniques are available, and may be small.