一句话：研究正则一阶理论的判定问题，证明 EPR 与 Gurevich 类在经典设定下可判定但在正则理论下不可判定，并给出可判定子类。
本文研究经典 Entscheidungsproblem（一阶逻辑公式可满足性判定）的扩展：正则一阶理论，即无限的正则公式集合。作者沿用经典判定问题中对语法类可判定/不可判定的分类，考察这些类在正则理论下是否仍可判定。关键结果表明，在经典设定中可判定的 EPR 类和 Gurevich 类，对于正则理论会变为不可判定；同时作者为每个类识别出仍可判定的子类。完整分类留作未来工作。论文还指出该问题推广了未解释程序的自动机验证，并提出一个可判定的存在公式语义类。
The Entscheidungsproblem , or the classical decision problem, asks whether a given formula of first-order logic is satisfiable. In this work, we consider an extension of this problem to regular first-order theories , i.e., (infinite) regular sets of formulae. Building on the elegant classification of syntactic classes as decidable or undecidable for the classical decision problem, we show that some classes (specifically, the EPR and Gurevich classes), which are decidable in the classical setting, become undecidable for regular theories. On the other hand, for each of these classes, we identify a subclass that remains decidable in our setting, leaving a complete classification as a challenge for future work. Finally, we observe that our problem generalises prior work on automata-theoretic verification of uninterpreted programs and propose a semantic class of existential formulae for which the problem is decidable.
@article{paperbot3234,
title = {The Decision Problem for Regular First Order Theories},
author = {Umang Mathur and David Mestel and Mahesh Viswanathan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704870}
}