Sohaib Ahmad and Osman Hasan
Recent progress in nanotechnology and optical imaging offers promising features to develop effective drugs to cure chronic diseases, such as cancer and malaria. However, qualitative characterization of biological organisms (such as molecules) is the foremost requirement to identify key drug targets. One of the most widely used approaches in this domain is molecular pathways, which offers a systematic way to represent and analyze complex biological systems. Traditionally, such pathways are analyzed using paper-and-pencil based proofs and simulations. However, these methods cannot ascertain accurate analysis, which is a serious drawback given the safety-critical nature of the applications of molecular pathways. To overcome these limitations, we propose to formally reason about molecular pathways within the sound core of a theorem prover. As a first step towards this direction, we formally express three logical operators and four inference rules of Zsyntax, which is a deduction language for molecular pathways. After Zsyntax formalization, we extend this approach by verifying a couple of behavioral properties of Zsyntax based deduction using the HOL4 theorem prover and developing a biologist friendly graphical user interface. Moreover, we demonstrate the utilization of our work by presenting the formal analysis of cancer related molecular pathway, i.e., TP53 degradation and metabolic pathway known as Glycolysis.