Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 22 2022 at 19:22):

From: Rene Vestergaard <renevestergaard@acm.org>
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.]

Cheers,
Rene

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


ABSTRACT
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.


Last updated: Apr 26 2024 at 20:16 UTC