Towards Formal Reasoning about Molecular Pathways in HOL

A molecular pathway primarily refers to a chain of chemical reactions within a cell and their analysis plays a vital role in developing effective drugs for various human infectious diseases, such as Cancer and Malaria. However, the existing cell pathway analysis techniques, such as paper and pencil proof methods, graph theory and Petri Nets, are either incapable of assuring accurate results or only deal with certain biological systems, which limits the usage of these techniques in the safety-critical field of human medicine. In this paper, we propose to use higher-order-logic theorem proving to accurately deduce results of biological reactions in a pathway. The proposed framework is primarily based on Z-Syntax, which is a formal language to model molecular reactions and is based on three logical operators and four inference rules. As a first step towards this goal, we formalize these operators and inference rules in higher-order logic and provide automated reasoning support for verifying molecular reactions using the HOL4 theorem prover. For illustration purposes, we present the formal verification of a reaction involving TP53 degradation.