Abstract de la publi numéro 13782

Le but de cet article est de montrer comment faire des simulations sociales en logique. Afin d’atteindre cet objectif, nous présentons une logique dynamique avec affectations et itérations bornées et non-bornées. Nous montrons que notre logique permet de représenter et de raisonner sur un exemple paradigmatique de la simulation sociale : le modèle de ségrégation de Schelling. Nous établissons également un lien entre simulation et planification. En particulier, nous montrons que le problème de la vérification qu’une certaine propriété P (comme la ségrégation) va émerger après n pas de simulation peut se ramener à un problème de planification à horizon n, c’est-à-dire le problème de la vérification de l’existence d’un plan de longueur au plus n assurant qu’un certain but va être atteint, problème qui a été très étudié en IA.