2026-07-20T11:27:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5205 2024-03-06T10:36:03Z ddc:004 open_access

Matrix Interpretations on Polyhedral Domains Waldmann, Johannes termination of term rewriting matrix interpretations constraint programming linear inequalities 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Johannes Waldmann 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.318 urn:nbn:de:0030-drops-52059 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.318 eng https://creativecommons.org/licenses/by/3.0/legalcode