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.

• Type: Journal
• Year: 2012
• Where: CADE
• Authors: Fabian Emmes, Tim Enger, Jürgen Giesl
• Keywords: CADE 2012, Logical Reasoning