License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.318
URN: urn:nbn:de:0030-drops-52059
URL: http://drops.dagstuhl.de/opus/volltexte/2015/5205/
Go to the corresponding LIPIcs Volume Portal


Waldmann, Johannes

Matrix Interpretations on Polyhedral Domains

pdf-format:
25.pdf (0.5 MB)


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: 17.06.2015


DROPS-Home | Fulltext Search | Imprint Published by LZI