The Decision Problem for Regular First-Order Theories
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917880765874176 |
|---|---|
| author | Mathur, Umang Mestel, David Viswanathan, Mahesh |
| author_facet | Mathur, Umang Mestel, David Viswanathan, Mahesh |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_17185 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Decision Problem for Regular First-Order Theories Mathur, Umang Mestel, David Viswanathan, Mahesh Logic in Computer Science Formal Languages and Automata Theory Programming Languages 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. |
| title | The Decision Problem for Regular First-Order Theories |
| topic | Logic in Computer Science Formal Languages and Automata Theory Programming Languages |
| url | https://arxiv.org/abs/2410.17185 |