Computational Logic for Biomedicine and Neurosciences

Description

We advocate here the use of computational logic for systems biology, as a \emph{unified and safe} framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including either induction, or a sequent calculus presentation enjoying cut-elimination and focusing), and should come with certified proof tools. Beyond providing a reliable framework, this allows the correct encodings of our biological systems. % For systems biology in general and biomedicine in particular, we have so far, for the modeling part, three candidate logics: all based on linear logic. The studied properties and their proofs are formalized in a very expressive (non linear) inductive logic: the Calculus of Inductive Constructions (CIC). The examples we have considered so far are relatively simple ones; however, all coming with formal semi-automatic proofs in the Coq system, which implements CIC. In neuroscience, we are directly using CIC and Coq, to model neurons and some simple neuronal circuits and prove some of their dynamic properties. % In biomedicine, the study of multi omic pathway interactions, together with clinical and electronic health record data should help in drug discovery and disease diagnosis. Future work includes using more automatic provers. This should enable us to specify and study more realistic examples, and in the long term to provide a system for disease diagnosis and therapy prognosis.

Abstract (French)

Nous pr{\^o}nons ici l'utilisation d'une logique calculatoire pour la biologie des systèmes, en tant que cadre \emph{unifié et sûr}, bien adapté à la fois à la modélisation du comportement dynamique des systèmes biologiques,à l'expression de leurs propriétés, et à la vérification de ces propriétés.Les logiques candidates potentielles doivent avoir un pedigree traditionnel en théorie de la preuve (y compris, soit l'induction, soit une présentation en calcul des séquents, avec l'élimination des coupures et des règles ``focales''), et doivent être accompagnées d'outils de preuves certifiés.En plus de fournir un cadre fiable, cela nous permet d'encoder de manière correcte nos systèmes biologiques. Pour la biologie des systèmes en général et la biomédecine en particulier, nous avons jusqu'à présent, pour la partie modélisation, trois logiques candidates : toutes basées sur la logique linéaire.Les propriétés étudiées et leurs preuves sont formalisées dans une logique inductive (non linéaire) très expressive : le Calcul des Constructions Inductives (CIC).Les exemples que nous avons étudiés jusqu'à présent sont relativement simples. Cependant, ils sont tous accompagnés de preuves formelles semi-automatiques dans le système Coq, qui implémente CIC. En neurosciences, nous utilisons directement CIC et Coq pour modéliser les neurones et certains circuits neuronaux simples et prouver certaines de leurs propriétés dynamiques.En biomédecine, l'étude des interactions entre des voies multiomiques,ainsi que les études cliniques et les données des dossiers médicaux électroniques devraient aider à la découverte de médicaments et au diagnostic des maladies.Les travaux futurs portent notamment sur l'utilisation de systèmes de preuves plus automatiques.Cela devrait nous permettre de modéliser et d'étudier des exemples plus réalistes,et à terme de fournir un système pour le diagnostic des maladies et le pronostic thérapeutique.

Additional details