| Freezing - Termination Proofs for Classical, Context-Sensitive and Innermost Rewriting (2007) | |||||||||||||||
Abstract | |||||||||||||||
| . Freezing is a powerful technique for orienting equations. Here we give a new presentation of it which is suitable for an efficient automatic use. Further, it is shown how slight modifications of it can be applied to context-sensitive and innermost term rewriting. The experimental results on an extensive test series of non-trivial examples performed using a prototype implementation strongly underlines the practical relevance of freezing not only in term rewriting but also in automated theorem proving. 1 Introduction In theorem proving, the search for proofs can be improved drastically by taking special care of the intended semantics of frequently occurring predicates like equality. Paramodulation [RW69] is one of the most important calculi for dealing with equality which allow for a realization of the principle of `replacement of equals by equals' in an efficient way. A source of inefficiency is due to the fact that equality is a congruence relation and consequently, every eq... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||