Linear termination is undecidable

DOI10.1145/3661814.3662081MaRDI QIDQ6970215zbMATH OpenFDO

Authors Fabian Mitterwallner, Aart Middeldorp, René Thiemann

Publication date 18 June 2025

Full work available at URL https://doi.org/10.1145/3661814.3662081

zbMATH Keywords

polynomial terminationterm rewritingundecidability

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Grammars and rewriting systems (68Q42)

Cites work

• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Decision problems for semi-Thue systems with a few rules
• Extending Sledgehammer with SMT solvers
• scientific article; zbMATH DE number 1722702 (Why is no real title available?)
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Matrix interpretations for proving termination of term rewriting
• Max/Plus tree automata for termination of term rewriting
• Omega-termination is undecidable for totally terminating term rewriting systems
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• On transfinite Knuth-Bendix orders
• Ordinals and Knuth-Bendix orders
• Orienting rewrite rules with the Knuth-Bendix order.
• Polynomial interpretations over the natural, rational and real numbers revisited
• Polynomial termination over \(\mathbb{N}\) is undecidable
• Polynomials over the reals in proofs of termination : from theory to practice
• Relative undecidability in term rewriting. I: The termination hierarchy
• Simple termination is difficult
• Simulation of Turing machines by a regular rewrite rule
• Sledgehammer: judgement day
• Term Rewriting and All That
• Termination of rewriting
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination of term rewriting using dependency pairs
• Termination of term rewriting: Interpretation and type elimination
• Termination proofs and the length of derivations
• The DPRM Theorem in Isabelle (Short Paper).
• Total termination of term rewriting is undecidable

This page was built for publication: Linear termination is undecidable

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