Wanda -- a higher-order termination tool (system description)

DOI10.4230/LIPICS.FSCD.2020.36MaRDI QIDQ6854397zbMATH OpenFDO

Authors Cynthia Kop

Publication date 24 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2020.36

zbMATH Keywords

automatic analysisdependency pair frameworkhigher-order recursive path orderinghigher-order term rewritingtermination

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX) Theory of computing (68Qxx)

Cites work

• A Higher-Order Iterative Path Ordering
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A Monotonic Higher-Order Semantic Path Ordering
• A static higher-order dependency pair framework
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Argument filterings and usable rules for simply typed dependency pairs
• Certification of Termination Proofs Using CeTA
• Combinatory reduction systems: Introduction and survey
• Counterexamples to termination for the direct sum of term rewriting systems
• Dynamic dependency pairs for algebraic functional systems
• Frontiers of Combining Systems
• Guided unfoldings for finding loops in standard term rewriting
• Harnessing first order termination provers using higher order dependency pairs
• scientific article; zbMATH DE number 996558 (Why is no real title available?)
• scientific article; zbMATH DE number 4092757 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• scientific article; zbMATH DE number 1761896 (Why is no real title available?)
• scientific article; zbMATH DE number 794237 (Why is no real title available?)
• Inductive-data-type systems
• Iterative Lexicographic Path Orders
• Logic for Programming, Artificial Intelligence, and Reasoning
• Loop detection in term rewriting using the eliminating unfoldings
• On the formalization of termination techniques based on multiset orderings
• Operational termination of conditional term rewriting systems
• Orderings for term-rewriting systems
• Polynomial interpretations for higher-order rewriting
• Proving Non-looping Non-termination Automatically
• Proving termination by dependency pairs and inductive theorem proving
• Rewriting Techniques and Applications
• Simplifying algebraic functional systems
• Termination of context-sensitive rewriting
• Termination of term rewriting using dependency pairs
• The Computability Path Ordering: The End of a Quest
• Theory and Applications of Satisfiability Testing

Cited in

(3)

• Sort-based confluence criteria for non-left-linear higher-order rewriting
• The computability path order for beta-eta-normal higher-order rewriting
• Higher-order constrained dependency pairs for (universal) computability

This page was built for publication: Wanda -- a higher-order termination tool (system description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6854397)