All-Termination(T)

We introduce the

All-Termination

(

T

) problem: given a termination solver

T

and a collection of functions

F

, find every subset 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. We study the

All-Termination

(

T

) problem as applied to the size-change termination analysis (

$\mathit{SCT}$

), a

PSpace

-complete problem that underlies many termination solvers. Surprisingly, we show that

All-Termination

$(\mathit{SCT})$

is also

PSpace

-complete, even though it substantially generalizes

$\mathit{SCT}$

. We develop a practical algorithm for

All-Termination

$(\mathit{SCT})$

, and show experimentally that on the ACL2 regression suite (whose size is over 100MB) our algorithm generates stronger induction schemes on 90% of multiargument functions.