Lundi 17 Octobre
Heure: 
14:00  15:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Framester: A Wide Coverage Linguistic Linked Data Hub 
Description: 
Mehwish Alam Semantic web applications leveraging NLP can benefit from easy access to expressive lexical resources such as FrameNet. However, the usefulness of FrameNet is affected by its limited coverage and nonstandard semantics. The access to existing linguistic resources is also limited because of poor connectivity among them. We present some strategies based on Linguistic Linked Data to broaden FrameNet coverage and formal linkage of lexical and factual resources. We created a novel resource, Framester, which acts as a hub between FrameNet, WordNet, VerbNet, BabelNet, DBpedia, Yago, DOLCEZero, as well as other resources. Framester is not only a strongly connected knowledge graph, but also applies a rigorous formal treatment for Fillmore's frame semantics, enabling fullfl edged OWL querying and reasoning on a large framebased knowledge graph. We also describe Word Frame Disambiguation, an application that reuses Framester data as a base in order to perform frame detection from text, with results comparable in precision to the state of the art, but with a much higher coverage. Open issues and current research directions will be also presented. 
Mardi 18 Octobre
Heure: 
12:30  13:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Lower bounds in resource constrained shortest path algorithms 
Description: 
Axel Parmentier Resource constrained shortest path problems arise naturally as pricing subproblems of column generation approaches to a wide range of routing and scheduling problems. The algorithms for these problems rely on dominance relations between paths to discard partial solutions in an enumeration of all the paths. It is well known that the use of bounds on paths resources in addition to dominance relations strongly accelerates these algorithms. Nonetheless, there is still no standard procedure to build such bounds in nonlinear or stochastic settings. We provide such a bounding procedure and sho w its efficiency on several deterministic and stochastic path problems. Besides, enumeration algorithms exhibit poor performances when the number of constraints increases. We show that using sets of bounds instead of single bounds enable to discard more paths and thus to tackle better with these difficult instances. Finally, we prove the relevance of these procedures in the context of column generation on industrial instances of the airline crew pairing problem.Â 
Heure: 
14:00  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Combinatoire des mots 
Description: 
Johan Nilsson 
Jeudi 20 Octobre
Heure: 
15:30  16:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
IntegerComplete Synthesis for Bounded Parametric Timed Automata 
Description: 
Étienne André Ensuring the correctness of critical realtime systems, involving concurrent behaviors and timing requirements, is crucial. Parameter synthesis aims at computing dense sets of valuations for the timing requirements, guaranteeing a good behavior. However, in most cases, the emptiness problem for reachability (i.e. whether there exists at least one parameter valuation for which some state is reachable) is undecidable and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproximation in the form of linear constraints containing all the integer points ensuring reachability or unavoidability, and all the (nonnecessarily integer) convex combinations of these integer points, for general PTA with a bounded parameter domain. Our algorithms terminate and can output constraints arbitrarily close to the complete result. Joint work with Didier Lime and Olivier H. Roux. 
Vendredi 21 Octobre
Heure: 
11:00  12:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Some interplays between proof theory and computational complexity 
Description: 
Anupam Das Proof complexity is the branch of proof theory concerned with the size of proofs. Due to old and wellknown results of Cook and Reckhow, many important questions about computational complexity are equivalent to natural problems in proof complexity. For instance, coNP = NP just if there is an 'efficient' proof system for classical propositional logic. I will survey a now welldeveloped line of work on the proof complexity of 'deep inference' systems which has culminated in several novel phenomena in proof complexity, including improved bounds for monotone proof systems. I will also discuss remaining open problems in the area and some of their consequences.
A closely related area to proof complexity is bounded arithmetic, which studies weak fragments of arithmetic whose representable functions are typically feasible complexity classes, via bounds on quantifiers. They also act as uniform versions of corresponding propositional systems, forming a threeway correspondence. I will show how this methodology can be extended to certain deep inference and monotone systems via intuitionistic versions of bounded arithmetic, making use of a novel technique that combines the usual 'witness function method' of bounded arithmetic with realisability style extraction. I will further motivate the study of such theories in 'linear logic' in order to address the remaining correspondences, and present some recent work along this line.
Finally I will present an upcoming research project that aims to unify various strands of this research in order to develop a comprehensive approach to monotone complexity classes. 

