All-Termination(T)

The authors introduce the All-Termination(T) problem: given a termination solver T and a collection of functions F, find every sub-set of the formal parameters to F whose consideration is sufficient to show, using T that F terminates. An important and motivating application is enhancing theorem proving systems by constructing the set of strongest induction schemes for F, modulo T. These schemes can be derived from the set of termination cores, the minimal sets returned by All-Termination(T), without any reference to an explicit measure function. They study the All-Termination(T) problem as applied to the Size-Change Termination analysis (SCT), a PSpace-complete problem that underlies many termination solvers.