Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

DOI10.4230/LIPICS.FSCD.2021.18MaRDI QIDQ6159935OpenAlexFDO

Authors Dominique Larchey-Wendling

Publication date 23 June 2023

Full work available at URL https://hal.inria.fr/hal-03280264

zbMATH Keywords

Minsky machinesundecidabilitycomputability theoryCoqmany-one reductionfractransub-exponential linear logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Recommendations

• Undecidability of multiplicative subexponential logic
• The undecidability theorem for the Horn-like fragment of linear logic (revisited)
• Decision problems for propositional linear logic
• The undecidability of second order linear logic without exponentials
• The undecidability of second order multiplicative linear logic

Cited in

(1)

• Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

This page was built for publication: Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6159935)