No label defined (Q4023458)

This is the German translation of the original English habilitation thesis presented by the author to the faculty of Computer Science at the University of Karlsruhe. The presentation is highly formal and technical. As indicated by the title the author is concerned with proving termination properties for algorithms. This task consists of several parts, but the author is mainly concerned with the (automatical) generation of hypotheses which are sufficient for the termination of an algorithm. Then one has to apply an inductive theorem proving system in order to verify the termination hypothesis. The book is organized as follows: Chapter I contains the introduction, Chapter II reviews syntactical and semantical concepts. In Chapter III the author introduces specifications as a means to describe data structures and algorithms. In Chapter IV an estimation calculus is developed which allows one to prove inequalities for founded orders. In Chapter V the estimation calculus is applied in order to automatically generate termination hypotheses for argument bounded algorithms. Chapter VI explains how to recognize whether an algorithm is argument bounded. The author develops a difference algorithm which decides (for argument bounded algorithms) if the output value is smaller (with respect to the founded order) than the input value at each step of the recursion. In Chapter VII an induction proving system is used to optimize the difference algorithm. If a user defines an algorithm which computes an argument bounded function without being bounded itself then the author's approach will fail in general. In Chapter VIII, however, he discusses cases where in this situation it is possible to modify the algorithm so as to make its argument bounded. The last chapter explains how one would have to implement the whole system. There are three appendices: the first one collects background material, the second one contains proofs of more complicated theorems, and the last one contains a collection of algorithms and the termination hypotheses which are automatically generated for these algorithms.