Verification of PCP-related computational reductions in Coq

DOI10.1007/978-3-319-94821-8_15MaRDI QIDQ1791165

Gert Smolka, Edith Heiter, Yannick Forster

Publication date: 4 October 2018

Full work available at URL: https://arxiv.org/abs/1711.07023

zbMATH Keywords

undecidability; context-free grammars; string rewriting; Coq; Post correspondence problem; computational reductions

Mathematics Subject Classification ID

68Q42: Grammars and rewriting systems

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item

Uses Software

• Coq