On the Complexity of Deduction in the Existential Conjunctive Fragment of FOL with Atomic Negation
Résumé
We consider the deduction problem in the fragment of first-order logic composed of existentially closed conjunctions of literals (without functions other than constants), noted FOL$\{\exists,\wedge,\neg_a\}$: given two formulas $g$ and $h$ in FOL$\{\exists,\wedge,\neg_a\}$, can $g$ be deduced from $h$? This problem can be recast as the containment problem of conjunctive queries with negation or as deduction in polarized conceptual graphs. Deduction in FOL$\{\exists,\wedge,\neg_a\}$ is $\Pi_2^P$-complete, whereas it is only NP-complete when the formulas contain no negation. In this paper, we investigate the role of particular literals in the complexity increasing. These literals have the property of being ``exchangeable'', with this notion being relative not only to the literals themselves but also to the structure of $g$ and $h$. For this study, we see formulas as graphs and rely on graph homomorphism. It is first proven that if $g$ has no pair of \emph{exchangeable} literals, and more generally if all \emph{pieces} of $g$ have no pair of exchangeable literals, deduction in FOL$\{\exists,\wedge,\neg_a\}$ has the same complexity as in the positive fragment (i.e. it is NP-complete, and even polynomial if $g$ has a special structure). Moreover, it is proven that the complexity remains NP-complete if each piece of $g$ has at most one pair of exchangeable literals. The problem complexity when each piece of $g$ has at most two pairs of exchangeable literals, and more generally $k$ pairs of exchangeable literals, is an open question. Finally, we point out that these results can be extended when the set of predicates is provided with a preorder (which allows us to introduce a basic ontology).