Formalization of the Pumping Lemma for Context-Free Languages

被引：0

作者：

Ramos, M. V. M. ^{[1
]}

De Queiroz, R. J. G. B. ^{[2
]}

Moreira, N. ^{[3
]}

Almeida, J. C. B. ^{[4
]}

机构：

[1] Fundacao Univ Fed Vale Sao Francisco, Colegiado Engn Computacao, Petrolina, PE, Brazil

[2] Univ Fed Pernambuco, Ctr Informat, Recife, PE, Brazil

[3] Univ Porto, Fac Ciencias, Dept Ciencia Computadores, P-4100 Oporto, Portugal

[4] Univ Minho, HASLab INESC TEC, P-4719 Braga, Portugal

来源：

JOURNAL OF FORMALIZED REASONING | 2016年 / 9卷 / 02期

关键词：

D O I：

暂无

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.

引用

页码：53 / 68

页数：16

共 20 条

[1]

Bar-Hillel Y., 1961, SPRACHTYPOLOGIE UNIV, V14, P143

[2] A mechanisation of some context-free language theory in HOL4 [J].

Barthwal, Aditi ;

Norrish, Michael .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2014, 80 (02) :346-362

[3]

Barthwal A, 2010, LECT NOTES COMPUT SC, V6247, P95, DOI 10.1007/978-3-642-15205-4_11

[4] Mechanisation of PDA and Grammar Equivalence for Context-Free Languages [J].

Barthwal, Aditi ;

Norrish, Michael .

LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, 2010, 6188 :125-135

[5]

Barthwal Aditi, 2010, THESIS

[6]

Bertot Y., 2004, TEXT THEORET COMP S

[7]

Doczkal C, 2013, LECT NOTES COMPUT SC, V8307, P82, DOI 10.1007/978-3-319-03545-1_6

[8] Certified Normalization of Context-Free Grammars [J].

Firsov, Denis ;

Uustalu, Tarmo .

CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2015, :167-174

[9] Certified CYK parsing of context-free languages [J].

Firsov, Denis ;

Uustalu, Tarmo .

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2014, 83 (5-6) :459-468

[10]

Hopcroft J.E., 1979, INTRO AUTOMATA THEOR

← 1 2 →