Bar-Hillel theorem mechanization in Coq

DOI10.1007/978-3-662-59533-6_17MaRDI QIDQ2303595zbMATH OpenOpenAlexFDO

Authors Sergey Bozhko, Leyla Khatbullina, Semyon Grigorev

Publication date 4 March 2020

Full work available at URL https://doi.org/10.1007/978-3-662-59533-6_17

zbMATH Keywords

Bar-Hillel theoremclosurecontext-free languageCoqformal languagesintersectionregular language

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Some applications of the formalization of the pumping lemma for context-free languages
• On the formalization of some results of context-free language theory
• Formalization of the pumping lemma for context-free languages
• A mechanisation of some context-free language theory in HOL4
• Mechanisation of PDA and grammar equivalence for context-free languages

Cited in

(2)

• A mechanized proof system of the third generation calculus in Coq
• scientific article; zbMATH DE number 7566048 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Bar-Hillel theorem mechanization in Coq

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