Further Tackling Post Correspondence Problem and Proof Generation

This video from the CPP 2025 conference presents research by Akihiro Omori and Yasuhiko Minamide from the Institute of Science Tokyo on tackling the Post Correspondence Problem (PCP). Learn about their novel algorithm that uses regular languages and automata theory to identify inductive invariants within transition systems associated with PCP[3,4] instances, demonstrating the unsolvability of certain instances. The researchers developed an interactive tool to manually find inductive invariants, successfully solving all but two instances. Discover how they generated proofs for each instance that can be verified using Isabelle/HOL, ensuring correctness of their results. The 31-minute presentation covers certified computation, proof assistants, transition systems, reachability problems, and regular languages, offering valuable insights for those interested in computational theory and formal verification.