Formal reasoning about synthetic biology using higher-order-logic theorem proving.

Synthetic biology is an interdisciplinary field that uses well-established engineering principles for performing the analysis of the biological systems, such as biological circuits, pathways, controllers and enzymes. Conventionally, the analysis of these biological systems is performed using paper-and-pencil proofs and computer simulation methods. However, these methods cannot ensure accurate results due to their inherent limitations. Higher-order-logic (HOL) theorem proving is proposed and used as a complementary approach for analysing linear biological systems, which is based on developing a mathematical model of the genetic circuits and the bio-controllers used in synthetic biology based on HOL and analysing it using deductive reasoning in an interactive theorem prover. The involvement of the logic, mathematics and the deductive reasoning in this method ensures the accuracy of the analysis. It is proposed to model the continuous dynamics of the genetic circuits and their associated controllers using differential equations and perform their transfer function-based analysis using the Laplace transform in a theorem prover. For illustration, the genetic circuits of activated and repressed expressions and autoactivation of protein, and phase lag and lead controllers, which are widely used in cancer-cell identifiers and multi-input receptors for precise disease detection, are formally analyzed.