Further Tackling Post Correspondence Problem and Proof Generation

Abstract

Post Correspondence Problem (PCP) is a classic example of an undecidable problem, with various heuristic algorithms proposed to tackle its instances. In this study, we focus on solving a particular subset of instances known as PCP[3,4]. We introduce a novel algorithm that leverages regular lan- guages and automata theory to identify inductive invariants within the transition systems associated with these instances, enabling us to demonstrate the unsolvability of instances. Additionally, we manually found some inductive invariants using an interactive tool developed specifically for this pur- pose. As a result, we successfully solved all instances except for two. To ensure the correctness of our results, we gen- erated proofs for each instance that can be verified using Isabelle/HOL.