1 Juillet - 7 Juillet


Retour à la vue des calendrier
Lundi 1 Juillet
Heure: 00:59 - 16:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: After the f-score: applying parser output in sentiment analysis, grammatical error detection and quality estimation for machine translation
Description: Jennifer Foster several natural language processing applications, either because the "sense-making" applications such as sentiment analysis or question in "language proofing" applications such as grammar checking or experiments carried out in the National Centre for Language Technology parser output in three downstream applications, namely, sentiment translation. In all these experiments some kind of phrase structure used to parse the input, and in some cases, the phrase structures were structure trees and dependency graphs was employed in the downstream clear from these experiments that syntactic parsing always provides some syntactic information or what the relationship between the accuracy of F1 or labelled attachment accuracy) and its usefulness in the downstream 
Vendredi 5 Juillet
Heure: 00:59 - 14:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Forcing in classical realizability: the case study of Herbrand trees
Description: Lionel Rieg Krivine presented in 2010 a methodology to combine Cohen's forcing with
the theory of classical realizability and showed that the forcing
condition can be seen as a reference that is not subject to backtracks.
The underlying classical program transformation was then analyzed by
Miquel (2011) in a fully typed setting in classical higher-order
arithmetic (PAw+).As a case study of this methodology, I present a method to extract a
Herbrand tree from a classical realizer of an existential formula,
following the idea of the proof of Herbrand theorem.  Unlike the
traditional proof based on Konig's lemma (using a fixed enumeration of
atomic formulas), our method is based on the introduction of a
particular Cohen real.  It is formalized as a proof in PAw+, making
explicit the construction of generic sets in this framework in the
particular case where the set of forcing conditions is arithmetical.  We
then analyze the algorithmic content of this proof.