Abstract This thesis addresses the issue of “Executable Knowledge Representation” in the context of molecular biology. We introduce the foundation of a logical framework, termed iota, whose aim is to facilitate knowledge collation of molecular interactions at the level of proteins and at the same time allows the modeler to compile a reasonable fragment of the logic into a finite set of executable graph rewriting rules. We define a logic FO[↓] over cell state transitions. States represent cell contents; domain elements are protein parts and relations are protein-protein bindings. The unary logical operator ↓ selects transitions where as little as possible happens. Formulas over transitions also denote runs, which are finite or infinite sequences of transitions. Every transition formula is also associated to a set of rewriting rules equipped with an operational semantics. We introduce two deductive systems that act as “typing” for formulas. We show that if a formula is typable in the first system then the execution of its associated rule set produces exactly the runs denoted by the formula, and that if it is typable in the second system then its associated rule set is finite. We introduce a grammar that produces formulas typable in both systems, up to logical equivalence. Finally we study decidability and definability properties of fragments of FO[↓]. In particular, we show that formulas typable in the second system are in a tight fragment of FO, which implies that the operator ↓ can then be eliminated.
Résumé 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 le 1er 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é.