The Decision Problem for Regular First Order Theories

Watch this 20-minute conference talk from POPL 2025 exploring the extension of the Entscheidungsproblem to regular first-order theories. Presented by researchers Umang Mathur, David Mestel, and Mahesh Viswanathan from the National University of Singapore, Maastricht University, and the University of Illinois at Urbana-Champaign, the video examines how certain decidable classes in classical first-order logic become undecidable when extended to regular theories. Learn about their identification of decidable subclasses within the EPR and Gurevich classes, and discover how this research connects to automata-theoretic verification of uninterpreted programs. The presentation introduces a semantic class of existential formulae for which the problem remains decidable, while highlighting open challenges for future classification work.