Relative Undecidability

  • Enno Ohlebusch


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?


Normal Form Function Symbol Ground Term Strict Monotonicity Ground Instance 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2002

Authors and Affiliations

  • Enno Ohlebusch
    • 1
  1. 1.Research Group in Practical Computer Science, Faculty of TechnologyUniversity of BielefeldBielefeldGermany

Personalised recommendations