Verification of PCP-related computational reductions in Coq

DOI10.1007/978-3-319-94821-8_15OpenAlexW2769209754MaRDI 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

undecidabilitycontext-free grammarsstring rewritingCoqPost correspondence problemcomputational reductions

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (8)

Trakhtenbrot’s Theorem in Coq ⋮ Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version) ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Hilbert's Tenth Problem in Coq ⋮ Formalization of the computational theory of a Turing complete functional language model

Uses Software

• Coq

This page was built for publication: Verification of PCP-related computational reductions in Coq