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.
Contact: Frédéric Blanqui.