A Logical Framework for Modelling Breast Cancer Progression

Abstract

Data streams for a personalised breast cancer programme could include collections of image data, tumour genome sequencing, likely at the single cell level, and liquid biopsies (DNA and Circulating Tumour Cells (CTCs)). Although they are rich in information, the full power of these datasets will not be realised until we develop methods to model the cancer systems and conduct analyses that transect these streams. In addition to machine learning approaches, we believe that logical reasoning has the potential to provide help in clinical decision support systems for doctors. We develop a logical approach to modelling cancer progression, focusing on mutation analysis and CTCs, which include the appearance of driver mutations, the transformation of normal cells to cancer cells in the breast, their circulation in the blood, and their path to the bone. Our long term goal is to improve the prediction of survival of metastatic breast cancer patients. We model the behaviour of the CTCs as a transition system, and we use Linear Logic (LL) to reason about our model. We consider several important properties about CTCs and prove them in LL. In addition, we formalise our results in the Coq Proof Assistant, thus providing formal proofs of our model. We believe that our results provide a promising proof-of-principle and can be generalised to other cancer types and groups of driver mutations.

Appendices

Appendix

A Proof of the Adequacy Results

Theorem 1:

Adequacy. Let s be a state and . Then, $(s',r,d)\in S_s$ iff focusing on the encoding of r leads to the following derivation.

Proof

The encoding of the rule r is a bipole [2] (i.e., a formula that, being focused, will produce a single positive and a single negative phases) of the form

Focusing on this formula (stored in ) necessarily produces the following derivation, starting with rule $D_C$ (decision on the classical context):

Here $(\varDelta , \varDelta ')$ is a partition of the atoms in . Since r is fireable in the state s, then $\varDelta$ must contain all the atoms needed to prove and . Moreover, $\varDelta '$ must correspond to the components not affected by the application of r, i.e., . Hence, derivation $\pi$ takes the form:

This means that . On the other hand, derivation $\psi$ starts with the release rule R (since $\otimes _L$ must be introduced in the negative phase and then, focusing is lost) and we have

In the last sequent, the negative phase ends. Note that the set corresponds to .

Corollary 1:

Adequacy. Let s and $s'$ be two states. Then iff the sequent is provable.

Proof

Note that after the negative phase, we have:

where $\varDelta$ is the multiset of atoms in . We cannot focus on those atoms (since they are positive). Moreover, we cannot focus on (since the atom is not in $\varDelta$ nor in ). Hence, we can only focus on the formulas in . We conclude by focusing on the encoding of r and using Theorem 1.

The proof of Corollary 2 follows easily from Theorem 1.

B Proof of the Properties of the Model

Property 1

The following sequent is provable:

Proof

After the negative phase (using the rules $\forall _R$, $\otimes _L$, ), we have only one proof obligation: , where G is

Note that the only non-atomic formulas are G and those formulas in . The proof proceeds by focusing, several times, on the formulas in thus transforming the state . In the end, we focus on G and the proof ends. Using the rules of the system as macro logical rules (see Corollary 2), we have the following:

In the above derivation, we note that, in the last sequent (bottom-up) we already reach the state , with delay $t_d=d_{42}(3)+d_{52}(5)+d_{72}(7)$. Hence, the derivation $\pi$ corresponds to focusing and decomposing entirely the formula G:

Property 2

The following sequent is provable:

Proof

After the negative phase (using the rules $\forall _R$, $\otimes _L$, $\oplus _L$, ), we have two proof obligations (due to $\oplus _L$)

where G is the goal

Let us start with the proof obligation (PO1). Similar to the proof of Property 1, we start by focusing on the formulas in so that we may later focus on G. One of the possible paths/proofs leading to the conclusion of the goal G is the following:

In such a derivation, the rules and could be used zero or more times - as long as the fitness remains positive. Moreover, in the last sequent (bottom-up) we have already reached the state , with delay $t_d=d_{40}(3)+d_{42}(2)+d_{50}(4)+d_{52}(3)+d_{72}(5)$ and derivation $\pi$ proceeds as in the proof of Property 1.

The proof obligation (PO2) can be discharged similarly by several paths, depending (as in PO1) on the order of mutations and and the eventually many passenger mutations (rules $bl_{ec0}, bl_{ecc0}, bl_{ecc0}$, and $bl_{ecm0}$). We give here the shortest path and one of the longest paths, as an illustration.

Note that along with the time delay $t_d$ we are looking for, the proof provides also the fitness of the extravasating CTC.

Property 3

The following sequents are provable:

Proof

In this case we present the Coq script needed to discard this proof. We prove separately the two sequents above:

Property 4

Let $\varDelta$ be a multiset of atoms of the form . Then, in any derivation of the form

we have .

Proof

We know that the above derivation must start by focusing on one of the formulas in (Theorem in our formalisation). Then, we proceed by case analysis on all of the rules. If the rule is not fireable, then we cannot focus on that rule since the initial rule cannot be applied (and the above derivation is not valid). If the rule can be fired, due to Corollary 2, we know that the resulting St is necessarily the one-step transformation of , that, in this case, satisfies .

Property 5

Let $\varDelta$ be a multiset of atoms of the form . Then, in any derivation of the form

with m containing , it must be the case that

• 1. either ,

• 2. or ,

• 3. or with $m'$ being as m plus an additional mutation,

• 4. or with .

Proof

In this case we present the Coq script needed to discard this proof. Definition is just a shorthand to denote the goal we need to prove.