On the Complexity of Deduction in the Existential Conjunctive Fragment of FOL with Atomic Negation - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Reports Year : 2008

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

Michaël Thomazo

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).
No file

Dates and versions

lirmm-00285475 , version 1 (05-06-2008)

Identifiers

  • HAL Id : lirmm-00285475 , version 1

Cite

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⟩
132 View
0 Download

Share

Gmail Facebook X LinkedIn More