On the formalization of termination techniques based on multiset orderings
View/ Open
Volume
15
Pagination
339 - 354
ISBN-13
9783939897385
DOI
10.4230/LIPIcs.RTA.2012.339
ISSN
1868-8969
Metadata
Show full item recordAbstract
Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions. Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques-where all parameters are provided-is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard. © René Thiemann, Guillaume Allais, and JulianNagele.