28 citations · 56 across the 20 of their papers we have counts for
6 papers · 1 filter
Recording Completion for Finding and Certifying Proofs in Equational Logic
Thomas Sternagel, René Thiemann, Harald Zankl +1
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify…
A Relative Dependency Pair Framework
Christian Sternagel, René Thiemann
In this paper we generalize the DP framework to a relative DP framework, where a so called split is possible.
Certification extends Termination Techniques
Christian Sternagel, René Thiemann
There are termination proofs that are produced by termination tools for which certifiers are not powerful enough. However, a similar situation also occurs in the other direction. W…
CeTA - A Tool for Certified Termination Analysis
Christian Sternagel, René Thiemann, Sarah Winkler +1
Since the first termination competition in 2004 it is of great interest, whether a proof that has been automatically generated by a termination tool, is indeed correct. The increas…
A Locale for Minimal Bad Sequences
Christian Sternagel
We present a locale that abstracts over the necessary ingredients for constructing a minimal bad sequence, as required in classical proofs of Higman's lemma and Kruskal's tree theo…
Getting Started with Isabelle/jEdit in 2018
Christian Sternagel
This is a beginner-oriented introduction to Isabelle/jEdit, the main user interface for the proof assistant Isabelle.