Integration and Interaction of multiple mathematical reasoning processes

Synopsis: The aim of the project was the automation of mathematical reasoning processes, including their analysis, development and interaction. These processes included: 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. In particular, the Platform provided the opportunity to:
- Develop, document and maintain our research platforms, e.g., IsaPlanner.
- To explore new mechanisms for mathematical reasoning, their integration and interaction.
- To explore diverse applications of mathematical reasoning.
- To use the flexibility it provided significantly to improve the productivity and effectiveness of our research via support for students, etc.
Results: The Platform Grant pump primed a large number of activities within the area of interacting mathematical reasoning processes. It enabled us to explore new directions and establish new projects that were adventurous, but on which we could demonstrate solid initial progress. During the project period, five new research grants can be directly attributed to pump-priming by the Platform Grant. It has also enabled us to maintain and develop the generic software that underpins much of our work, especially IsaPlanner, our proof planning system that guides and repairs proofs by mathematical induction.