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
- 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.
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
fully automated system for
termination (and innermost termination) of term rewrite systems
by C. Borralleras and A. Rubio). New version: Feb 2003.
- The TerminationLab (developed by
R. Nieuwenhuis and A. Rubio) is a termination proof checker based on
method (by C. Borralleras, M.
and A. Rubio)
Have a look at TPDB
Termination Problem Data Base
a variety of test problems on termination of processes (logic and
programs, rewrite systems,...).