Abstract
We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verification includes a reduction of the halting problem for Turing 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.
Author supplied keywords
Cite
CITATION STYLE
Forster, Y., Heiter, E., & Smolka, G. (2018). Verification of PCP-Related Computational Reductions in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10895 LNCS, pp. 253–269). Springer Verlag. https://doi.org/10.1007/978-3-319-94821-8_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
