Abstract

In this paper we present our formalization of two important termination techniques for term rewrite systems:
the subterm criterion and the reduction pair processor in combination with usable rules. For both techniques
we developed executable check functions in the theorem prover Isabelle/HOL which can certify the correct
application of these techniques in some given termination proof. As there are several variants of usable rules
we designed our check function in such a way that it accepts all known variants, even those which are not
explicitly spelled out in previous papers.

We integrated our formalization in the publicly available IsaFoR-library. This led to a significant increase in the
power of CeTA, the corresponding certified termination proof checker that is extracted from IsaFoR.

BibTeX

@inproceedings{CSRT-RTA10,
  author      = "Christian Sternagel and Ren\'e Thiemann",
  title       = "Certified Subterm Criterion and Certified Usable Rules",
  booktitle   = "Proceedings of the 21st International Conference on
                 Rewriting Techniques and Applications",
  series      = "Leibniz International Proceedings in Informatics",
  volume      = 6,
  pages       = "325--340",
  year        = 2010
}