4 citations · 16 across the 10 of their papers we have counts for
16 papers · 1 filter
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.