License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.36
URN: urn:nbn:de:0030-drops-123587
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12358/
Go to the corresponding LIPIcs Volume Portal

Kop, Cynthia

WANDA - a Higher Order Termination Tool (System Description)

pdf-format:
LIPIcs-FSCD-2020-36.pdf (0.7 MB)

Abstract

Wanda is a fully automatic termination analysis tool for higher-order term rewriting. In this paper, we will discuss the methodology used in Wanda. Most pertinently, this includes a higher-order dependency pair framework and a variation of the higher-order recursive path ordering, as well as some non-termination analysis techniques and delegation to a first-order tool. Additionally, we will discuss Wanda’s internal rewriting formalism, and how to use Wanda in practice for systems in two different formalisms. We also present experimental results that consider both formalisms.

BibTeX - Entry

@InProceedings{kop:LIPIcs:2020:12358,
  author =	{Cynthia Kop},
  title =	{{WANDA - a Higher Order Termination Tool (System Description)}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12358},
  URN =		{urn:nbn:de:0030-drops-123587},
  doi =		{10.4230/LIPIcs.FSCD.2020.36},
  annote =	{Keywords: higher-order term rewriting, termination, automatic analysis, dependency pair framework, higher-order recursive path ordering}
}

Keywords: higher-order term rewriting, termination, automatic analysis, dependency pair framework, higher-order recursive path ordering
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: A detailed experimental evaluation and the snapshot of Wanda used in this paper are available from: https://www.cs.ru.nl/~cynthiakop/experiments/fscd20.

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