Proof search in a context-sensitive logic for molecular biology

We study the proof theory and the automatic proof search for a fragment of linear logic with context-sensitive deductions inspired by molecular biology. We formulate an intuitionistic (multiplicative) linear logic sequent calculus where sequents are decorated so to account for the biological constraints. We then draw on the literature to develop a generalized proof search technique that allows to automatically deal with context-sensitive deductions and non-monotonic reasoning. Finally, we present the implementation of a theorem prover that can be used to automatically verify biological pathways expressed as logical sequents.