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 http://arxiv.org/abs/1811.02478
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?
[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