The Integration and Interaction of Multiple Mathematical Reasoning Processes

点击翻译按钮获取中文摘要

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.