The Decision Problem for Regular First-Order Theories
Umang Mathur, David Mestel, Mahesh Viswanathan
TL;DR
This work extends the classical decision problem to regular first-order theories, where theories are infinite but presented by finite automata. It develops weak and strong bounded model properties that yield decidability for conjunctive and disjunctive satisfiability, respectively, and provides a framework for automata-based model checking on finite structures. The study shows that two central decidable FO fragments, EPR and Gurevich, become undecidable in the regular setting, but also identifies decidable subfragments and a semantic coherent existential class, mapping out a landscape that connects logic with automata theory and program verification. The results illuminate how regular presentations of theories interact with decidability, with implications for verification, synthesis, and learning tasks that rely on regular formula sets and congruence reasoning.
Abstract
The \emph{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 \emph{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.