** PhD vacancy at LORIA / University of Lorraine, Nancy, France **
** application deadline 7 July 2019 **
PROJECT DESCRIPTION
Dynamic Epistemic Logics with Separation
Dynamic epistemic logics (Baltag, van Benthem, van Ditmarsch, …) (DEL) model change of knowledge and belief in multi-agent systems. Bunched implication logics (BI, Boolean BI / BBI) and separation logics (O’Hearn, Pym, Galmiche, …) model composing and dividing (separating) resources or information in data structures. Relations between BBI and DEL have recently been investigated (see references below). In such works modal logics have been proposed combining update modalities, epistemic modalities, and separating conjunctions and implications.
This PhD project aims to further integrate methods and tools of dynamic epistemic logic with methods and tools of bunched implications logics with separation. Among the different research directions that we envisage are: (i) defining new epistemic logics with separation, with corresponding structures and semantics; (ii) investigating the expressivity of such logics, how they contribute to modelling concurrency, and resolving decision problems for various fragments (model checking and satisfiability); (iii) defining proof calculi, both labelled and unlabelled, and investigating their properties.
The PhD supervisors for this project will be Hans van Ditmarsch and Didier Galmiche. Hans van Ditmarsch is senior researcher at CNRS, and he is heading the CELLO research group (Computational Epistemic Logic in LOrraine) at LORIA. Didier Galmiche is professor at the University of Lorraine, and he is heading the TYPES research group (Logic, Proof Theory and Programming) at LORIA.
A detailed project description (in French) can be downloaded on
https://sites.google.com/site/hansvanditmarsch/. Information on LORIA can be found on http://www.loria.fr/. Information on the University of Lorraine doctoral school IAEM (in French) can be found on http://doctorat.univ-lorraine.fr/fr/les-ecoles-doctorales/iaem/presentation.
REQUIREMENTS
The candidate must have a Master degree in computer science, logic or artificial intelligence, and a strong background in some of the following topics: (i) formal logic (non-classical, substructural, modal, epistemic, …); (ii) proof theory (sequents, tableaux, natural deduction, …), (iii) computability (decidability, complexity, …). Candidates who intend to defend their Master thesis before September 2019 are also encouraged to apply.
VENUE/SALARY
The position is for 3 years (36 months). The PhD student would preferably start between 1 October 2019 and 1 December 2019. The PhD student will be enrolled at the University of Lorraine. The PhD student will be based at LORIA and will work with the members of the CELLO and TYPES research teams. The salary will be 2135 euros (gross) per month, which is after deductions 1690 euros (net) per month.
APPLICATION PROCEDURE
The deadline for application is July 7, 2019. An email to inform about the intention to apply is welcome any time. Applications should be sent in electronic form. Applications should include (i) a c.v. including a publications list (if any), (ii) title and abstract of the MSc thesis including (if any) reports on the MSc thesis, (iii) two or three references with contact information details (recommendation letters are fine, but not necessary), and (iv) a motivation letter w.r.t. the research topics related to the PhD position. Applications may be made in English and in French. The application materials should be sent by email to (both) Hans van Ditmarsch, hans.van-ditmarsch@loria.fr and Didier Galmiche, Didier.Galmiche@loria.fr.
RECENT PUBLICATIONS ON THE PROJECT THEME
– Jean-Rene Courtault, Hans van Ditmarsch, Didier Galmiche. A public announcement separation logic. Mathematical Structures in Computer Science, 2019
– Didier Galmiche, Pierre Kimmel, David J. Pym. A Substructural Epistemic Resource Logic. ICLA, 2017.
– Stephane Demri, Raul Fervari. On the Complexity of Modal Separation Logics. AiML, 2018
– Andreas Herzig. A simple separation logic. WoLLiC, 2013
———————————————————————
Desinscription: envoyez un message a: bull-ia-unsubscribe@gdria.fr
Pour obtenir de l’aide, ecrivez a: bull-ia-help@gdria.fr