Hereditary First-Order Logic: the tractable quantifier prefix classes
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908430653980672 |
|---|---|
| author | Bodirsky, Manuel Guzmán-Pro, Santiago |
| author_facet | Bodirsky, Manuel Guzmán-Pro, Santiago |
| contents | Many computational problems can be modelled as the class of all finite structures $\mathbb A$ that satisfy a fixed first-order sentence $ϕ$ hereditarily, i.e., we require that every (induced) substructure of $\mathbb A$ satisfies $ϕ$. We call the corresponding computational problem the hereditary model checking problem for $ϕ$, and denote it by Her$(ϕ)$.
We present a complete description of the quantifier prefixes for $ϕ$ such that Her$(ϕ)$ is in P; we show that for every other quantifier prefix there exists a formula $ϕ$ with this prefix such that Her$(ϕ)$ is coNP-complete. Specifically, we show that if $Q$ is of the form $\forall^\ast\exists\forall^\ast$ or of the form $\forall^\ast\exists^\ast$, then Her$(ϕ)$ can be solved in polynomial time whenever the quantifier prefix of $ϕ$ is $Q$. Otherwise, $Q$ contains $\exists \exists \forall$ or $\exists \forall \exists$ as a subword, and in this case, there is a first-order formula $ϕ$ whose quantifier prefix is $Q$ and Her$(ϕ)$ is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula $ϕ$ whether Her$(ϕ)$ is in P (unless P$=$NP). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_10860 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Hereditary First-Order Logic: the tractable quantifier prefix classes Bodirsky, Manuel Guzmán-Pro, Santiago Logic Computational Complexity Discrete Mathematics Logic in Computer Science 03B16, 03B70, 03C13 F.1.3; F.4.1 Many computational problems can be modelled as the class of all finite structures $\mathbb A$ that satisfy a fixed first-order sentence $ϕ$ hereditarily, i.e., we require that every (induced) substructure of $\mathbb A$ satisfies $ϕ$. We call the corresponding computational problem the hereditary model checking problem for $ϕ$, and denote it by Her$(ϕ)$. We present a complete description of the quantifier prefixes for $ϕ$ such that Her$(ϕ)$ is in P; we show that for every other quantifier prefix there exists a formula $ϕ$ with this prefix such that Her$(ϕ)$ is coNP-complete. Specifically, we show that if $Q$ is of the form $\forall^\ast\exists\forall^\ast$ or of the form $\forall^\ast\exists^\ast$, then Her$(ϕ)$ can be solved in polynomial time whenever the quantifier prefix of $ϕ$ is $Q$. Otherwise, $Q$ contains $\exists \exists \forall$ or $\exists \forall \exists$ as a subword, and in this case, there is a first-order formula $ϕ$ whose quantifier prefix is $Q$ and Her$(ϕ)$ is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula $ϕ$ whether Her$(ϕ)$ is in P (unless P$=$NP). |
| title | Hereditary First-Order Logic: the tractable quantifier prefix classes |
| topic | Logic Computational Complexity Discrete Mathematics Logic in Computer Science 03B16, 03B70, 03C13 F.1.3; F.4.1 |
| url | https://arxiv.org/abs/2411.10860 |