However, a major limitation of this work is that it cannot cater for the temporal information associated with biological processes and, hence, does not support modeling the time evolution of molecular populations involved in a biological network, which is of a dire need when studying the dynamics of a biological system. Reaction kinetics [ 14 ] provide the basis to understand the time evolution of molecular populations involved in a biological network.
To overcome the limitation of the work presented by Sohaib et al. In this section, we provide a brief introduction to the higher-order-logic theorem proving and HOL Light theorem prover. Theorem proving involves the construction of mathematical proofs by a computer program using axioms and hypothesis. Theorem proving systems theorem provers are widely used for the verification of hardware and software systems [ 56 , 57 ] and the formalization or mathematical modeling of classical mathematics [ 58 — 60 ]. For example, hardware designers can prove different properties of a digital circuit by using some predicates to model the circuits model.
Similarly, a mathematician can prove the transitivity property for real numbers using the axioms of real number theory. These mathematical theorems are expressed in logic, which can be a propositional, first-order or higher-order logic based on the expressibility requirement. Based on the decidability or undecidability of the underlying logic, theorem proving can be done automatically or interactively. Propositional logic is decidable and thus the sentences expressed in this logic can be automatically verified using a computer program whereas higher-order logic is undecidable and thus theorems about sentences, expressed in higher-order logic, have to be verified by providing user guidance in an interactive manner.
A theorem prover is a software for deductive reasoning in a sound environment. This is achieved by defining a precise syntax of the mathematical sentences that can be input in the software. Moreover, every theorem prover comes with a set of axioms and inference rules which are the only ways to prove a sentence correct. This purely deductive aspect provides the guarantee that every sentence proved in the system is actually true.
HOL Light [ 19 ] is an interactive theorem prover used for the constructions of proofs in higher-order logic. The logic in HOL Light is represented in meta language ML , which is a strongly-typed functional programming language [ 61 ]. A theorem is a formalized statement that may be an axiom or could be deduced from already verified theorems by an inference rule.
Users interacting with HOL Light can reload a theory and utilize the corresponding definitions and theorems right away. HOL Light theories are organized in a hierarchical fashion and child theories can inherit the types, constants, definitions and theorems of the parent theories. The HOL Light theorem prover provides an extensive support of theorems regarding Boolean variables, arithmetics, real numbers, transcendental functions, lists and multivariate analysis in the form of theories which are extensively used in our formalization. The proofs in HOL Light are based on the concept of tactics which break proof goals into simple subgoals.
There are many automatic proof procedures and proof assistants [ 62 ] available in HOL Light, which help the user in concluding a proof more efficiently. The proposed theorem proving based formal reasoning framework for system biology, depicted in Fig 1 , allows the formal deduction of the complete pathway from any given time instance and model and analyze the ordinary differential equations ODEs corresponding to a kinetic model for any molecular reaction.
For this purpose, the framework builds upon existing higher-order-logic formalizations of Lists, Pairs, Vectors, and Calculus.
The two main rectangles in the higher-order logic block present the foundational formalizations developed to facilitate the formal reasoning about the Zsyntax based pathway deduction and the reaction kinetics. In order to perform the Zsyntax based molecular pathway deduction, we first formalize the functions representing the logical operators and inference rules of Zsyntax in higher-order logic and verify some supporting theorems from this formalization. This formalization can then be used along with a list of molecules and a list of Empirically Valid Formulae EVFs to formally deduce the pathway for the given list of molecules and provide the result as a formally verified theorem using HOL Light.
Similarly, we have formalized the flux vectors and stoichiometric matrices in higher-order-logic. These foundations can be used along with a given list of species and the rate of the reactions to develop a corresponding ODEs based kinetic reactions model.
Department of Physics
The solution to this ODE can then be formally verified as a theorem by building upon existing formalizations of Calculus theories. The distinguishing characteristics of the proposed framework include the usage of deductive reasoning to derive the deduced pathways and solutions of the reaction kinetic models. Thus, all theorems are guaranteed to be correct and explicitly contain all required assumptions. Zsyntax [ 13 ] is a formal language which exploits the analogy between biological processes and logical deduction. Some of its key features are that: 1 it enables us to represent molecular reactions in a mathematical rigorous way; 2 it is of heuristic nature, i.
Zsyntax has three operators namely Z-Interaction , Z-Conjunction and Z-Conditional that are used to represents different phenomenon in a biological process.
These are the atomic formulas residing in the core of Zsyntax. In biological reactions, the Z-interaction operation is not associative. These molecules can be same or different. Unlike the Z-Interaction operator, the Z-Conjunction is fully associative. To apply the above-mentioned operators on a biological process, Zsyntax provides four inference rules that are used for the deduction of the outcomes of the biological reactions.
These inference rules are given in Table 1.
Lawrence R. Pratt | School of Science & Engineering
Zsyntax also utilizes the EVFs which are the empirical formulas validated in the lab and are basically the non-logical axioms of molecular biology. A biological reaction can be mapped and then these above-mentioned Zsyntax operators and inference rules are used to derive the final outcome of the reaction as shown in [ 13 ]. Using this data type, we can apply the Z-Conjunction operator between individual molecules a list with a single element , or between multiple interacting molecules a list with multiple elements.
Thus, based on our datatype, Z-Conjunction is a list of Z-interactions for both of these cases, i. So, overall, Z-conjunction acts as a set of Z-interaction. When a new set of molecules is generated based on the EVFs available for a reaction, the status of the molecules is updated using the Z-Conditional operator.
Next, we formalize the inference rules using higher-order logic. Thus, both of these rules can be handled by the simplification and rewriting rules of the theorem prover and we do not need to define new rules for handling these inference rules. We apply it at the end of the biological reaction to check whether the product of the reaction is the desired molecule or not.
If the condition is true, it returns the given element x as a single element of that list l.
Otherwise, it returns the list l as is, as shown in Fig 2a. This rule is basically the append operation of lists, based on the above data types defined in our formalization. It takes a list l and two of its elements x and y , and appends the list of these two elements on its head as shown in Fig 2b. According to laws of stoichiometry [ 13 ], we have to delete the initial reacting molecules from the main list, for which the Z-Conjunction operator is applied.
The function checks if the index x is greater than the index y , i. If the condition is true, then it deletes the x th element first and then the y th element. In this deletion process, to make sure that the deletion of first element will not affect the index of the other element that has to be deleted, we delete the element present at the higher index of list before the deletion of the lower indexed element. We aim to build a framework that takes the initial molecules of a biological experiment along with the possible EVFs and enables us to deduce its corresponding final outcomes.
Upon finding no match, this function returns a pair having first element as false F , which acts as a flag and indicates that there is no match between any of the EVFs and the corresponding molecule, whereas the second element of the pair is the tail of the corresponding list l of the initial molecules. If a match is found, then the function will return a pair with its first element as a true T , which indicates the confirmation of the match that have been found, and the second element of the pair is the modified list l , whose head is removed, and the second element of the corresponding EVF pair is added at the end of the list and the matched elements are deleted as these have already been consumed.
Otherwise, it recursively checks for the match with all of the remaining values of the variable x. This iterative process continues until no match is found in the execution of these functions. In order to guarantee the correct operation of deduction, we instantiate the variable of recursion q with a value that is greater than the total number of EVFs so that the application of none of the EVF is missed.
Similarly, in order to ensure that all the combinations of the list l are checked against the entries of the EVF list e , the value LENGTH l - 1 is assigned to both of the variables x and y. More detail about the behavior of all of these functions can be found in our proof script [ 63 ].
These formal definitions enable us to check recursively all of the possible combinations of the molecules, present in the initial list l , against each of the first element of the list of EVFs e. Upon finding a match, the reacting molecules are replaced by their outcome in the initial list of molecules l by applying the corresponding EVF.
This process is repeated on the current updated list of molecules until there are no further molecules reacting with each other. The list l at this point contains the post-reaction molecules. In order to prove the correctness of the formal definitions presented above, we verify a couple of key properties of Zsyntax involving operators depicting the vital behaviour of the molecular reactions. The first verified property captures the scenario when there is no reacting molecule present in the initial list of the experiment.
As a result of this scenario, the post-experiment molecules are the same as the pre-experiment molecules.