Das Fuhren von Terminierungsbeweisen flir rekursiv definierte
Algorithmen erfordert eine gewisse Kreativitiit des (menschlichen oder
automatischen) Bewei- sers, die sich im Erfinden einer Hypothese
manifestiert, deren Giiltigkeit hinrei- chend flir die Terminierung
eines Algorithmus ist. In dieser Arbeit wird ein Ver- fahren
vorgestellt, mit dem diese KreativiUit durch ein Computerprogramm
nachgebildet werden soIl. Mit diesem Verfahren konnen
Terminierungsbeweise in vielen Hillen vollautomatisch, d.h. ohne
jegliche menschliche Unterstutzung, gefiihrt werden. Es wird gezeigt, -
wie flir einen Algorithmus eine Terminierungshypothese automatisch
synthetisiert werden kann, - welches Wissen uber Algorithmen dazu
erforderlich ist, - wie dieses Wissen reprasentiert wird, und - wie
dieses Wissen durch eine Maschine selbst berechnet werden kann. Das hier
beschriebene Verfahren lOst die gestellte Aufgabe fUr eine relevante
Klasse von Algorithmen, wie etwa klassische Sortieralgorithmen und
Algorith- men flir grundlegende arithmetische Operationen, die in einer
rein funktionalen Programmiersprache gegeben sind. Die hier vorliegende
Arbeit, die in den Jahren 1984 -1988 entstand, wurde zum Teil durch den
Sonderforschungsbereich 314 "Kunstliche Intelligenz und Wissensbasierte
Systeme" der Deutschen Forschungsgemeinschaft gefOrdert und von der
Fakultat flir Informatik der Universitat Karlsruhe als Habilitations-
schrift angenommen. Ich danke Prof. Dr. P. Deussen flir die
Arbeitsmoglichkei- ten und Unterstiitzung wahrend der Jahre an seinem
Institut.
