Download PDFOpen PDF in browser

Efficient Formalization of Simplification Orders

EasyChair Preprint no. 8639

5 pagesDate: August 11, 2022


We present recent developments in CeTA w.r.t. the efficient certification of termination proofs. Here, efficiency is seen under various aspects. First, we present a case study on minimizing the formalization effort, namely when trying to verify the classical path orders by viewing them as instances of the weighted path order. Second, we argue that the efficient generation of certificates within termination tools requires more powerful certifiers, in particular when considering the usage of SAT- or SMT-solvers. Third, we present recent developments which aim at improving the execution time of CeTA.

Keyphrases: formalization, Isabelle/HOL, simplification order, termination analysis

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {René Thiemann and Akihisa Yamada},
  title = {Efficient Formalization of Simplification Orders},
  howpublished = {EasyChair Preprint no. 8639},

  year = {EasyChair, 2022}}
Download PDFOpen PDF in browser