Given a term rewriting system R, a term t is inductive reducible if every ground instance ts of it is reducible. A pair (t, s) of terms is inductive co-reducible if every ground instance (ts, ss) of it for which ts and ss are distinct, is reducible. Inductive (co)-reducibility has been proved to be the fundamental tool for mechanizing inductive proofs, together with Knuth-Bendix completion (Jouannaud and Kounalis [JK, 86 and 89]).
In [JK, 86 and 89] an algorithm for testing inductive reducibility is also presented which is tractable in pratical cases, but restricted to left-linear term rewriting systems. The solution of the inductive-(co)-reducibility problem, for the general case, turned out to be surprisingly complicated. Decidability of inductive reducibility for arbitrary term rewriting systems has been first proved by Plaisted [PLA, 85] and next by Kapur, Narendran, and Zhang [KNZ, 87]. However Plaisted's and Kapur, Narendran, and Zhang's algorithms amount to intractable computation, even in very simple cases.
We present here a new algorithm for the general case which outperforms Plaisted's and Kapur, Narendran and Zhang's algorithms and even our previous algorithm in case of a left-linear term rewriting system. We then show how to adapt it to check for inductive co-reducibility.