Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations

Georg Moser, Andreas Schnabl & Johannes Waldmann
For a given (terminating) term rewriting system one can often estimate its \emph{derivational complexity} indirectly by looking at the proof method that established termination. In this spirit we investigate two instances of the interpretation method: \emph{matrix interpretations} and \emph{context dependent interpretations}. We introduce a subclass of matrix interpretations, denoted as \emph{triangular matrix interpretations}, which induce polynomial derivational complexity and establish tight correspondence results between a subclass of context dependent interpretations and restricted triangular matrix interpretations....
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.