MUTERM

What inputs are supported?

Term Rewriting Systems (TRSs), Context-Sensitive Term Rewriting Systems (CS-TRSs), Order-Sorted Term Rewriting Systems (OS-TRSs), Associative or Commutative TRSs (AvC-TRSs), and Conditional Term Rewriting Systems (CTRSs) in TPDB or Maude format, see http://zenon.dsic.upv.es/muterm/index.php/documentation/

For which programming languages has it support?

Maude

What properties can be verified?

Termination and innermost termination of (context-sensitive) rewriting. Termination of rewriting modulo AvC theories. Termination and operational termination of conditional rewriting.

What are the tool’s main techniques for the supported (input, property) pairs?

Specialized Dependency Pair Frameworks for CS-TRSs, OS-TRSs, AvC-TRSs and CTRSs. (In)feasibility solvers. Generation of logical (possibly well-founded) models. Polynomial interpretations over the naturals and over the rationals. Matrix interpretations over the naturals and over the rationals. Context-Sensitive Recursive Path Ordering.

What external tools are used? (e.g., compilers, SMT solvers)

Barcelogic, Mace4, Prover9, infChecker, AGES

What is the tool’s URL?

http://zenon.dsic.upv.es/muterm/

Example(s)

A CTRS in TPDB format:

(VAR X Y)

(RULES

h(d) -> c(a)

h(d) -> c(b)

f(k(a),k(b),X) -> f(X,X,X)

g(X) -> k(Y) | h(X) -> d , h(X) -> c(Y)

)

Other relevant information

References

The last system description was published in proc. of IJCAR 2020, LNCS 12167:436-447, 2020