The Integration and Interaction of Multiple Mathematical Reasoning Processes.

拟议的平台赠款将用于提供必要的基础设施和探索性活动，以支持以下总体目标范围内的项目组合。数学推理组的研究目标是数学推理过程的自动化，包括它们的分析、开发和交互。这些过程包括：概念形成；理论形成;猜想制作;证明和反例查找；学习新的证明方法和批评；证明的提出和证据的检索；以及对猜想、表述和理论的改进、修正和维护。重点将继续放在指导证明搜索的机制上，特别是证明计划的进一步发展，它将包括正式和“非正式”推理，例如图解推理、示意图证明和类比、抽象、反射、对称和多智能体搜索控制的使用。我们期望在系统设计、系统生物学、常识推理和为数学家提供计算辅助的形式化方法中找到这项工作的应用。我们的工作是人工智能技术和理论计算机科学的独特融合。

The proposed platform grant will be used to provide essential infrastructure and exploratory activities that will support a portfolio of projects within the overall aims described below.The research aims of the Mathematical Reasoning Group are the automation of mathematical reasoning processes, including their analysis, development and interaction. These processes willinclude: concept formation; theory formation; conjecture making; proof and counterexample finding; the learning of new proof methods and critics; the presentation of proofs and proof search; and the refinement, revision and maintenance of conjectures, representations and theories. A major focus will continue to be on mechanisms for guiding proof search, especially the further development of proof planning, and it will include both formal and `informal' reasoning, for instance diagrammatic reasoning, schematic proof and the use of analogy, abstraction, reflection, symmetry and multi-agent search control. We expect to find applications of this work in formal methods of system design, system biology, commonsense reasoning, and the provision of computational aids for mathematicians. Our work is a unique blend of the techniques of artificial intelligence and theoretical computer science.