Certified Subterm Criterion and Certified Usable Rules

Sternagel, Christian; Thiemann, René

doi:10.4230/LIPIcs.RTA.2010.325

Document

Certified Subterm Criterion and Certified Usable Rules

Authors Christian Sternagel, René Thiemann

Part of: Volume: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Rewriting Techniques and Applications (RTA)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-07-06

PDF

File

PDF

LIPIcs.RTA.2010.325.pdf

Filesize: 199 kB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.RTA.2010.325
URN: urn:nbn:de:0030-drops-26611

Subject Classification

Keywords

Term Rewriting
Certification
Termination
Theorem Proving

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Christian Sternagel and René Thiemann. Certified Subterm Criterion and Certified Usable Rules. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 325-340, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.RTA.2010.325

Author Details

Christian Sternagel

René Thiemann

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail