Certified Subterm Criterion and Certified Usable Rules

9 years 6 months ago
Certified Subterm Criterion and Certified Usable Rules
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 using the theorem prover Isabelle/HOL. These functions are able to certify the correct application of the formalized techniques in a 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, a certified termination proof checker that is extracted from IsaFoR.
Christian Sternagel, René Thiemann
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where RTA
Authors Christian Sternagel, René Thiemann
Comments (0)