28 citations · 48 across the 13 of their papers we have counts for
13 papers
Verification of Provers and Solvers
René Thiemann
Automatic deduction tools such as automatic theorem provers, SAT (satisfiability) solvers, SMT (satisfiability modulo theories) solvers, and termination analyzers can be connected…
Linear Termination over N is Undecidable
Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Recently it was shown that it is undecidable whether a term rewrite system can be proved terminating by a polynomial interpretation in the natural numbers. In this paper we show th…
A Verified Efficient Implementation of the Weighted Path Order
René Thiemann, Elias Wenninger
The Weighted Path Order of Yamada is a powerful technique for proving termination. It is also supported by CeTA, a certifier for checking untrusted termination proofs. To be more p…
Certification of Confluence Proofs using CeTA
Julian Nagele, René Thiemann
CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, th…
The Certification Problem Format
Christian Sternagel, René Thiemann
We provide an overview of CPF, the certification problem format, and explain some design decisions. Whereas CPF was originally invented to combine three different formats for termi…
Towards the Certification of Complexity Proofs
René Thiemann
We report on our formalization of matrix-interpretation in Isabelle/HOL. Matrices are required to certify termination proofs and we wish to utilize them for complexity proofs, too.…