Efficient Formalization of Simplification Orders

EasyChair Preprint no. 8639

Abstract

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

@Booklet{EasyChair:8639,
  author = {René Thiemann and Akihisa Yamada},
  title = {Efficient Formalization of Simplification Orders},
  howpublished = {EasyChair Preprint no. 8639},

  year = {EasyChair, 2022}}