On the Complexity of Deduction in Existential Conjunctive First Order Logic with Atomic Negation (Long Version) - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Rapport Année : 2009

On the Complexity of Deduction in Existential Conjunctive First Order Logic with Atomic Negation (Long Version)

Geneviève Simonet
  • Fonction : Auteur
  • PersonId : 922824
Michael Thomazo

Résumé

We consider the deduction problem in the fragment of first-order logic (FOL) composed of existentially closed conjunctions of literals (without functions), denoted FOL$\{\exists,\wedge,\neg_a\}$. This problem can be recast as several fundamental problems in artificial intelligence and databases, namely query containment for conjunctive queries with negation, clause entailment for clauses without functions and query answering with incomplete information for boolean conjunctive queries with negation over a fact base. Deduction in FOL$\{\exists,\wedge,\neg_a\}$ is $\Pi_2^P$-complete, whereas it is only NP-complete when the formulas contain no negation. We investigate the role of specific literals in this complexity increase. These literals have the property of being ``exchangeable'', with this notion taking the structure of the formulas into account. To focus on the structure of formulas, we see them as labeled graphs. Graph homomorphism, which provides a sound and complete proof procedure for positive formulas, is at the core of this study. Let Deduction$_k$ be the following family of problems: given two formulas $g$ and $h$ in FOL$\{\exists,\wedge,\neg_a\}$, such that $g$ has at most $k$ pairs of exchangeable literals, can $g$ be deduced from $h$? The main results are that Deduction$_k$ is NP-complete if $k \leq 1$, and in $P^{NP}$ for any value of $k$; moreover, it is both NP-difficult and co-NP-difficult for $k \geq 3$. As a corollary of our proofs, we are able to classify exactly previous problems when $g$ is decomposable into a tree. Finally, several complementary results and extensions are provided.
Fichier principal
Vignette du fichier
RRLIRMM0926.pdf (360.02 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

lirmm-00413699 , version 1 (04-09-2009)
lirmm-00413699 , version 2 (02-09-2011)

Identifiants

  • HAL Id : lirmm-00413699 , version 1

Citer

Marie-Laure Mugnier, Geneviève Simonet, Michael Thomazo. On the Complexity of Deduction in Existential Conjunctive First Order Logic with Atomic Negation (Long Version). RR-09026, 2009, pp.53. ⟨lirmm-00413699v1⟩

Collections

ENS-CACHAN
382 Consultations
374 Téléchargements

Partager

More