2026-07-22T10:50:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12358 2024-03-06T10:50:03Z ddc:004 open_access

WANDA - a Higher Order Termination Tool (System Description) Kop, Cynthia higher-order term rewriting termination automatic analysis dependency pair framework higher-order recursive path ordering 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Cynthia Kop 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.36 urn:nbn:de:0030-drops-123587 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.36 eng https://creativecommons.org/licenses/by/3.0/legalcode