ON PROVING THE TERMINATION OF ALGORITHMS BY MACHINE

Proving the termination of a recursively defined algorithm requires a certain creativity of the (human or automated) reasoner for inventing a hypothesis whose truth implies that the algorithm terminates. We pre sent a reasoning method for simulating this kind of creativity by mach ine. The proposed method works automatically, i.e. without any human s upport. We show, (1) how a termination hypothesis for an algorithm is synthesized by machine, (2) which knowledge about algorithms is requir ed for an automated synthesis, and (3) how this knowledge is computed. Our method solves the problem for a relevant class of algorithms, inc luding classical sorting algorithms and algorithms for standard arithm etical operations, which are given in a pure functional notation. The soundness of the method is proved and several examples are presented f or illustrating the performance of the proposal. The method has been i mplemented and proved successful in practice.