3 citations · 4 across the 3 of their papers we have counts for
4 papers
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…
Level-Confluence of 3-CTRSs in Isabelle/HOL
Christian Sternagel, Thomas Sternagel
We present an Isabelle/HOL formalization of an earlier result by Suzuki, Middeldorp, and Ida; namely that a certain class of conditional rewrite systems is level-confluent. Our for…
KBCV 2.0 - Automatic Completion Experiments
Thomas Sternagel
This paper describes the automatic mode of the new version of the Knuth-Bendix Completion Visualizer. The internally used data structures have been overhauled and the performance w…
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…