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: https://drops.dagstuhl.de/opus/volltexte/2020/12358/
Kop, Cynthia
WANDA - a Higher Order Termination Tool (System Description)
| pdf-format: |
|
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 | |
| Seminar: | 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. |
