ISR 2026 — 15th International School on Rewriting

Advanced Track lecturers: Andrej Dudenhefner

Mechanizing undecidable properties of rewriting systems using the Rocq Prover

This introductory course presents the mechanized verification of undecidability results for string rewriting systems using the Rocq Prover [2] (formerly Coq Proof Assistant). We study classical rewriting problems:

• string rewriting (SR)
• Thue system reachability (TSR) [6]
• Post canonical systems in normal form (PCSnf) [7]
• simple semi-Thue system 01 rewriting (SSTS01)

We investigate their formalization and outline computable reductions from undecidable problems to the individual rewriting problems. The certification of such reductions induces undecidability of the corresponding problems [3, 4, 5]. We finish the course by discussing how composing such certified reductions within the library of undecidability proofs [1] gives us fully machine-checked undecidability results.

Literature

• [1] Coq Library of Undecidability Proofs Development Team. "Coq Library of Undecidability Proofs."
• [2] The Rocq Prover Development Team. "The Rocq Prover Reference Manual."
• [3] Forster, Yannick, et al. "A Coq library of undecidable problems." CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages. 2020.
• [4] Forster, Yannick. "Computability in constructive type theory." 2021.
• [5] Forster, Yannick, Edith Heiter, and Gert Smolka. "Verification of PCP-related computational reductions in Coq." International Conference on Interactive Theorem Proving. 2018.
• [6] Post, Emil L. "Recursive unsolvability of a problem of Thue." The Journal of Symbolic Logic 12.1 (1947): 1-11.
• [7] Post, Emil L. "Formal reductions of the general combinatorial decision problem." American journal of mathematics 65.2 (1943): 197-215.