License
when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.203
URN: urn:nbn:de:0030-drops-31177
URL: http://drops.dagstuhl.de/opus/volltexte/2011/3117/

Kop, Cynthia ; van Raamsdonk, Femke

Higher Order Dependency Pairs for Algebraic Functional Systems

pdf-format:
Dokument 1.pdf (664 KB)


Abstract

We extend the termination method using dynamic dependency pairs to higher order rewriting systems with beta as a rewrite step, also called Algebraic Functional Systems (AFSs). We introduce a variation of usable rules, and use monotone algebras to solve the constraints generated by dependency pairs. This approach differs in several respects from those dealing with higher order rewriting modulo beta (e.g. HRSs).

BibTeX - Entry

@InProceedings{kop_et_al:LIPIcs:2011:3117,
  author =	{Cynthia Kop and Femke van Raamsdonk},
  title =	{{Higher Order Dependency Pairs for Algebraic Functional Systems}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{203--218},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3117},
  URN =		{urn:nbn:de:0030-drops-31177},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2011.203},
  annote =	{Keywords: higher order rewriting, termination, dynamic dependency pairs}
}

Keywords: higher order rewriting, termination, dynamic dependency pairs
Seminar: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue date: 2011
Date of publication: 26.04.2011


DROPS-Home | Fulltext Search | Imprint Published by LZI