Automatisierung von Terminierungsbeweisen

Inhaltsverzeichnis 1 Einleitung 1.1 Ein Terminierungsbeweis für einen Sortieralgorithmus 1.2 Das Termenierungsverfahren — Ein Überblick 1.3 Bibliographische Anmerkungen und verwandte Arbeiten 2 Syntaktische und semantische Begriffe 2.1 Syntaktische Definitionen 2.2 Semantik der Sprache erster Stufe 2.3 Standardalgebren und Standardmodelle 2.4 Fundierte Ordnungen 3 Spezifikationen 3.1 Datenstrukturen 3.2 Algorithmen 3.3 Normalformen für Algorithmen 3.4 Zulässige Spezifikationen und Beweisen durch Induktion 3.5 Zusammenfassung 4 Beweisen durch Abschätzen mit dem E-Kalkül 4.1 Die Anzahlordnung 4.2 Abschätzungen durch argumentbeschränkte Operationen 4.3 Differenzliterale für argumentbeschränkte Operationen 4.4 Abschätzungen durch Datenstrukturen 4.5 Formale Definition und Korrektheit des E-Kalküls 4.6 Das Differenzäquivalent 4.7 Ein Beweisverfahren für den E-Kalkül 4.8 Zusammenfassung 5 Erzeugung von Terminierungshypothesen 5.1 Terminierungshypothesen durch Abschätzungen 5.2 Ein Terminierungskriterium mit Termrepräsentanten 5.3 Algorithmen in positiver Strukturnormalform 5.4 Lexikographische Terminierungsordnungen 5.5 Terminierungshypothesen für das ‘Sort’-Beispiel 5.6 Zusammenfassung 6 Erkennen argumentbeschränkter Operationen 6.1 Reflexive Selektoren 6.2 Argumentbeschränkte Algorithmen 6.3 Synthese von Differenzalgorithmen 6.4 Zusamme