Abstract FR:

La thèse comprend deux parties. La première propose une axiomatisation, dans la logique linéaire de Girard, des notions d'états et d'actions en planification. Grâce au choix d'un fragment approprié de la logique linéaire, on peut montrer la correction et la complétude des preuves effectuables dans ce fragment par rapport à une classe assez large (incluant des formes de non-déterminisme) de problèmes de planification. D'autre part, un mode de représentation logique des actions, sous forme de graphes orientés, est présenté et exploité. La deuxième partie étudie le pouvoir d'expression et la complexité de langages purement relationnels étendant la logique du premier ordre et la logique inductive à l'aide de mécanismes de comptage. On montre d'abord, à l'aide de jeux adaptés, qu'en l'absence d'opérateur de point-fixe, l'arite des compteurs induit une hiérarchie stricte de langages. On étudie ensuite le comportement asymptotique de divers langages avec compteurs: la disparité de ces comportements (loi 0-1, loi de convergence, absence de régularité) permet d'obtenir des résultats de séparation en fonction de la puissance de l'arithmétique autorisée sur les compteurs. On décrit enfin plusieurs modèles de machine générique dans le but de remédier à l'apparente inadéquation des modèles de calcul traditionnels à la représentation abstraite des bases de données comme collections d'objets non ordonnées.