权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Cool: Coalgebras, Ontologies and Logic

酷：代数、本体论和逻辑

基本信息

批准号：
EP/H016317/1
负责人：
Dirk Pattinson
金额：
$ 50.17万
依托单位：
Imperial College London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2010
资助国家：
英国
起止时间：
2010 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FH016317%2F1
关键词：
Cool Coalgebras Ontologies Logic

项目摘要

The main theme that underlies this research project is automatedreasoning, an applied sub-discipline of mathematical logic. Logichas found applications in many areas of computer sciencesuch as the verification of digital circuits, reasoning aboutprograms and knowledge representation. One of the most fundamentalaspects in this context is to automatically decide whether aparticular formula is a logical consequence of a given set ofassumptions. The set of assumptions may describe complex relationsbetween diseases and their symptoms, and one possible reasoning taskwould be to confirm or reject a diagnosis based on observed symptomsand medical history.In this research project, we investigate applications ofmathematical logic in knowledge representation. One of the primechallenges in this area is to design logical formalisms that strikea balance between the two conflicting goals of expressiveness (theability to formally represent the application domain) andcomputational tractability. The family of modal logics, conceived ina broad way, combines both aspects and serves as the mathematicalfoundation of a large number of knowledge representation formalisms.The core ingredient of modal logic is the possibility to qualifylogical assertions to hold in a certain way. Depending on thecontext, we may for instance stipulate that assertion holds `alwaysin the future', `with a likelihood of at least 50%' or `normally'.Together with names for individual entities, this allows us toformulate assertions like `the likelihood of congestion on Queen'sRoad is greater than 30%', and complex knowledge bases arise bycombining different logical primitives. Automated reasoning thenallows us to mechanically verify e.g. the consistency of scientifichypotheses against an existing knowledge base. Our goal is to builda modular and practical knowledge representation system that allowsto represent and reason about knowledge represented in this way,based on a large and diverse class of logical primitives, includinge.g. the coalitional behaviour of agents, quantitative uncertainty,counterfactual reasoning and default assumptions. This goes waybeyond the current state of the art, where only logical primitiveswith a relational interpretation are supported by automated tools.Recent research has shown these new logical features can beaccounted for in a uniform way by passing to a more generalmathematical model, known as `coalgebraic semantics'. This richerframework does not only provide a uniform umbrella for a largenumber of reasoning principles, but also supports a richmathematical theory that has by now matured to the extent which putsthe development of automated tools within reach. The researchchallenge that this proposal addresses is the further development of thesetheoretical results as to bring them to bear on practical applications.As a concrete case study, we will use the Cool system to formalisequantitative models in Systems Biology.

这项研究项目的主要主题是自动推理，这是数理逻辑的一个应用子学科。逻辑学在计算机科学的许多领域都有应用，如数字电路的验证、程序推理和知识表示。在这种情况下，最基本的方面之一是自动确定特殊公式是否是一组给定假设的逻辑结果。这组假设可以描述疾病及其症状之间的复杂关系，一种可能的推理任务是根据观察到的症状和病史来确认或拒绝诊断。在本研究项目中，我们研究了数理逻辑在知识表示中的应用。这一领域的主要挑战之一是设计逻辑形式，以便在表现力(形式化表示应用程序领域的能力)和计算可操纵性这两个相互冲突的目标之间取得平衡。广义上构思的模态逻辑族结合了这两个方面，是大量知识表示形式主义的数学基础，其核心成分是以某种方式限定逻辑断言的可能性。例如，根据上下文的不同，我们可以规定断言“未来总是成立”、“至少有50%的可能性”或“正常情况下”。与个别实体的名称一起，这允许我们提出诸如“皇后大道拥堵的可能性大于30%”这样的断言，而复杂的知识库是通过组合不同的逻辑原语而产生的。然后，自动推理允许我们机械地验证科学假设与现有知识库的一致性。我们的目标是建立一个模块化和实用的知识表示系统，允许基于一大类不同的逻辑原语来表示和推理以这种方式表示的知识，例如。代理人的联合行为、数量不确定性、反事实推理和违约假设。这远远超出了目前的技术水平，自动化工具只支持带有关系解释的逻辑原语。最近的研究表明，这些新的逻辑特征可以通过传递到一个更通用的数学模型来统一解释，即所谓的协代数语义。这个丰富的框架不仅为大量推理原理提供了一个统一的保护伞，而且还支持了一个丰富的数学理论，该理论现在已经成熟到了使自动化工具的开发触手可及的程度。作为一个具体的案例研究，我们将使用COOL系统来形式化系统生物学中的等价性模型。