On the Formalization of Some Results of Context-Free Language Theory
On the Formalization of Some Results of Context-Free Language Theory
dc.contributor.author | Midena Ramos,MVM | en |
dc.contributor.author | de Queiroz,RJGB | en |
dc.contributor.author | Moreira,N | en |
dc.contributor.author | José Bacelar Almeida | en |
dc.date.accessioned | 2017-12-22T12:07:14Z | |
dc.date.available | 2017-12-22T12:07:14Z | |
dc.date.issued | 2016 | en |
dc.description.abstract | 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. | en |
dc.identifier.uri | http://repositorio.inesctec.pt/handle/123456789/4753 | |
dc.identifier.uri | http://dx.doi.org/10.1007/978-3-662-52921-8_21 | en |
dc.language | eng | en |
dc.relation | 5598 | en |
dc.rights | info:eu-repo/semantics/openAccess | en |
dc.title | On the Formalization of Some Results of Context-Free Language Theory | en |
dc.type | conferenceObject | en |
dc.type | Publication | en |
Files
Original bundle
1 - 1 of 1