On the Formalization of Some Results of Context-Free Language Theory
| Autor: | Marcus Vinícius Midena Ramos, J. C. Almeida, Nelma Moreira, Ruy Jose G. B. de Queiroz |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Chomsky normal form
Computer science Programming language Context-free language Context-sensitive grammar Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing) 0102 computer and information sciences 02 engineering and technology Context-free grammar computer.software_genre 01 natural sciences Pumping lemma for regular languages Formal grammar TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Pumping lemma for context-free languages computer Context-sensitive language Computer Science::Formal Languages and Automata Theory |
| Zdroj: | Logic, Language, Information, and Computation ISBN: 9783662529201 WoLLIC |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|