Formal Reasoning about Molecular Pathways in Higher Order Logic

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.



Proposed Methodology


  1. S. Ahmad, O. Hasan, U. Siddique and S. Tahar, “Formalization of Z-Syntax to reason about Molecular Pathways in HOL4”, Brazilian Symposium on Formal Methods (SBMF-2014), Springer LNCS, Maceio, AL, Brazil, To Appear.

  2. S. Ahmad, O. Hasan and U. Siddique, “Towards Formal Reasoning about Molecular Pathways in HOL ”, 23rd IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE), Parma, Italy, pp. 378 – 383.