On the formalization of termination techniques based on multiset orderings

DOI10.4230/LIPICS.RTA.2012.339zbMATH Open1437.68088OpenAlexW1533854855MaRDI QIDQ5111915FDOQ5111915

René Thiemann, Guillaume Allais, Julian Nagele

Publication date: 27 May 2020

Full work available at URL: https://dx.doi.org/10.4230/LIPIcs.RTA.2012.339

Recommendations

• scientific article; zbMATH DE number 794239
• scientific article; zbMATH DE number 2185669
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Extension functions for multiset orderings
• scientific article; zbMATH DE number 408817

zbMATH Keywords

term rewritingterminationformalizationmultiset orderings

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Cited In (5)

• A framework for developing stand-alone certifiers
• Title not available (Why is that?)
• Relative termination via dependency pairs
• AC-KBO revisited
• Reducing Relative Termination to Dependency Pair Problems

Uses Software

• Isabelle

This page was built for publication: On the formalization of termination techniques based on multiset orderings

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