De la déduction dans le fragment {Existe,Et,Neg} de la logique du premier ordre à SAT

Khalil Ben Mohamed 1 Michel Leclère 2 Marie-Laure Mugnier 2
2 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
Résumé : Nous considérons le problème de déduction dans le fragment existentiel conjonctif muni de la négation atomique en logique du premier ordre. Nous proposons une réécriture de ce problème en un problème de test de validité d'une formule propositionnelle, tout en exploitant les résultats antérieurs obtenus sur un problème équivalent, celui de l'inclusion de requêtes conjonctives avec négation [LM07]. Ces résultats sont basés sur la notion d'homomorphisme de graphes. Premièrement, nous faisons une synthèse de ces résultats et les reformulons dans un cadre logique. Deuxièmement, nous présentons notre nouvelle approche qui conduit à tester la validité d'une forme disjonctive propositionnelle, autrement dit l'insatisfiabilité d'une forme clausale propositionnelle, ce qui permet d'utiliser un solveur SAT.
Type de document :
Communication dans un congrès
Journées d'Intelligence Artificielle Fondamentale, Oct 2008, pp.11, 2008, 〈http://gdri3iaf.info.univ-angers.fr/〉
Liste complète des métadonnées

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00355290
Contributeur : Khalil Ben Mohamed <>
Soumis le : jeudi 22 janvier 2009 - 15:05:23
Dernière modification le : jeudi 24 mai 2018 - 15:59:22

Identifiants

  • HAL Id : lirmm-00355290, version 1

Collections

Citation

Khalil Ben Mohamed, Michel Leclère, Marie-Laure Mugnier. De la déduction dans le fragment {Existe,Et,Neg} de la logique du premier ordre à SAT. Journées d'Intelligence Artificielle Fondamentale, Oct 2008, pp.11, 2008, 〈http://gdri3iaf.info.univ-angers.fr/〉. 〈lirmm-00355290〉

Partager

Métriques

Consultations de la notice

80