On tree automata that certify termination of left-linear term rewriting systems

DOI10.1016/J.IC.2006.08.007zbMATH Open1112.68077OpenAlexW2111433946MaRDI QIDQ876043FDOQ876043

Dieter Hofbauer, Hans Zantema, Alfons Geser, Johannes Waldmann

Publication date: 16 April 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2006.08.007

zbMATH Keywords

tree automataterm rewriting systemsterminationforward closuresrewrite labellings

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Termination of context-sensitive rewriting
• Reachability analysis over term rewriting systems
• Term Rewriting and Applications
• Deleting string rewriting systems preserve regularity
• Decidability for left-linear growing term rewriting systems.
• Term Rewriting and Applications
• Match-bounded string rewriting systems
• Termination of string rewriting proved automatically
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS
• Approximations for strategies and termination

Cited In (15)

• Match-bounds revisited
• Increasing Interpretations
• Automatic Termination
• A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems
• Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
• Beyond Dependency Graphs
• Proving Quadratic Derivational Complexities Using Context Dependent Interpretations
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Increasing interpretations
• Symbol different term rewrite systems
• Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems
• Automated Complexity Analysis Based on the Dependency Pair Method
• From Outermost Termination to Innermost Termination
• Title not available (Why is that?)
• Reachability, confluence, and termination analysis with state-compatible automata

Uses Software

• Timbuk
• Chaff
• Tyrolean
• AProVE
• CiME
• TPDB
• Matchbox
• TORPA

This page was built for publication: On tree automata that certify termination of left-linear term rewriting systems

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