Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.318
URN: urn:nbn:de:0030-drops-52059
URL: https://drops.dagstuhl.de/opus/volltexte/2015/5205/
Waldmann, Johannes
Matrix Interpretations on Polyhedral Domains
| pdf-format: |
|
Abstract
We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities. Admissibility of such a restriction is shown by certificates whose validity can be expressed as a constraint program. This refinement is orthogonal to other features of matrix interpretations (complexity bounds, dependency pairs), but can be used to improve complexity bounds, and we discuss its relation with the usable rules criterion. We present an implementation and experiments.
BibTeX - Entry
@InProceedings{waldmann:LIPIcs:2015:5205,
author = {Johannes Waldmann},
title = {{Matrix Interpretations on Polyhedral Domains}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {318--333},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Maribel Fern{\'a}ndez},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5205},
URN = {urn:nbn:de:0030-drops-52059},
doi = {10.4230/LIPIcs.RTA.2015.318},
annote = {Keywords: termination of term rewriting, matrix interpretations, constraint programming, linear inequalities}
}
| Keywords: | termination of term rewriting, matrix interpretations, constraint programming, linear inequalities | |
| Seminar: | 26th International Conference on Rewriting Techniques and Applications (RTA 2015) | |
| Issue date: | 2015 | |
| Date of publication: | 18.06.2015 |
