In order to motivate relative undecidability, let us consider the following scenario. All methods for proving termination of a TRS ℛ fail but an implementation of the dependency pair method is able to prove innermost termination of ℛ automatically. In view of the fact that nonterminating but innermost terminating systems hardly occur in practice, it is most likely that ℛ is in fact terminating. But how can we prove this?
KeywordsNormal Form Function Symbol Ground Term Strict Monotonicity Ground Instance
Unable to display preview. Download preview PDF.