We formally verify several computational reductions con- cerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verification includes a reduction of the halting problem for Tur- ing machines to string rewriting, a reduction of string rewriting to PCP, and reductions of PCP to the intersection problem and the palindrome problem for context-free grammars.
Coq Formalisation - Preliminary version at arXiv
Download PDF Show BibTeX
Login to edit