THOR.
Developed by Cristina Borralleras and Albert Rubio.
THOR is an automatic tool for proving Termination of Higher-Order
Rewriting. It ranked first in the 2010 International Termination
Competition ( termComp ) in the
Higher-Order category.
NEW HORPO.
Developed by Frédéric Blanqui, Jean-Pierre Jouannaud and Albert Rubio.
It is an implementation written in GNU-Prolog of the new more powerful version of the Higher-Order Recursive Path Ordering.
HORPO.
Developed by Jean-Pierre Jouannaud and Albert Rubio.
It is an implementation written in GNU-Prolog of the Higher-Order
Recursive Path Ordering.
TERMPTATION (TERMination
Proof Techniques
automATION)
is a
fully automated system for
proving
termination (and innermost termination) of term rewrite systems
(developed
by C. Borralleras and A. Rubio). New version: Feb 2003.
The TerminationLab (developed by
P.
Nivela,
R. Nieuwenhuis and A. Rubio) is a termination proof checker based on
the MSPO
method (by C. Borralleras, M.
Ferreira
and A. Rubio)
Problems:
Have a look at TPDB
the
Termination Problem Data Base. It
provides
a variety of test problems on termination of processes (logic and
functional
programs, rewrite systems,...).