Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering

This publication has 27 references indexed in Scilit:

• Proving Confluence of Term Rewriting Systems Automatically
  2009
• Mechanizing and Improving Dependency Pairs
  Journal of Automated Reasoning, 2007
• Mechanically Proving Termination Using Polynomial Interpretations
  Journal of Automated Reasoning, 2005
• Proving and Disproving Termination of Higher-Order Functions
  Lecture Notes in Computer Science, 2005
• The confluence of ground term rewrite systems is decidable in polynomial time
  2001
• Termination of term rewriting using dependency pairs
  Theoretical Computer Science, 2000
• Term Rewriting and All That
  1998
• Decidable approximations of sets of descendants and sets of normal forms
  Lecture Notes in Computer Science, 1998
• Decidable call by need computations in term rewriting (extended abstract)
  1997
• Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
  Information and Computation, 1990