De la déduction dans le fragment {Existe,Et,Neg} de la logique du premier ordre à SAT - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers Year : 2008

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

Abstract

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

Dates and versions

lirmm-00355290 , version 1 (22-01-2009)

Identifiers

  • HAL Id : lirmm-00355290 , version 1

Cite

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, Angers, France. ⟨lirmm-00355290⟩
94 View
0 Download

Share

More