一句话：提出可扩展框架，用于判定、证明并解释上下文无关文法的等价与非等价，并在教育数据上验证。
上下文无关语言的等价性问题一般是不可判定的，但教育支持系统等场景仍需要对大量文法进行等价性判定与错误解释。本文提出一个可扩展框架，结合抽象文法转换语言、面向一大类上下文无关语言的理论比较算法，以及受图论启发的文法规范化方法，从而识别等价文法、足够相似的非等价文法以及同构文法。作者实现了该框架并在教育支持系统收集的大规模数据集上评估。结果表明，尽管问题一般不可判定，该框架仍能处理数据集中的很大一部分，并提供（非）等价的证明或解释。
We propose a scalable framework for deciding, proving, and explaining (in-)equivalence of context-free grammars. We present an implementation of the framework and evaluate it on large data sets collected within educational support systems. Even though the equivalence problem for context-free languages is undecidable in general, the framework is able to handle a large portion of these datasets. It introduces and combines techniques from several areas, such as an abstract grammar transformation language to identify equivalent grammars as well as sufficiently similar inequivalent grammars, theory-based comparison algorithms for a large class of context-free languages, and a graph-theory-inspired grammar canonization that allows to efficiently identify isomorphic grammars.
@article{paperbot3016,
title = {Detecting and Explaining (In-)equivalence of Context-Free Grammars},
author = {Marko Schmellenkamp and Thomas Zeume and Sven Argo and Sandra Kiefer and Cedric Siems and Fynn Stebel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763156}
}