On the formalization of termination techniques based on multiset orderings

DOI10.4230/LIPICS.RTA.2012.339MaRDI QIDQ5111915zbMATHOpenAlexFDO

Authors 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

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)

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

Cited in

(5)

• Reducing relative termination to dependency pair problems
• Relative termination via dependency pairs
• AC-KBO revisited
• A framework for developing stand-alone certifiers
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)

Describes a project that uses

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)