Electronic Appendix
A Logical Framework for Systems Biology, Elisabetta de Maria,
Joëlle Despeyroux, and Amy P. Felty, in
Proceedings of the First International Conference Formal Methods
in Macro-Biology (FMMB),
Springer-Verlag LNCS,
September 2014.
Appendices A and B
Extended Report
An extended version is available here. It
contains the sequent proofs of all 4 properties.
Coq Files
The files run in Coq V8.4pl2.
They must be compiled in the order they are listed.
Lambda Prolog Files
Tactic proof scripts for HyLL proofs of the 4 properties described in
the paper. (These scripts are read in by the Lambda Prolog prover and
translated to Coq script, which is imported and then fine-tuned to
complete the above Coq proof development.)
- property1.hyll: Property 1, version 1
- property1a.hyll: Property 1, version
2, subgoal 1
- property1b.hyll: Property 1, version
2, subgoal 2
- property2.hyll: Property 2
- property3_0.hyll: Property 3, base
case
- property3_1.hyll: Property 3, case
for rule 1
- property3_2.hyll: Property 3, case
for rule 2
- property3_3.hyll: Property 3, case
for rule 3
- property3_4.hyll: Property 3, case
for rule 4
- property3_5.hyll: Property 3, case
for rule 5
- property3_6.hyll: Property 3, case
for rule 6
- property4_1.hyll: Property 4, case
for rule 1
- property4_2.hyll: Property 4, case
for rule 2
- property4_3.hyll: Property 4, case
for rule 3
- property4_4.hyll: Property 4, case
for rule 4
- property4_5.hyll: Property 4, case
for rule 5
- property4_6.hyll: Property 4, case
for rule 6
The prover is available as a zip file. It runs in the trunk version
of the Teyjus implementation
of Lambda Prolog.