WANDA is a tool for proving or disproving higher-order termination.
It was created by Cynthia Kop as part of the HOT (Higher-Order
Termination) project from the VU University Amsterdam, which was
supported by the Netherlands Organisation for Scientific Research
(NWO-EW) under grant 612.000.629.

Full documentation of the techniques used in WANDA 2.2 is given in the
paper "WANDA -- a Higher Order Termination Tool" by Cynthia Kop, which
is included in this release.  The details of the techniques largely
appear in the PhD thesis "Higher-Order Termination" by Cynthia Kop.
Citations to additional theory are provided by the tool when used.

As back-ends, WANDA uses:
* a sat-solver (resources/satsolver): this is the open-source tool
  MiniSat, which is available from http://minisat.se
  (MIT licence)
* a first-order termination prover (resources/firstorderprover), and an
  additional non-termination prover that gives an explicit counterexample when
  possible; for both tools, a version of the closed-source tool AProVE is
  included in this release
* a small script to timeout external calls when they take too long:
  this is the script timeout, which is available from
  http://www.odi.ch/prog/timeout.php

Both the sat-solver and the termination prover can be replaced by
other tools, provided these tools satisfy the formats of the
corresponding competitions.  The timeout script, too, can be
replaced by any tool with the same interface.  More information about
those external tools can be found in resources/NOTICE.

All licences are available in the licences/ directory.  WANDA herself
is released under the Apache licence.

If the executables do not work, then you should be able to compile
WANDA from the source by typing "make" in the main directory.  To
get the back-ends compiled, see the relevant information in
resources/NOTICE.

