Abstract FR:

Pendant les dernieres annees, la construction automatique de modeles s'est etablie comme un sous-domaine important de la deduction automatique. Son but est de construire automatiquement (la description d') un modele pour une formule logique satisfaisable donnee d'une maniere qui permet d'effectuer des operations utiles comme l'evaluation d'atomes et de clauses dans le modele. Dans cette these, nous presentons des methodes de construction automatique de modeles finis et infinis pour des ensembles de clauses gardees (sans egalite). Les clauses gardees sont des formes clausales de formules du fragment garde qui generalise les logiques modales minimales, tout en gardant les bonnes proprietes de ces logiques comme la decidabilite ou la propriete du modele fini. Le fragment garde et ses derivations se sont averes comme un concept tres fructueux promettant de nombreux applications. Les systemes existants de construction de modeles ne permettent pas de traiter des ensembles de clauses gardees efficacement, parce qu'ils ne peuvent pas beneficier des leurs proprietes particulieres. Pour cette raison, il etait necessaire de concevoir des methodes speciales pour des clauses gardees. La methode de construction de modeles pour des ensembles satisfaisables de clauses gardees introduite dans cette these est une extension de la procedure de decision par resolution. Un ensemble satisfaisable donne e est d'abord sature par resolution, et puis il est transforme en un ensemble e de clauses de horn gardees d'une forme particuliere representant un modele de e. Il est possible d'evaluer des clauses gardees dans le modele represente par e, mais e peut aussi etre utilise pour guider la recherche d'un modele fini de e. Nous montrons que notre methode peut facilement etre adaptee aux clauses legerement gardees qui generalisent les clauses gardees. Nous presentons egalement une methode de construction de modeles pour des clauses de horn faiblement gardees. Les clauses faiblement gardees sont une autre generalisation des clauses gardees.