Abstract

Automatic tools for proving (non)termination of term rewrite systems, if successful, deliver proofs as justification. In this work, we focus on how to certify nontermination proofs. Besides some techniques that allow to reduce the number of rules, the main way of showing nontermination is to find a loop, a finite derivation of a special shape that implies nontermination. For standard termination, certifying loops is easy. However, it is not at all trivial to certify whether a given loop also implies innermost nontermination. To this end, a complex decision procedure has been developed in earlier work. We formalized this decision procedure in Isabelle/HOL and were able to simplify some parts considerably. Furthermore, from our formalized proofs it is easy to obtain a low complexity bound. Along the way of presenting our formalization, we report on generally applicable ideas that allow to reduce the formalization effort and improve the efficiency of our certifier.

BibTeX

@inproceedings{CSRT-ITP12,
  author      = "Christian Sternagel and Ren{\'e} Thiemann",
  title       = "Certification of Nontermination Proofs",
  booktitle   = "Proceedings of the 3rd International Conference on
                 Interactive Theorem Proving",
  series      = "Lecture Notes in Computer Science",
  volume      = 7406,
  pages       = "266--282",
  publisher   = "Springer-Verlag",
  year        = 2012
}