Proving Non-looping Non-termination Automatically

摘要

We introduce a technique to prove non-termination of term rewrite systems automatically. Our technique improves over previous approaches substantially, as it can also detect non-looping non-termination.