De la déduction dans le fragment {Existe,Et,Neg} de la logique du premier ordre à SAT
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.