Simulating dependency pairs by semantic labeling

DOI10.4230/LIPICS.FSCD.2024.13MaRDI QIDQ6875000zbMATH OpenFDO

Authors Nao Hirokawa

Publication date 14 January 2026

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

dependency pairsrelative terminationsemantic labelingterm rewriting

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A dependency pair framework for \(A \vee C\)-termination
• A fully syntactic AC-RPO.
• A static higher-order dependency pair framework
• AC dependency pairs revisited
• Automating the dependency pair method
• Certifying the weighted path order (invited talk)
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• scientific article; zbMATH DE number 1670496 (Why is no real title available?)
• scientific article; zbMATH DE number 3921960 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 794240 (Why is no real title available?)
• Labelings for decreasing diagrams
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic Programming
• On the formalization of termination techniques based on multiset orderings
• Orderings for term-rewriting systems
• Relative termination via dependency pairs
• Signature extensions preserve termination. An alternative proof via dependency pairs
• Termination by absence of infinite chains of dependency pairs
• Termination of term rewriting using dependency pairs
• Transforming termination by self-labelling

This page was built for publication: Simulating dependency pairs by semantic labeling

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