KBCV - Knuth-Bendix Completion Visualizer. - Thomas Sternagel; Harald Zankl (IJCAR, 2012)

Recording Completion for Finding and Certifying Proofs in Equational Logic - Thomas Sternagel; René Thiemann; Harald Zankl; Christian Sternagel (CoRR, 2012)

Initial Experiments on Deriving a Complete HOL Simplification Set. - Cezary Kaliszyk; Thomas Sternagel (PxTP@CADE, 2013)

Conditional Confluence (System Description). - Thomas Sternagel; Aart Middeldorp (RTA-TLCA, 2014)

Recording Completion for Certificates in Equational Reasoning. - Thomas Sternagel; Sarah Winkler; Harald Zankl (CPP, 2015)

Conditional Complexity. - Cynthia Kop; Aart Middeldorp; Thomas Sternagel (RTA, 2015)

KBCV 2.0 - Automatic Completion Experiments. - Thomas Sternagel (CoRR, 2015)

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. - Christian Sternagel; Thomas Sternagel (FSCD, 2016)

Level-Confluence of 3-CTRSs in Isabelle/HOL. - Christian Sternagel; Thomas Sternagel (CoRR, 2016)

Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs. - Thomas Sternagel; Christian Sternagel (CoRR, 2016)

A Characterization of Quasi-Decreasingness. - Thomas Sternagel; Christian Sternagel (CoRR, 2016)

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. - Christian Sternagel; Thomas Sternagel (CADE, 2017)

Complexity of Conditional Term Rewriting. - Cynthia Kop; Aart Middeldorp; Thomas Sternagel (Log. Methods Comput. Sci., 2017)

Certified Non-Confluence with ConCon 1.5. - Thomas Sternagel; Christian Sternagel (CoRR, 2017)

Regular Tree Relations. - Alexander Lochmann; Bertram Felgenhauer; Christian Sternagel; René Thiemann; Thomas Sternagel (Arch. Formal Proofs, 2021)

First-Order Rewriting. - René Thiemann; Christian Sternagel; Christina Kirk; Martin Avanzini; Bertram Felgenhauer; Julian Nagele; Thomas Sternagel; Sarah Winkler; Akihisa Yamada 002 (Arch. Formal Proofs, 2025)