Termination of term rewriting: Interpretation and type elimination
From MaRDI portal
Publication:1332336
DOI10.1006/jsco.1994.1003zbMath0810.68087OpenAlexW2041799549MaRDI QIDQ1332336
Publication date: 10 October 1994
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/904bcda0a109ea3b0482b3d30d3cb849372433cc
Related Items (49)
mu-term: Verify Termination Properties Automatically (System Description) ⋮ A complete characterization of termination of 0p 1q→1r 0s ⋮ Problems in rewriting III ⋮ Termination of constructor systems ⋮ Dummy elimination in equational rewriting ⋮ Dummy elimination: Making termination easier ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ Termination of string rewriting proved automatically ⋮ An initial algebra approach to term rewriting systems with variable binders ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Total termination of term rewriting ⋮ Termination of Cycle Rewriting by Transformation and Matrix Interpretation ⋮ Elimination transformations for associative-commutative rewriting systems ⋮ A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy ⋮ Layer Systems for Proving Confluence ⋮ Modularity in term rewriting revisited ⋮ Termination modulo equations by abstract commutation with an application to iteration ⋮ Simple termination of rewrite systems ⋮ An upper bound on the derivational complexity of Knuth-Bendix orderings. ⋮ Levels of undecidability in rewriting ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Normalization of Infinite Terms ⋮ Matrix interpretations for proving termination of term rewriting ⋮ The order types of termination orderings on monadic terms, strings and multisets ⋮ Termination of term rewriting using dependency pairs ⋮ Logic programming with function symbols: Checking termination of bottom-up evaluation through program adornments ⋮ Transforming termination by self-labelling ⋮ Match-bounded string rewriting systems ⋮ Explicit Substitutions à la de Bruijn ⋮ Lazy productivity via termination ⋮ Operational Termination of Membership Equational Programs: the Order-Sorted Way ⋮ An automated approach to the Collatz conjecture ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ The Hydra battle and Cichon's principle ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ Proving Confluence of Term Rewriting Systems Automatically ⋮ Proving Infinitary Normalization ⋮ Transforming SAT into Termination of Rewriting ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ Invariants, patterns and weights for ordering terms ⋮ Relative undecidability in term rewriting. I: The termination hierarchy ⋮ Relative undecidability in term rewriting. II: The confluence hierarchy ⋮ Tuple interpretations for termination of term rewriting ⋮ Modular termination proofs for rewriting using dependency pairs ⋮ Undecidable Properties on Length-Two String Rewriting Systems ⋮ Domain expansion for ASP-programs with external sources ⋮ Termination by absence of infinite chains of dependency pairs
This page was built for publication: Termination of term rewriting: Interpretation and type elimination
