On the formalization of termination techniques based on multiset orderings

DOI10.4230/LIPICS.RTA.2012.339MaRDI QIDQ5111915zbMATH OpenOpenAlexFDO

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

formalizationmultiset orderingsterm rewritingtermination

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

(11)

• Relative termination via dependency pairs
• Reducing relative termination to dependency pair problems
• AC-KBO revisited
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• A framework for developing stand-alone certifiers
• Wanda -- a higher-order termination tool (system description)
• Certifying the weighted path order (invited talk)
• Simulating dependency pairs by semantic labeling
• Inferring RPO symbol orderings
• The Generalized Multiset Ordering is NP-Complete
• A Formalization of Weighted Path Orders and Recursive Path Orders

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)