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

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

Polynomial Termination Over ℕ Is Undecidable. - Fabian Mitterwallner; Aart Middeldorp (FSCD, 2022)

Linear Termination over N is Undecidable. - Fabian Mitterwallner; Aart Middeldorp; René Thiemann (CoRR, 2023)

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

Confluence of Logically Constrained Rewrite Systems Revisited. - Jonas Schöpf; Fabian Mitterwallner; Aart Middeldorp (IJCAR (2), 2024)

Linear Termination is Undecidable. - Fabian Mitterwallner; Aart Middeldorp; René Thiemann (LICS, 2024)

Undecidability Results on Orienting Single Rewrite Rules. - René Thiemann; Fabian Mitterwallner; Aart Middeldorp (Arch. Formal Proofs, 2024)

Automated Strategy Invention for Confluence of Term Rewrite Systems. - Liao Zhang; Fabian Mitterwallner; Jan Jakubuv; Cezary Kaliszyk (CoRR, 2024)