Re: [isabelle] "Proofs of Life"/axiomatics for all

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

accompanying video, with proof visualization and more:

I've been unable to find a venue that's prepared to take on the task of reviewing the work. The little feedback I've been able to obtain seems to indicate that the desk/chief editors were unwilling to go ahead with work that does not fit within their prior experiences. Of course, this leaves no room for multi- and antedisciplinary[*] efforts like Proofs of Life. My suggestions of an editor group have been roundly ignored.

Does anyone know of places with a proven record for mixed work?

Outside-the-box thoughts?

[The arXiv version is up to v3. The changes have mostly been about background and, in particular, about translating axiomatic reasoning and its meta-theory-carried implications into the languages of the other naturally-involved subjects. The manuscript is slightly too big for most wide-audience venues as it stands.]


[*] Sean R. Eddy. “Antedisciplinary” science. PLoS Computational Biology, 1(1), 2005.


We axiomatize the molecular-biology reasoning style, show compliance of the standard reference: Ptashne, A Genetic Switch, and present proof-theory-induced technologies to help infer phenotypes and to predict life cycles from genotypes. The key is to note that `reductionist discipline' entails constructive reasoning: any proof of a compound property can be decomposed to proofs of constituent properties. Proof theory makes explicit the inner structure of the axiomatized reasoning style and allows the permissible dynamics to be presented as a mode of computation that can be executed and analyzed. Constructivity and execution guarantee simulation when working over domain-specific languages. Here, we exhibit phenotype properties for genotype reasons: a molecular-biology argument is an open-system concurrent computation that results in compartment changes and is performed among processes of physiology change as determined from the molecular programming of given DNA. Life cycles are the possible sequentializations of the processes. A main implication of our construction is that formal correctness provides a complementary perspective on science that is as fundamental there as for pure mathematics. The bulk of the presented work has been verified formally correct by computer.

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