Skip to Main content Skip to Navigation

On the Complexity of Deduction in the Existential Conjunctive Fragment of FOL with Atomic Negation

Marie-Laure Mugnier 1 Michaël Thomazo 1
1 GRAPHIK - Graphs for Inferences on Knowledge
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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).
Document type :
Complete list of metadata
Contributor : Marie-Laure Mugnier <>
Submitted on : Thursday, June 5, 2008 - 3:50:10 PM
Last modification on : Wednesday, December 12, 2018 - 2:38:02 PM


  • HAL Id : lirmm-00285475, version 1



Marie-Laure Mugnier, Michaël Thomazo. On the Complexity of Deduction in the Existential Conjunctive Fragment of FOL with Atomic Negation. RR-08013, 2008, pp.18. ⟨lirmm-00285475⟩



Record views