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.