The Decision Problem for Regular First Order Theories
summary
Work shows decidability for satisfiability of regular sets of first‑order formulae hinges on concrete bounds and automata encodings: tree automata represent formula trees and a bounded model property (or its strong, computable form) yields decidability for conjunctive and disjunctive variants, while classical decidable fragments like EPR and Gurevich become undecidable for regular theories (via PCP encodings). The authors also isolate a semantic “coherence” fragment of existential formulae that is automata‑decidable and links directly to verification and synthesis encodings.
AI-written summary · about
chapters (12)
- 0:00Decision problem introduction
- 1:08Decision problem in first order logic
- 2:57Generalizing the decision problem
- 4:00Regular first order theories
- 6:32Problem statement
- 7:58Program verification and synthesis
- 10:29Computational aspects and decidability
- 11:54EPR undecidability
- 13:59Bounded model property
- 16:09Decidability proof sketch
- 17:13Semantic fragments and coherent formulas
- 18:58Applications and future directions
related talks
24mWhen Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
49mCompiling FO Sentences to Circuits: Upper Bounds and Lower Bounds on the Size of the Circuit
28mOn the Expressive Power of String Constraints
18mParikh's Theorem Made Symbolic
38mThe Intensional-Extensional Problem in Probabilistic Databases
01h 08mAlgebraic Structures in Logic and Query Evaluation 4
01h 24mIntroduction to Constraint Logic Programming
41mOptimizing Relational Programs I