AProVE is a system for automated termination and innermost termination proofs of term rewrite systems (TRSs).
AProVE is based on the dependency pair framework and offers a wide variety of different termination proof techniques. These techniques can be freely configured and combined by the user via a graphical user interface. Moreover, AProVE also offers a "fully automatic" mode where suitable termination techniques are applied in a certain fixed order that often turns out to be successful in practice.
· Java runtime system version 1.5 or newer
Untar the archive.
Start AProVE with
java -jar AProVE.jar
If AProVE crashes because of not enough memory, you should start AProVE with the -XmxNm option which allows java and therefore AProVE to use N megabytes of memory. For example,
java -Xmx400m -jar AProVE.jar
starts AProVE with a memory limit of 400 megabytes. Without this option the default limit is used which is quite low.