Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50463
Título: | On the formalization of some results of context-free language theory |
Autor(es): | Midena Ramos, Marcus Vinicius de Queiroz, Ruy J. G. B. Moreira, Nelma Almeida, José Bacelar |
Palavras-chave: | Context-free language theory Language closure Grammar simplification Chomsky Normal Form Pumping Lemma Formalization Coq |
Data: | 2016 |
Editora: | Springer Verlag |
Revista: | Lecture Notes in Computer Science (LNCS) |
Resumo(s): | This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping Lemma for context-free languages. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/50463 |
ISBN: | 9783662529201 |
DOI: | 10.1007/978-3-662-52921-8_21 |
ISSN: | 0302-9743 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
16WOLLIC.pdf | 258,5 kB | Adobe PDF | Ver/Abrir |