Logical foundations of a modelling assistant for molecular biology

Fondements logiques d’un assistant à la modélisation en biologie moléculaire Cette thèse concerne la “représentation exécutable du savoir”dans le domaine de la biologie moléculaire. Elle introduit les fondements d’un cadre logique appelé iota, dont le but est de décrire et rassembler des faits au sujet d’interactions entre protéines tout en offrant au modeleur la possibilité de compiler un fragment raisonnable de la logique vers un ensemble fini de règles de réécriture. On définit une logique FO[↓] qui décrit des transitions d’états cellulaires. Un état représente le contenu d’une cellule : les éléments du domaine sont des parties de protéines et les relations sont des liaisons entre protéines. L’opérateur logique unaire ↓sélectionne les transitions où un ensemble minimal de changements a lieu. Les formules qui parlent de transitions dénotent aussi des exécutions, c’est-à-dire des séquences finies ou infinies de transitions. Chaque formule de transition est de plus associée à un ensemble de règles de réécritures équipé d’une sémantique opérationnelle. On introduit deux système déductifs qui permettent de“typer” les formules. On montre que si une formule est typable dans le1er système, alors l’exécution des règles de réécriture qui lui sont associées produit exactement les exécutions dénotées par la formule ;et que si elle est typable dans le 2nd système, alors son système de règles associé est fini. On introduit une grammaire qui produit des formules typables dans les deux systèmes à équivalence logique près. Enfin, on étudie la décidabilité et l’expressivité de fragments de FO[↓]. On montre en particulier que les formules typables dans le second système sont définissables dans un petit fragment de FO, ce qui implique que l’opérateur ↓ peut alors être éliminé.