|
We describe a deduction-based approach to biocomputation that semiautomatically combines knowledge, software, and data to satisfy biologists’ goals expressed in a high-level logical language. The approach is implemented in a system called BioDeducta, which combines SRI’s SNARK theorem prover with the BioBike integrated knowledge base and biocomputing platform. The user expresses a high-level conjecture, representing
a biocomputational goal query, without indicating how this goal is to be achieved. A subject domain theory, represented in SNARK’s logical language, expresses the meaning of the terms in the conjecture in terms of the capabilities of the available resources and of the background knowledge necessary to link them together. If the subject domain theory enables SNARK to prove the conjecture—that is, to find paths between the goal and
BioBike resources—then the resulting proofs record various solutions to the conjecture/query. The proofs also provide specific provenance for each result, indicating
in detail how they were computed. In addition to beingentirely open source, a BioDeducta demo server is available on the web in which the examples in this paper can be tested, and further experiments performed.
| |
