| Erasure for Termination Proofs (2007) | |||||||||||||||
Abstract | |||||||||||||||
| . Weintroduce a technique to facilitate termination proofs for term rewriting systems. We especially focus on innermost termination. The main features of this technique lie in its simplicity and e#ectiveness in practice. This work can be regarded as an application of the general notion termination through transformation to both termination and innermost termination proofs. 1 Introduction It is a highly signi#cant question to determine whether a term rewriting system #TRS# is terminating. In theorem proving, TRSs are widely used for a variety of purposes. For instance, it is often desirable to transform a set of equality rules into a TRS in order to reduce the search space. Also TRSs can be used for proving the termination of both functional and logic programs. Though termination is an undecidable property of TRSs in general, there have been many techniques developed for facilitating termination proofs. Some surveys are given in #Der87,Ste95b#. As mentioned in #MOZ96#, techniques... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||