The Maude Termination Assistant


We present the Maude Termination Assistant (MTA). Its purpose is to complement the fully automatic Maude Termination Tool (MTT) [2] in two ways: (i) to help users find a proof when MTT may not find one; and (ii) for teaching purposes. The main features supported by MTA are: (1) termination proofs of order-sorted equational theories, which may include conditional rules without extra variables; (2) such proofs can be modulo any combination of associativity and/or commutativity and/or identity axioms; (3) identity axioms are automatically transformed into rules by a semantics-preserving theory transformation; (4) support for user-specified recursive path orders modulo any combination of the above axioms; and (5) support for user-specified linear polynomial orders modulo any combination of the above axioms.


We have provided a tar archive of our code with example files. The examples will run with version 2.7.1 of Maude (and probably newer versions as well). Binaries and source are downloadable from the Maude website.


Once you have downloaded the Maude binary and code archive, to run the tool, following four easy steps:

  1. Take a Maude module in some file (say the module FOO in file foo.maude ) that you wish to analyze and annotate each operator in FOO with a metadata attribute that defines how the operators are to be ordered.
  2. Load the Maude file you just annontated into the Maude interpreter by typing
     $ maude ~/ex/foo.maude 
    at the command prompt, assuming your example is in a folder ex which is a subdirectory of your home folder and that the Maude binary is located on your PATH.
  3. Initialize the MTA tool by typing
     Maude> load ~/mta/mta.maude 
    at the Maude prompt, assuming you unzipped the tool tarball inside your home folder.
  4. Check module termination using the AvC-RPO or polynomial orderings using the commands:
    1.  (check-poly FOO .) 
    2.  (check-AvCrpo FOO .) 
Alternatively, to run one of preloaded examples in the archive, you can do:
$ maude ~/mta/test/acrpo/example_name.maude
$ maude ~/mta/test/poly/example_name.maude
assuming that you unzipped the tool tarball in your home folder and that the Maude binary is located on your PATH. This is because the examples load the tool for you and have the termination check commands already embedded inside of them.