Abstract FR:

Cette these a pour objet la recherche d'algorithmes bases sur la programmation lineaire pour la conception d'un systeme pour le raisonnement automatique a partir d'informations incompletes. Le formalisme choisi pour modeliser ce type de raisonnement non monotone est la logique autoepistemique de moore. Aucune limitation de syntaxe de la logique autoepistemique est imposee pour representer les informations incompletes. Les algorithmes de programmation lineaire reposent sur une formalisation finie des expansions stables par des modeles (au sens de la theorie des modeles) autoepistemiques. L'algorithme calculant les modeles autoepistemiques est un algorithme de type generer-tester. L'etape de generation debute par la traduction de l'ensemble des premisses autoepistemiques en un ensemble s d'(in)equations lineaires. Puis des (in)equations lineaires supplementaires exprimant des proprietes semantiques de la logique autoepistemiques sont adjoints a s. La phase de generation se cloture par la recherche des solutions lineaires de s etendu, ces solutions decrivant des candidats de modeles autoepistemiques. L'algorithme traduisant un ensemble de premisses en un systeme d'(in)equations lineaires et recherchant les solutions de ce dernier permet en fait de verifier la satisfaisabilite d'un ensemble de formules propositionnelles classiques de syntaxe quelconque. La traduction a une complexite lineaire en espace et n'est pas assujettie a la traduction des premisses sous forme normale. La phase de test de l'algorithme utilise a nouveau la programmation lineaire pour rechercher parmi les solutions generees celles qui constituent des modeles autoepistemiques.