2002 | OriginalPaper | Chapter
Relative Undecidability
Author : Enno Ohlebusch
Published in: Advanced Topics in Term Rewriting
Publisher: Springer New York
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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?