Sujet : Formalisation des grammaires minimalistes dans le calcul des constructions inductives

Responsable : Pierre Castéran, Christian Retoré
Téléphone : 0556846931
e-mail : casteran@labri.fr, retore@labri.fr
Equipe : LAAA

Présentation du sujet :

On s'appuiera sur une formalisation des grammaires minimalistes de Chomsky
telle que proposée par E. Stabler et A. Lecomte.
On étudiera comment traduire cette formalisation dans le calcul des constructions
inductives à la base de l'assistant de preuves Coq.
Cette formalisation doit remplir 3 objectifs principaux :
- Etudier les propriétés formelles des grammaires minimalistes et l'interopérabilité avec d'autres formalismes (ex: grammaires catégorielles).
- Fournir des outils suffisamment bien conçus pour raisonneer sur le
langage engendré par une grammaire donnée,
- Valider les programmes OCaml développés dans le cadre du projet Signes.

L'approche devra être validée par un jeu d'exemples significatif pris
dans une langue naturelle à choisir par le doctorant.
Ce travail prend place dans le cadre du projet Signes, dont l'application
principale est le traitement de la langue des signes.

Mot-clés : Langues naturelles, logique, assistant de preuve, sémantique, syntaxe

Références :

Site de Signes