Formal Reasoning about Systems Biology using Theorem Proving
PLoS ONE, Vol. 12, No. 3, e0180179, pp. 1–27
Theorem Proving · HOL Light
A theorem-proving framework for formally analyzing biological networks and pathways — applied to cancer-related pathways used in prognosis and drug design.
Abstract
Systems biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, systems-biology models of disease have been analyzed with paper-and-pencil proofs and simulations — methods that cannot provide accurate analysis, a serious drawback in the safety-critical domain of human medicine.
We propose a framework to formally analyze biological networks and pathways: formalizing the notion of reaction kinetics in higher-order logic and formally verifying commonly used reaction-based models using HOL Light, and porting our earlier formalization of Zsyntax — a deductive language for reasoning about biological pathways — from HOL4 to HOL Light. We illustrate the framework on three case studies: the pathway leading to TP53 phosphorylation, the pathway leading to cancer stem cell death, and tumor growth based on cancer stem cells, used for prognosis and future drug design.
Methodology
People
Related Publications