Certified ACKBO. - Alexander Lochmann 001; Christian Sternagel (CPP, 2019)

Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting. - Alexander Lochmann 001; Aart Middeldorp (TACAS (2), 2020)

A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. - Alexander Lochmann 001; Aart Middeldorp; Fabian Mitterwallner; Bertram Felgenhauer (CPP, 2021)

Certifying Proofs in the First-Order Theory of Rewriting. - Fabian Mitterwallner; Alexander Lochmann 001; Aart Middeldorp; Bertram Felgenhauer (TACAS (2), 2021)

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

Reducing Rewrite Properties to Properties on Ground Terms. - Alexander Lochmann 001 (Arch. Formal Proofs, 2022)

First-Order Theory of Rewriting. - Alexander Lochmann 001; Bertram Felgenhauer (Arch. Formal Proofs, 2022)

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. - Aart Middeldorp; Alexander Lochmann 001; Fabian Mitterwallner (J. Autom. Reason., 2023)