OPERATION QSL

CONTRA

CONTRe-modèles et Analyse de systèmes


Les logiques mixtes, comme la logique linéaire mixte (ou logique non-commutative) où cohabitent des connecteurs commutatifs et non-commutatifs ou la logique BI où cohabitent des connecteurs intuitionnistes et linéaires, sont de nouvelles logiques qui semblent appropriées à la modélisation de protocoles et au raisonnement sur les programmes impératifs. Un des objectifs de l'équipe TYPES du LORIA est de proposer des outils de preuve et de vérification pour de telles logiques en développant des méthodes qui construisent soit des preuves, soit des contre-modèles en cas de non-prouvabilité.

Dans ce contexte, l'opération CONTRA se focalise sur la génération de structures sémantiques, comme les graphes de dépendances, qui permettent de capturer les interactions entre les connecteurs logiques durant la recherche de preuves dans des logiques mixtes. La décision de la prouvabilité ainsi que la génération de contre-modèles se fondent sur de telles structures qui seront étudiées de différents points de vue : construction, représentation, minimalité et analyse de l'échec de la preuve. Les résultats seront intégrés, au sein de la plateforme QSL, notamment dans le démonstrateur LINK, en logique non-commutative, et également dans un démonstrateur pour BI qui sera développé à partir de nos résultats récents en recherche de preuves.


PARTICIPANTS


PROPOSITION

proposition