Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

Friedrich Neurauter & Aart Middeldorp
Matrix interpretations are a powerful technique for proving termination of term rewrite systems, which is based on the well-known paradigm of interpreting terms into a domain equipped with a suitable well-founded order, such that every rewrite step causes a strict decrease. Traditionally, one uses vectors of non-negative numbers as domain, where two vectors are in the order relation if there is a strict decrease in the respective first components and a weak decrease in all...
This data center is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.
We found no citations for this text. For information on how to provide citation information, please see our documentation.