HOT is an automated termination prover for higher-order rewriting, based on the notion of computability closure (see papers below).

It accepts as input termination problems in the termination competition format XTC and also a simpler home-made text format.

On 29 June 2012, HOT won the international termination competition in the category "higher-order rewriting".

On 14 June 2012, on the competition platform, it can prove in 171s the (non) termination of 130/156=83% of the higher-order termination problems of the termination competition database TPDB 8.0.1.

Scientific background:

Contact: Frédéric Blanqui.

Statcounter W3C Validator Last updated on 26 November 2015. Come back to main page.