2026-07-21T14:19:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2661 2024-03-06T10:33:30Z ddc:004 open_access

Certified Subterm Criterion and Certified Usable Rules Sternagel, Christian Thiemann, René Term Rewriting Certification Termination Theorem Proving 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christian Sternagel and René Thiemann 2010 Is Part Of LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2010.325 urn:nbn:de:0030-drops-26611 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.325 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode