II(BIO): BioLogica--Deductive Integration of Heterogeneous Biological Data Sources

网络上的生物学数据的数量和多样性都在不断增长，我们的目标是帮助生物学学生和研究人员有效地利用这些丰富的数据，开发一个概念验证软件助手BioLogica，能够从多个不同的数据源中提取信息。已经组建了一个跨学科小组来开展这项工作。自动逻辑推理将用于实现多个异构生物数据源的语义集成，并回答涉及来自不同数据源的数据组合的查询。一个公理化的生物学理论将被开发的能力1）表达基本的生物学概念和关系2）表示元数据描述不同的数据源的能力，3）理解复杂的查询的含义，4）分解查询成简单的组件，以回答可用的来源和5）组装答案，通过组合多个组件查询的结果。虽然查询可以用英语提出或通过图形用户界面传达，但最终它们被重新表述为命题，即在正式的生物学理论中证明的定理。该定理由自动定理证明器证明，并且从证明中自动提取查询的答案。该项目包括开发正式的生物语言和理论，开发自动形成“程序附件”（访问数据源的软件）的技术，以及发现特定领域的策略来加速定理证明过程。BioLogica将展示空间和时间推理以及应用于特定领域形式理论的更一般推理的应用，为科学数据源的语义集成提供了一种有效的方法。每年将举行研讨会，以使更广泛的社区了解该工具的使用，并就如何改善基础技术.各种计划的学生项目将训练学生整合不同生物数据源和开发生物信息学工具的技术。我们将与感兴趣的教师合作，将该工具的使用纳入课程。社会影响之一是开发一种软件助手，使研究生物学家能够处理令人困惑的多样性可用的在线数据，并使这些数据提供给教师和学生。所提出的原型的自然语言组件能够口语，以及类型，互动。因此，BioLogica可以进行调整，以供有视觉或其他障碍的研究人员和学生使用。预计BioLogica为生物科学引入的技术将更普遍地适用于所有科学中数据源的语义集成。

An overwhelming and growing volume and diversity of biological data is available on the Web.The objective of the proposed work is to help biology students and researchers make effective useof this wealth of data by developing a proof-of-concept software assistant, BioLogica, capable ofinferring information from multiple and diverse data sources. A cross-disciplinary team has beenassembled to carry out this work. Automated logical deduction will be used to achieve semantic integration of multiple heterogeneous biological data sources and to answer queries that involve combination of data from diverse data sources. An axiomatic biological theory will be developed with the ability to 1) Express fundamental biological concepts and relationships2) Represent metadata describing the capabilities of diverse data sources, 3) Understand the meaning of complex queries, 4)Decompose queries into simpler components to be answered by available sources and 5)Assemble answers by combining results from multiple component queries. While queries can be posed in English or conveyed via a graphical user interface, ultimately they are rephrased as conjectures, that is, theorems to be proven in the formal biological theory. The theorem is proven by an automatic theorem prover, and an answer to the query is extracted automatically from the proof. The project includes the development of a formal biological language and theory, the development of techniques to automate the formation of "procedural attachments" (software to access the data sources), and the discovery of domain-specific strategies to accelerate the theorem-proving process. BioLogica will demonstrate that the application of spatial and temporal inference and more general reasoning applied to a domain-specific formal theory provides an effective approach to the semantic integration of scientific data sources.The formal knowledge base and prototype tool will be made available on the Web, and annualworkshops will be held to acquaint the broader community with use of the tool and to exchangeideas about improving the underlying technology. A variety of planned student projects willtrain students in techniques for integration of diverse biological data sources and in developmentof bioinformatics tools. We will work with interested faculty to incorporate use of the tool intocourses. Among the social impacts are developing a software assistant that enables research biologists to deal with the bewildering multiplicity of available online data and making such data available to instructors and students. The natural-language component of the proposed prototype is capable of spoken, as well as typed, interaction. Thus BioLogica could be adapted for use by researchers and students with visual or other impairments. It is expected that the techniques introduced by BioLogica for the biological sciences will more generally be applicable to semantic integration of data sources in all the sciences.