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.

WANDA features:

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.