TY - GEN
T1 - A finite model theory for biological hypotheses
AU - Racunas, Stephen
AU - Griffin, Christopher
AU - Shah, Nigam
PY - 2004
Y1 - 2004
N2 - We have designed and implemented a set of software tools for the composition and evaluation of hypotheses about gene regulation in biological systems. Our software uses a unified formal grammar for the representation of both diagram-based and text-based hypotheses. The objective of this paper is to show how to use this grammar as the basis for an effective logic for specifying hypotheses about biological systems in precise model-theoretic terms. To accomplish this, we take inspiration from inflationary extensions to fixed point logics and define a new type of logic: a deflationary logic for describing the effects of experiments upon models of biological systems. We present results that characterize decidability, satisfiability, and inflationary/deflationary properties of this logic. We formally define what it means for a set of assertions to be discoverable under this new logic, and show that our software generates discoverable queries. Thus, we lay the groundwork for a formal treatment of machine-aided experimental design under the conceptual framework we have developed for our hypothesis evaluation software.
AB - We have designed and implemented a set of software tools for the composition and evaluation of hypotheses about gene regulation in biological systems. Our software uses a unified formal grammar for the representation of both diagram-based and text-based hypotheses. The objective of this paper is to show how to use this grammar as the basis for an effective logic for specifying hypotheses about biological systems in precise model-theoretic terms. To accomplish this, we take inspiration from inflationary extensions to fixed point logics and define a new type of logic: a deflationary logic for describing the effects of experiments upon models of biological systems. We present results that characterize decidability, satisfiability, and inflationary/deflationary properties of this logic. We formally define what it means for a set of assertions to be discoverable under this new logic, and show that our software generates discoverable queries. Thus, we lay the groundwork for a formal treatment of machine-aided experimental design under the conceptual framework we have developed for our hypothesis evaluation software.
UR - http://www.scopus.com/inward/record.url?scp=14044254817&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=14044254817&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:14044254817
SN - 0769521940
SN - 9780769521947
T3 - Proceedings - 2004 IEEE Computational Systems Bioinformatics Conference, CSB 2004
SP - 616
EP - 620
BT - Proceedings - 2004 IEEE Computational Systems Bioinformatics Conference, CSB 2004
T2 - Proceedings - 2004 IEEE Computational Systems Bioinformatics Conference, CSB 2004
Y2 - 16 August 2004 through 19 August 2004
ER -