Computational Logic for Biomedicine and Neurosciences

TL;DR

This paper advocates for using computational logic, especially proof-theoretic frameworks like CIC and Coq, to model, verify, and analyze biological and neuroscientific systems, aiming for reliable and formalized biomedical applications.

Contribution

It introduces a unified logical framework based on linear logic and CIC for modeling and verifying biological and neural systems, with formal proofs implemented in Coq.

Findings

Formal semi-automatic proofs for simple biological models in Coq

Modeling neurons and circuits with CIC and Coq

Potential for disease diagnosis and therapy prognosis

Abstract

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.