Résumé : L'étude de la relation entre syntaxe et sémantique qu'établissent les grammaires de types
logiques a essentiellement privilégié le sens de l'analyse - syntaxe vers sémantique. Cette thèse souligne le profit que la génération - sémantique vers syntaxe - tire de l'étroitesse de cette relation.

Elle s'appuie sur l'étude logique de ces modèles grammaticaux et met en avant l'utilisation de la logique linéaire et de ses réseaux de preuve. Autour du calcul de Lambek, un fragment intuitionniste de la logique linéaire non commutative, nous étudions le comportement des extensions de ce calcul en tant que modèles syntaxiques, notamment avec le calcul ordonné. Nous montrons par exemple qu'un fragment de ce dernier permet d'engendrer la même classe de langage que les grammaires d'arbres adjoints.

D'autre part, l'adéquation de la syntaxe, portée par la notion de preuve, à la sémantique de Montague, portée par la notion de lambda-terme, s'illustre dans la correspondance de Curry-Howard. L'utilisation des réseaux de preuve nous permet de montrer que, pour le calcul de Lambek et pour des représentations sémantiques linéaires avec une constante au moins, le problème de génération est décidable et que ces grammaires sont intrinsèquement réversibles. Nous caractérisons les formes sémantiques permettant une réalisation syntaxique polynomiale. Aussi pouvons-nous proposer une méthode complète de génération dans ce cadre.

Ces résultats, de même que l'implémentation dont ils ont fait l'objet, exploitent la théorie de la démonstration sous-jacente et en particulier les réseaux de preuve sous forme de graphes. Nous obtenons ainsi un cadre uniforme pour l'analyse et la génération. Pour le conserver, dans l'optique d'une prise en compte sémantique de termes non linéaires grâce aux connecteurs exponentiels de la logique linéaire, nous donnons une nouvelle syntaxe et un nouveau critère de correction pour les réseaux avec exponentiels sous forme de graphes.