Abstract FR:

Dans cette these, notre interet s'est porte vers le probleme de la demonstration automatique dans les logiques non-monotones, qui sont des logiques formalisant le raisonnement sur des informations incompletes. Dans notre travail de these, nous avons propose deux nouveaux demonstrateurs, un pour les logiques des defauts semi-monotones, et l'autre pour la logique modale des hypotheses de siegel et schwind. Le but d'un demonstrateur est de repondre a la question suivante : etant donnees une theorie non-monotone et une formule q (la requete), existe-t-il un ensemble de conclusions de la theorie qui contient la formule q ?. Pour construire ces demonstrateurs, nous avons rapporte le probleme de la deduction dans les logiques non-monotones a un probleme typique d'abduction en recherchant un ensemble d'hypotheses qui permettent de prouver la requete a partir d'une theorie. Pour cela, nous avons utilise les algorithmes de production dont le but est de calculer l'ensemble des consequences logiques d'une theorie, qui verifient certaines proprietes specifiques. Plus precisement, les demonstrateurs que nous avons proposes pour les logiques des defauts semi-monotones et pour la logique modale des hypotheses sont bases sur deux nouveaux algorithmes de productions, l'un prenant en compte le caractere oriente d'un defaut et l'autre s'appliquant a des formules modales. Nous avons aussi realise une implantation de notre demonstrateur pour les logiques des defauts et compare ses performances avec celles des demonstrateurs existants.