Abstract FR:

Les travaux presentes concernent les deux problemes fondamentaux de la logique propositionnelle : la satisfiabilite d'une formule logique (probleme sat) et la determination de ses impliquants/impliques premiers. Le premier probleme est largement etudie par la communaute ia et les progres recents sont si importants que l'on utilise actuellement des algorithmes de resolution de sat pour traiter des problemes dans des domaines jusqu'alors reserves a des prouveurs specialises (planification ou diagnostic par exemple). Le second est tres important car il caracterise le raisonnement abductif (notion d'implique). Nous proposons de modifier une methode de resolution de sat (la procedure de davis et putnam) afin de produire des formules utilisees par des outils comme l'atms. Nous avons formalise cette methode par la notion d'impliquant p-restreint premier : intuitivement, il s'agit de l'intersection d'un modele avec un ensemble consistant de litteraux. Nous utilisons ensuite cette notion dans le cadre du raisonnement non monotone : en raisonnement en monde clos (closed world reasoning) et dans le cadre de l'argumentation. Nous avons etendu notre formalisation afin d'utiliser differentes relations de preference entre impliquants p-restreints (notion d'impliquant p-restreint prefere). Dans le cadre du diagnostic, on cherchera souvent les explications mettant en cause le plus petit nombre de composants. Si l'on dispose de connaissances exogenes (des probabilites de panne pour chaque composant par exemple), on souhaite obtenir le diagnostic de panne le plus probable. Dans le cadre de l'argumentation, nous donnons deux exemples de ces relations de preference. Ces travaux s'eloignent du domaine de la satisfaction pour rejoindre les travaux sur l'optimisation. Nous montrons enfin dans le cadre de l'approche logique de la decision qualitative comment profiter de certaines particularites de notre methode de calcul d'impliquant p-restreint pour calculer des decisions optimales.