全称量词使得自动结构难以决定
摘要：自动结构是其宇宙和关系可以表示为正则语言的结构。由于正则语言的标准闭包特性，自动结构的一阶理论是可决定的。尽管存在量词可以通过同态映射在线性时间内消除，但通常通过恒等式$ forall,x,.,而不需对$\Phi$进行两次补充。尽管一些现有自动结构类的下界证明了在消除普遍量词时一个线性指数反弹是不可避免的，但目前还不清楚是否可能有更好的方法避免天真思考的两次指数反弹，尤其是在受限制的场景下。 在本文中，我们对这个问题给出了否定的答案，并展示了一类NFA表示的自动关系族，当消除一个通用量词时，识别该语言的最小NFA是双指数的，并且判断该语言是否为空是ExpSpace完全的。
作者：Christoph Haase and Rados{l}aw Pi''orkowski
论文ID：2306.10432
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-21