License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2012.339
URN: urn:nbn:de:0030-drops-35029
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3502/
Go to the corresponding LIPIcs Volume Portal

Thiemann, René ; Allais, Guillaume ; Nagele, Julian

On the Formalization of Termination Techniques based on Multiset Orderings

pdf-format:
25.pdf (0.5 MB)

Abstract

Multiset orderings are a key ingredient in certain termination
techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle
Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions.

Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.

BibTeX - Entry

@InProceedings{thiemann_et_al:LIPIcs:2012:3502,
  author =	{Ren{\'e} Thiemann and Guillaume Allais and Julian Nagele},
  title =	{{On the Formalization of Termination Techniques based on Multiset Orderings}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
  pages =	{339--354},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Ashish Tiwari},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3502},
  URN =		{urn:nbn:de:0030-drops-35029},
  doi =		{10.4230/LIPIcs.RTA.2012.339},
  annote =	{Keywords: formalization, term rewriting, termination, orderings}
}

Keywords: formalization, term rewriting, termination, orderings
Collection: 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Issue Date: 2012
Date of publication: 29.05.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI