WANDA is a tool aimed to prove termination of higher-order term rewriting systems, using both recent and less recent scientific results. She is designed to compete in the annual termination competition.
- a dual dependency pair framework, combining static and dynamic dependency pairs
- automatic search for suitable polynomial interpretations
- a higher-order recursive path ordering with minimal symbols
- partial conversion to a first-order termination problem
- the subterm criterion
- usable rules
- formative rules
- a bound-variable-conscious dependency graph approximation
- (minor) non-termination analysis
WANDA uses an external SAT-solver to find reduction pairs and a projection function for the subterm criterion, as well as an external first-order termination tool. Both can be replaced by alternative solvers.
The current version of WANDA is 2.1. Downloads are built for and compiled on linux.