On the Complexity of Entailment in Existential Conjunctive First Order Logic with Atomic Negation

Marie-Laure Mugnier 1 Geneviève Simonet 2 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
2 ALGCO - Algorithmes, Graphes et Combinatoire
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
Abstract : We consider the entailment problem in the fragment of first-order logic (FOL) composed of existentially closed conjunctions of literals (without functions), denoted FOL(exists, et, not_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. Entailment in FOL(exists, et, not_a) is Pi2P-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 shall 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 ENTAILMENT_k be the following family of problems: given two formulas g and h in FOL(exists, et, not_a), such that g has at most k pairs of exchangeable literals, is g entailed by h? The main results are that ENTAILMENT_k is NP-complete if k is less or equal to 1, and P^NP-II-complete for any value of k greater or equal to 3. As a corollary of our proofs, we are able to classify exactly ENTAILMENTk for any value of k different from 2 when g is decomposable into a tree.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2012, 215, pp.8-31. 〈10.1016/j.ic.2012.03.001〉
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00681914
Contributeur : Marie-Laure Mugnier <>
Soumis le : jeudi 22 mars 2012 - 17:59:27
Dernière modification le : jeudi 24 mai 2018 - 15:59:22
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 17:40:24

Fichier

MugnierSimonetThomazo-pre-vers...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Marie-Laure Mugnier, Geneviève Simonet, Michaël Thomazo. On the Complexity of Entailment in Existential Conjunctive First Order Logic with Atomic Negation. Information and Computation, Elsevier, 2012, 215, pp.8-31. 〈10.1016/j.ic.2012.03.001〉. 〈lirmm-00681914〉

Partager

Métriques

Consultations de la notice

435

Téléchargements de fichiers

727