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).
Type de document :
RR-08013, 2008, pp.18
Liste complète des métadonnées

Contributeur : Marie-Laure Mugnier <>
Soumis le : jeudi 5 juin 2008 - 15:50:10
Dernière modification le : mercredi 12 décembre 2018 - 14:38:02


  • 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〉



Consultations de la notice