Re: [isabelle] "Proofs of life"



I should have mentioned earlier that there's an accompanying video, with proof visualization and more:

	http://ceqea.sourceforge.net/extras/instructionalPoL.mp4


On 11/7/18 10:37 AM, Rene Vestergaard wrote:
"Proofs of life: molecular-biology reasoning simulates cell behaviors from first principles" is now available at http://arxiv.org/abs/1811.02478

The work springs from computer-verified reasoning and establishes wider utility by means of a reasoning-computation correspondence, including for long-standing critical problems in biology that have defied standard approaches.

Sincerely,
Rene

-----

ESSENCE
Mathematics-style correctness works for molecular biology and enables phenotype and life-cycle prediction from genotypes. Formally, reductionist science involves constructive reasoning, i.e., executable simulation.

SIGNIFICANCE
Axiomatic reasoning provides an alternative perspective that allows us to address long-standing open problems in biology. Our approach is supported by meta-theory and likely applies to any reductionist discipline.

ABSTRACT
Science relies on external correctness: statistical analysis and reproducibility, with ready applicability but inherent false positives/negatives. Mathematics uses internal correctness: conclusions must be established by detailed reasoning, with high confidence and deep insights but not necessarily real-world significance. Here, we formalize the molecular-biology reasoning style; establish that it constitutes an executable first-principle theory of cell behaviors that admits predictive technologies, with a range of correctness guarantees; and show that we can fully account for the standard reference: Ptashne, A Genetic Switch. Everything works for principled reasons and is presented within an open-ended meta-theoretic framework that seemingly applies to any reductionist discipline. The framework is adapted from a century-long line of work on mathematical reasoning. The key step is to not admit reasoning based on an external notion of truth but work only with what can be justified from considered assumptions. For molecular biology, the induced theory involves the concurrent running/interference of molecule-coded elementary processes of physiology change over the genome. The life cycle of the single-celled monograph organism is predicted in molecular detail as the aggregate of the possible sequentializations of the coded-for processes. The difficult question of molecular coding, i.e., the specific means of gene regulation, is addressed via a detailed modeling methodology. We establish a complementary perspective on science, complete with a proven correctness notion, and use it to make progress on long-standing and critical open problems in biology.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.