On the Formalization of Termination Techniques based on Multiset Orderings
René Thiemann, Guillaume Allais, and Julian NageleProceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Leibniz International Proceedings in Informatics 15, pp. 339 – 354, 2012.
Abstract
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.
BibTeX
@inproceedings{RTGAJN-RTA12, author = "Ren\'{e} Thiemann and Guillaume Allais and Julian Nagele", title = "On the Formalization of Termination Techniques based on Multiset Orderings", booktitle = "Proceedings of the 23rd International Conference on Rewriting Techniques and Applications", series = "Leibniz International Proceedings in Informatics", volume = 15, pages = "339--354", year = 2012 }