Scifaro

中文

上下文无关语言泵引理的形式化

形式语言与自动机理论 2015-10-19 v1

作者: Marcus V. M. Ramos , Ruy J. G. B. de Queiroz , Nelma Moreira , José Carlos Bacelar Almeida

在 arXiv 上查看 ↗ PDF ↗

摘要

上下文无关语言（CFLs）在计算机语言处理技术以及形式语言理论中极为重要。泵引理（Pumping Lemma）是对所有上下文无关语言都成立的一个性质，并用于证明非上下文无关语言的存在性。本文给出了使用 Coq 证明助手的上下文无关语言泵引理的形式化。

关键词

上下文无关语言泵引理形式化 Coq 证明助手形式语言理论

引用

@article{arxiv.1510.04748,
  title  = {Formalization of the pumping lemma for context-free languages},
  author = {Marcus V. M. Ramos and Ruy J. G. B. de Queiroz and Nelma Moreira and José Carlos Bacelar Almeida},
  journal= {arXiv preprint arXiv:1510.04748},
  year   = {2015}
}