The Integration and Interaction of Multiple Mathematical Reasoning Processes

多种数学推理过程的整合与交互

• 批准号: EP/J001058/1
• 负责人: Andrew Ireland
• 金额: $ 145.3万
• 依托单位: Heriot-Watt University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2011
• 资助国家: 英国
• 起止时间: 2011 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FJ001058%2F1
• 关键词: Integration; Interaction; Multiple; Mathematical; Reasoning

The proposed Platform Grant renewal will be used to provide essential infrastructure and exploratory activities that will support a portfolio of projects that focus on the automation of mathematical reasoning processes, including their analysis, development and interaction. We can be broadly classified by our "holistic" perspective of automated reasoning. Central to this theme is the interplay between representation and reasoning. Discovering the "right" representation can often dramatically simplify the reasoning required in solving a problem. Conversely, meta-level reasoning, and in particular proof-failure analysis, can often provide guidance in evolving the "right" representation. The renewal of the Platform Grant will enable us to maintain and strengthen the momentumthat has been build up around this theme -- both in terms of basic research aswell as applications: The former covers a spectrum of topics, including:cognitive aspects of theory formulation and reformulation; mathematical discovery and automatic theorem generation; ontology creation,repair and evolution; proof procedures; proof planning; AI problem reformulation;quantum computation; computational creativity; visualisation of reasoning processes. The latter covers wide ranging applications such as: software verification; formalmodelling of software intensive systems; graphics design; games design; disaster recovery planning. Our work is a unique blend of the techniques of artificial intelligence and theoretical computer science -- we also believe we are unique in ourholistic perspective of automated reasoning and mathematical discovery.

拟议的平台赠款展期将用于提供必要的基础设施和探索活动，以支持一系列项目，这些项目侧重于数学推理过程的自动化，包括其分析、开发和互动。我们可以根据我们对自动推理的“整体”观点进行广泛的分类。这一主题的核心是表征和推理之间的相互作用。发现“正确”的表示法通常可以大大简化解决问题所需的推理。相反，元级推理，特别是证明失败分析，往往可以提供指导，在发展的“正确”的表示。平台资助的更新将使我们能够保持和加强围绕这一主题建立的势头-无论是在基础研究还是应用方面：前者涵盖了一系列主题，包括：理论制定和重新制定的认知方面;数学发现和自动定理生成;本体创建，修复和进化;证明程序;证明规划;人工智能问题重新制定;量子计算;计算创造力;推理过程的可视化。后者涵盖了广泛的应用，如：软件验证; formalmodeling软件密集型系统;图形设计;游戏设计;灾难恢复规划。我们的工作是人工智能和理论计算机科学技术的独特融合-我们也相信我们在自动推理和数学发现的整体视角方面是独一无二的。

项目成果

Checking Contact Tracing App Implementations

检查接触者追踪应用程序的实施情况

• DOI: 10.5220/0010237201330144
• 发表时间: 2021
• 作者: Aspinall D

The Use of Automated Theory Formation in Support of Hazard Analysis

使用自动理论形成支持危害分析

• 发表时间: 2018
• 作者: A. Ireland

A multi-lingual Ontology Matcher

多语言本体匹配器

• 发表时间: 2015
• 作者: Bella, G.

Logic for Programming, Artificial Intelligence, and Reasoning

编程逻辑、人工智能和推理

• DOI: 10.1007/978-3-642-45221-5_9
• 发表时间: 2013
• 作者: Benzmüller C

Multilingual Ontology Matching

多语言本体匹配

• 发表时间: 2015
• 作者: Bella, G.