| EP/N014758/1 | The Integration and Interaction of Multiple Mathematical Reasoning Processes | (C) |
| EP/J020524/1 | Interpreting and integrating mismatched data on the fly | (P) |
| EP/J001058/1 | The Integration and Interaction of Multiple Mathematical Reasoning Processes | (C) |
| EP/H024204/1 | AI4FM: using AI to aid automation of proof search in Formal Methods | (P) |
| EP/H023119/1 | The potential of automated reasoning tools to assist the working mathematician | (P) |
| EP/H043055/1 | The 2010 Federated Logic Conference | (C) |
| EP/G000700/1 | Ontology Evolution in Physics | (P) |
| EP/F033559/1 | Automated Theorem Discovery | (P) |
| EP/E005713/1 | The Integration and Interaction of Multiple Mathematical Reasoning Processes. | (P) |
| EP/E005322/1 | Automated Reasoning in Large Structured Theories | (C) |
| GR/S98139/01 | Automated Analysis of Security Critical Systems | (P) |
| GR/S76328/01 | The use of Data-Mining Techniques for the Automatic Formation of Tactics | (P) |
| GR/S62949/01 | Inferring Quality of Service Properties for Grid Applications | (P) |
| GR/S31099/01 | Automated Discovery in Mathematics | (P) |
| GR/S25388/01 | The Application of Deductive Synthesis Techniques to the Rapid Assembly of Grid Applications | (P) |
| GR/S01771/01 | Platform : The Integration and Interaction of Multiple Mathematical Reasoning Processes | (P) |
| GR/R84559/01 | Applying HR to the Study of Zariski Spaces | (P) |
| GR/R52954/01 | Flexible incorporation of decision procedures into the LambdaClam proof-planning system | (P) |
| GR/M98012/01 | AUTOMATIC CONJECTURE MAKING IN MATHEMATICS | (P) |
| GR/M46624/01 | MECHANISING FIRST - ORDER TEMPORAL LOGICS | (C) |
| GR/M32443/01 | UNIFYING PROOF PLANS AND SCHEMAS FOR PROGRAM SYNTHESIS AND TRANSFORMATION | (P) |
| GR/M45030/01 | COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING | (P) |
| GR/L14381/01 | AUTOMATIC GUIDENCE OF MECHANICALLY GENERATED PROOFS | (P) |
| GR/L11724/01 | COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING | (P) |
| GR/K84981/01 | DIFFERENCE REDUCTION TECHNIQUES IN AUTOMATING THEOREM PROVING | (P) |
| GR/J80702/01 | COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING | (P) |
| GR/J59111/01 | THE RELATIONSHIP BETWEEN FORMAL AND INFORMAL PROOFS | (P) |
| GR/J58619/01 | COMMUNICATION IN SAFTEY CASES - A SEMANTIC APPROACH | (C) |
| GR/J05903/01 | APPLICATION OF LOGIC TO AUTOMATED PROGRAM DEVELOPMENT | (P) |
| GR/H23610/01 | COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING | (P) |
| GR/G35565/01 | PROGRAM SYNTHESIS AND TRANSFORMATION USING INTUITIONIST TYPE THEORY AND PROOF PLANS | (P) |
| GR/F69703/01 | PROGRAM SYNTHESIS AND TRANSFORMATION USING INTUITIONIST TYPE THEORY AND PROOF PLANS | (P) |
| GR/F71799/01 | COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING | (P) |