Transforming termination by self-labelling

DOI10.1007/3-540-61511-3_101zbMath1412.68112OpenAlexW2024932951MaRDI QIDQ4647535

Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://dspace.library.uu.nl/handle/1874/18323

zbMATH Keywords

semantic labellingreduction orderfunction symbolinduction hypothesisdistribution rule

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (6)

Extending reduction orderings to ACU-compatible reduction orderings ⋮ Size-based termination of higher-order rewriting ⋮ Root-Labeling ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Termination by completion
• Termination of rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• Termination of term rewriting: Interpretation and type elimination
• Modular proofs for completeness of hierarchical term rewriting systems
• Modular properties of composable term rewriting systems
• Dummy elimination: Making termination easier
• On the Church-Rosser property for the direct sum of term rewriting systems

This page was built for publication: Transforming termination by self-labelling