Beyond Dependency Graphs

DOI10.1007/978-3-642-02959-2_26zbMath1250.68143OpenAlexW1536239557MaRDI QIDQ5191112

Martin Korp, Aart Middeldorp

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_26

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Proving termination by dependency pairs and inductive theorem proving

Uses Software

• Tyrolean
• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Tyrolean termination tool: techniques and features
• On tree automata that certify termination of left-linear term rewriting systems
• Mechanizing and improving dependency pairs
• Match-bounds revisited
• Decidability for left-linear growing term rewriting systems.
• Decidable call-by-need computations in term rewriting
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
• Term Rewriting and All That
• Proving Termination of Rewrite Systems Using Bounds
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS
• Frontiers of Combining Systems
• Logic for Programming, Artificial Intelligence, and Reasoning