STAGE DE RECHERCHE M2

UN DEMONSTRATEUR POUR LA LOGIQUE DE LA CAPABILITÉ (ABILITY LOGIC)

La logique de la capabilité (ability logic) de Elgesem est une logique modale qui formalise la notion de "faire en sorte que". 
Elle a été étudiée dans le contexte du raisonnement juridique et en intelligence artificielle  dans le cadre du raisonnement multi-agent. 
Cette logique contient deux modalités [E] et [C] indexées par des agents: une  formule [E] _i A est interprété comme «l'agent i fait 
en sorte que A», tandis que une formules [C] _i A est interprété comme «l'agent i a la capacité de faire en sorte que A». 
Dans cette logique, nous pouvons exprimer des phrases comme «John fait en sorte que le loyer soit payé» - ce qui signifie à peu près 
que John paie le loyer - et «John a la capacité de faire en sorte que le loyer soit payé» - ce qui signifie à peu près que John peut payer 
le loyer. Dans cette logique, les agents sont censés "faire en sorte que" quelque chose seulement s'ils sont directement responsables 
de sa réalisation. Par exemple, affirmer que "John fait en sorte que Bob fait en sorte que le loyer soit payé" (délégation) 
n'est pas équivalent à affirmer que John paie le loyer.  De même, un agent ne peut "faire en sorte que" quelque chose qui serait 
toujours réalisée (ou vraie), même sans son intervention : par exemple, John "ne peut faire en sorte que" la terre tourne autour du soleil.

L'objectif de cette stage est de developper un demonstrateur qui vérifie si une formule de logique de Elgesem est valide ou pas
en produisant une preuve ou un contre-modèle.  Le demonstrateur sera developpé en Prolog et implémentera les calculs à hyperséquents définis dans l'article [1]. 

PREREQUIS : 
Des connaissances de base de la logique, et des logiques modales en particulier,  des méthodes des preuves  et de la programmation logique sont fortement souhaitées. 

DEBUT prévu: 1/02/2021 

DUREE : de 4 à 5 mois

GRATIFICATION : la gratification préconisée par la loi (actualisée au 2021) pour les stages au sein d'établissements publics. 

CANDIDATURE  
Envoyer un CV, vos relevés de notes des deux dernières années et une lettre de motivation.

CONTACTS :
Charles Grellois, LIS, Univ. d'Aix-Marseille, charles.grellois@univ-amu.fr
Nicola Olivetti, LIS, Univ. d'Aix-Marseille, nicola.olivetti @univ-amu.fr, 


REFERENCES BIBLIOGRAPHIQUE

[1] Tiziano Dalmonte, Charles Grellois, and Nicola Olivetti,  Proof systems for the logics of
inging-it-about. Proceedings of the 15th International Conference on Deontic Logic and Normative Systems (DEON2020/2021). 
http://www.collegepublications.co.uk/DEON/Dalmonte%20&%20Grellois%20&%20Olivetti_DEON2020.pdf

[2] D. Elgesem, The modal logic of agency. Nordic Journal of Philosophical Logic, 2(2), 1–46 (1997).

[3] G. Governatori and A. Rotolo, On the axiomatisation of Elgesem’s logic of agency and ability. Journal of Philosophical Logic, 
34, 403–431 (2005).

[4] N. Troquard,,Reasoning about coalitional agency and ability in the logics of "bringing-it-about". 
Autonomous Agents and Multi-Agent Systems 28(3): 381-407 (2014).