Some applications of the formalization of the pumping lemma for context-free languages

DOI10.1016/J.ENTCS.2019.07.010MaRDI QIDQ2333674zbMATH OpenOpenAlexWikidataFDO

Authors Marcus V. M. Ramos, José Bacelar Almeida, Nelma Moreira, Ruy J. G. B. de Queiroz

Publication date 13 November 2019

Full work available at URL https://doi.org/10.1016/j.entcs.2019.07.010

zbMATH Keywords

closureCoqformalizationintersectionnon-context-free languagespumping lemma

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formalization of the pumping lemma for context-free languages
• On the formalization of some results of context-free language theory
• Pumping lemmas for linear and nonlinear context-free languages
• A mechanisation of some context-free language theory in HOL4
• Pumping lemma and Ogden lemma for displacement context-free grammars

Cites work

• scientific article; zbMATH DE number 3174044 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• On the formalization of some results of context-free language theory

Cited in

(12)

• The failure of the strong pumping lemma for multiple context-free languages
• Bar-Hillel theorem mechanization in Coq
• On the formalization of some results of context-free language theory
• scientific article; zbMATH DE number 3958762 (Why is no real title available?)
• An “Interchange Lemma” for Context-Free Languages
• A mechanisation of some context-free language theory in HOL4
• scientific article; zbMATH DE number 1222097 (Why is no real title available?)
• Pumping, Shrinking and Pronouns: From Context Free to Indexed Grammars
• Formalization of the pumping lemma for context-free languages
• Theory and Applications of Models of Computation
• Pumping lemmas for classes of languages generated by folding systems
• Context-Free Grammars and Languages

Describes a project that uses

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Some applications of the formalization of the pumping lemma for context-free languages

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