Abstract FR:

L'objet de cette these est l'application d'une methode de demonstration classique connue sous le nom de tableaux analytiques a une logique non monotone, la logique de la circonscription. Ce travail nous amene, d'abord, a poursuivre une etude detaillee des tableaux analytiques. Nous definissons des operations sur l'ensemble des tableaux et nous identifions la structure de cet ensemble muni de ces operations: il s'agit d'une algebre de boole. Nous montrons ainsi en quoi l'ensemble des tableaux forme un langage simple et puissant de description et de manipulation d'ensembles de formules. Dans un second temps, cette methode des tableaux analytiques est adaptee pour traiter de la logique de la circonscription. C'est par l'intermediaire de la semantique preferentielle de la circonscription que s'etablit le lien entre ce demonstrateur et cette logique. Nous montrons comment calculer, a partir du tableau d'une theorie, le tableau minimal de cette theorie caracterisant l'ensemble des modeles minimaux de la theorie. L'organisation de ce travail suit toujours le meme schema directeur: les resultats acquis en logique propositionnelle sont etendus, par la suite, a la logique du premier ordre