Termination Analysis of Term Rewriting by Polynomial Interpretations and Matrix Interpretations

Die Frage der Terminierung von Algorithmen ist ein zentrales Problem in der Softwareentwicklung, und formale Methoden für die Terminierungsanalyse spielen bei der Verifikation von Computerprogrammen eine wichtige Rolle. In diesem Zusammenhang wurde in der jüngeren Vergangenheit viel Forschungsarbeit auf dem Gebiet der Termersetzung geleistet, einem konzeptionell einfachen, aber dennoch universellen Berechnungsmodell, für welches im Lauf der Zeit viele mächtige Methoden für die Erminierungsanalyse entwickelt wurden. Zwei davon, nämlich Polynominterpretationen und Matrixinterpretationen, werden im vorliegenden Buch einer genauen Analyse unterzogen. Es werden alle relevanten Forschungsergebnisse aus der Literatur präsentiert sowie einige offene Forschungsfragen im Zusammenhang mit der Terminierungsanalyse von Termersetzungssystemen beantwortet.