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 momentum
that has been build up around this theme -- both in terms of basic research as
well 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; formal
modelling 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 our
holistic perspective of automated reasoning and mathematical discovery.

Issues of representation and reasoning are fundamental to the digital age
in which we live. Our research agenda therefore has potential wide ranging
impact as highlighted below:

* Academia: Our research results are published across a wide spectrum of
venues, i.e. journals, conferences, workshops that focus on automated software
engineering, formal methods, automated reasoning, ontologies, logic and
computation, software verification, artificial intelligence, computational creativity,
theoretical computer science, knowledge management. This diversity underlines
the fundamental nature of our work. We also take lead roles in the Scottish Theorem
Proving and Scottish Programming Languages networks, as well as the
Scottish Informatics and Computer Science Alliance. We also collaborate
with over ten international leading research groups.

* Public sector: A major challenge for local and central government
is how to effectively deal with the transparency of public data.
That is, large volumes of public data need to be made available in
linked forms, with the intent of making the data intelligible and
reusable. Our ontology creation, repair and evolution work has
significant potential in this area of data transparency.

* Business and industry: A key differentiator in commercial products is
embedded software, e.g. automotives and mobile technologies. The
dependability of such software remains a major challenge.
Whoever can cost effectively crack the dependability challenge
will have a major commercial advantage. Our group is well placed
to help UK companies address this challenge. In particular, the
tools and techniques we aim to develop to support automated reasoning
and representational change.

In terms of the Digital Economy, we have a track-record within the
creative industries, i.e. games design and graphics design.
More broadly, unreliable software will increasingly impact negatively
on the viability of the Digital Economy, e.g. critical infrastructure
and e-commerce. Again the knowledge, tools and techniques that our
group are exploring will potentially impact on the next generation of
design and verification technologies.

* Security: Failing to meet the challenges posed by Cyber Security
carries significant risks for economic growth and society
in general. Cyber attacks can bring down real-world infrastructure.
Combating Cyber Security threats will call for more scientific methods
in designing software intensive systems than is currently the case.
We believe that our research agenda has the potential to influence
such a change: a change that calls for new methods of representing and
and reasoning about systems; a change that calls for engineers with new skill sets.

* Environmental: Our ontology evolution work has significant potential
in the area of disaster recovery planning. Disparate agencies without
the aid of a shared ontology, need to be able to cooperate and
react dynamically when faced with volatile disaster scenarios and
incomplete data. Our ongoing ontology evolution research will be of
potential benefit to various emergency response services (a UK
spending review priority).

* Education: We are influencing educational policy by responding to
Government papers on educational reform. Furthermore, we are named in
a proposal for funding under the European Cooperation in the field
of Scientific and Technical Research (COST) programme, which,
if successful, will work on mathematical practice and pedagogy.
Our work on automated reasoning and theory formation, in
particular that which models theories of how humans perform
mathematical reasoning, has the potential to deliver a new generation
of computer-aided teaching assistants for mathematics, thus greatly
enhancing the educational process.