Transformation orderings are a powerful tool for proving termination of term rewriting systems. However, it is rather hard to establish their applicability to a given rule system. We introduce an algorithm which automatically generates transformation orderings for many nontrivial systems including Hercules & hydra and sorting algorithms.
CITATION STYLE
Steinbach, J. (1995). Automatic termination proofs with transformation orderings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 914, pp. 11–25). Springer Verlag. https://doi.org/10.1007/3-540-59200-8_44
Mendeley helps you to discover research relevant for your work.