The Integration and Interaction of Multiple Mathematical Reasoning Processes

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

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.