scientific article; zbMATH DE number 107881
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.
- Decision Procedures for Automating Termination Proofs
- Automata-Based Termination Proofs
- Automata-based termination proofs
- Automatizing termination proofs of recursively defined functions
- Modular and incremental automated termination proofs
- Automatic proofs of termination with elementary interpretations
- Certification of Automated Termination Proofs
- Automated termination proofs for logic programs by term rewriting
- On proving the termination of algorithms by machine
- Automatizing termination proofs of recursively defined functions
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- Decision Procedures for Automating Termination Proofs
- scientific article; zbMATH DE number 4072437 (Why is no real title available?)
- On automating inductive and non-inductive termination methods
- scientific article; zbMATH DE number 1748590 (Why is no real title available?)
- Termination of theorem proving by reuse
- Termination of algorithms over non-freely generated data types
- Extensions to the estimation calculus
- Automated modular termination proofs for real Prolog programs
- Automatic termination proofs with transformation orderings
- A Transformational Approach to Prove Outermost Termination Automatically
- How to make ad hoc proof automation less ad hoc
- Formalizing bounded increase
- A higher-order interpretation of deductive tableau
- Improving automation for higher-order proof steps
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4023458)
