  We advocates here the use of (mathematical) logic for systems biology, as a
unified framework well suited for both modeling the dynamic behaviour of
biological systems, expressing properties of them, and verifying these
properties. The potential candidate logics should have a traditional proof
theoretic pedigree (including a sequent calculus presentation enjoying
cut-elimination and focusing), and should come with (certified) proof tools.
Beyond providing a reliable framework, this allows the adequate encodings of
our biological systems. We present two candidate logics (two modal extensions
of linear logic, called HyLL and SELL), along with biological examples. The
examples we have considered so far are very simple ones-coming with completely
formal (interactive) proofs in Coq. Future works includes using automatic
provers, which would extend existing automatic provers for linear logic. This
should enable us to specify and study more realistic examples in systems
biology, biomedicine (diagnosis and prognosis), and eventually neuroscience.
