28 citations · 56 across the 20 of their papers we have counts for
20 papers
TTT2 with Termination Templates for Teaching
Jonas Schöpf, Christian Sternagel
On the one hand, checking specific termination proofs by hand, say using a particular collection of matrix interpretations, can be an arduous and error-prone task. On the other han…
Certified Ordered Completion
Christian Sternagel, Sarah Winkler
On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such too…
The remote_build Tool
Christian Sternagel
This is an introduction to the remote_build tool for transparent remote session builds. The intended workflow for a user is to locally issue a build command for some session heap i…
Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel +1
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstra…
Certified Non-Confluence with ConCon 1.5
Thomas Sternagel, Christian Sternagel
We present three methods to check CTRSs for non-confluence: (1) an ad hoc method for 4-CTRSs, (2) a specialized method for unconditional critical pairs, and finally, (3) a method t…
The Generalized Subterm Criterion in TTT2
Christian Sternagel
We present an SMT encoding of a generalized version of the subterm criterion and evaluate its implementation in TTT2.