Master informatique semestre 3

Logique et Langages J1IN9M11
(partie théorie de la démonstration, lambda calcul et grammaires catégorielles)

Devoirs

• corrigé du devoir surveillé
• devoir à la maison pour le 11 janvier

Programme du cours et de l'examen.

• Calcul propositionnel intuitionniste
  • propositionelle: preuves et lambda termes
  • propositionnelle quantifiée: preuve et lambda termes (système F)
    
• Analyse sémantique du langage naturel

Théorie de la démonstration

• Un excellent livre de cours sur les systèmes déductifs, épuisé et désormais sur Internet:
  Proofs and Types J.-Y. Girard, notes de cours traduites par Yves Lafont et Paul Taylor; Cambridge University Press
• Quelques transparents sur les systèmes déductifs

Systèmes déductifs et grammaires formelles:
les grammaires catégorielles et applications à la modélisation du langage naturel

• Notes de cours sur les grammaires catégorielles (100 pp., plus complet que le cours sur ce sujet):
  The Logic of Categorial Grammars - Lecture Notes . Ch. Retoré. Rapport de Recherche INRIA 5703
• Présentation générale de la linguistique informatique suivie d'une présentation des grammaires catégorielles
• Sur ce genre de sujet, voir aussi la page de l'équipe Signes

Sujets d'examens, de DS, parfois avec correction:

• Examen de syntaxe licence de sciences du langage, Bordeaux 3 (même genre de sujet, en plus simple)
• Examen Traitement Symbolique des Langues 2002/2003
• Examen Traitement Symbolique des Langues 2003/2004
• Examen Traitement Symbolique des Langues 2004/2005
• Contrôle Continu 2004/2005
• Devoir à rendre le jeudi 3 janvier 2008.
• Devoir à rendre le 5 janvier 2009
• Examen janvier 2009 en grande partie corrigé (sauf questions mécaniques, sauf arbres de preuves)
• Contrôle continu 2008/2009 La logique classique en déduction naturelle Enoncé
  La non-non traduction de Gödel-Kolmogorov entre logique classique (NK) et logique intuitionniste (NJ) ) Enoncé Indications Solution
• Devoir surveillé corrigé: logique intuitionniste propositionnelle: preuves et sémantique dénotationnelle
• Devoir à rendre pour le 5 janvier 2011.
  • éléments de correction