2015/09/07 by Marcus Vinícius Midena Ramos, Marcus V. M. Ramos, Ruy J. G. B. de Queiroz +2
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic, programming, and type systems #Natural Language Processing Techniques #cs.FL #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1509.02032
LSFA 2015
openalex publication_date 2015/09/07 · arxiv created 2015/10/16 · arxiv updated 2015/10/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inaccessible symbol elimination, unit rules elimination and empty rules elimination operations were described and proven correct with respect to the preservation of the language generated by the original grammar.