Argument Filterings and Usable Rules for Simply Typed Dependency Pairs

DOI10.1007/978-3-642-04222-5_7zbMath1193.68142MaRDI QIDQ3655195

Toshiyuki Yamada, Takahito Aoto

Publication date: 7 January 2010

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04222-5_7

Mathematics Subject Classification ID

68Q42: Grammars and rewriting systems

Related Items

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs, Argument Filterings and Usable Rules for Simply Typed Dependency Pairs

Uses Software

• Tyrolean
• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Comparing curried and uncurried rewriting
• Termination of term rewriting using dependency pairs
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Modular and incremental automated termination proofs
• Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
• Proving Termination Using Recursive Path Orders and SAT Solving
• Solving Partial Order Constraints for LPO Termination
• Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
• Frontiers of Combining Systems
• Uncurrying for Termination
• Term Rewriting and Applications
• Rewriting Techniques and Applications