Research
I am interested in exploring how people solve mathematical problems. I computationally model this type of reasoning on computers to enable machines to reason in a similar way to humans. In particular, my research aims to investigate and mechanise some of "informal" humanmathematical reasoning, such as the use of diagrams in proofs of mathematical theorems. Few automated reasoning systems attempt to benefit from the power of human techniques. In my work, I aim to do just that: integrate informal human reasoning techniques with classical formal techniques.
Projects and Grants
Current

Heterogeneous Reasoning
 Phd student Mateja Urbas' project: "Mechanising Heterogeneous Reasoning In Theorem Provers" (2009current)
 EPSRC Advanced Fellowship "Automating Informal Human Mathematical Reasoning" (20022012).
I am looking into combining diagrammatic reasoning with existing symbolic reasoning techniques, like different types of logic, and formalise this socalled heterogeneous reasoning. It should be possible to switch between the two modes of reasoning, diagrammatic and symbolic, at any point in the same proof attempt, but still end up with a formally correct proof. The hope is that ultimately such a system will be able to automatically discover new, interesting and intuitive proofs.

Diagrammatic Reasoning
 NSF Standard Grant "Diagrams 2010 Conference" (2010).
 EPSRC Standard Research Grant "Diagrams 2004 Conference" (2004).
 PhD studentship "Automating Diagrammatic Proofs of Arithmetic Arguments" (19951998).
I investigate the relationship between formal, logical proofs and diagrammatic reasoning proofs. In particular, I am interested in theorems that require mathematical induction to prove them in the usual symbolic way (i.e., proofs which use formulae of some logic as inference steps), but avoid induction in a socalled "diagrammatic proof" (i.e., proofs which use geometric operations of diagrams as inference steps). I implemented these ideas creating a system, DIAMOND, which interactively proves theorems of mathematics by using operations on diagrams. These operations capture the inference steps of the proof.
This work broke new ground in automated reasoning, and is comprehensively described in my book entitled Mathematical Reasoning with Diagrams: From Intuition to Automation (CSLI Press).
 NSF Standard Grant "Diagrams 2010 Conference" (2010).

Women and Computing Research
 10th Anniversary of women@CL event
 1st Oxbridge Women in Computer Science Conference
 Industrial Funding from Microsoft Research, IBM and Google for "women@CL Network". (2008now)
 EPSRC Research Networks Grant "EPSRC Network for Women in Computing Research". (20042008)
I direct women@CL national network (cofounded with Prof. Ursula Martin) that provides local, national and international activities to celebrate, inform and support women who are engaged in careers in computing research and academic leadership. On the local level, I organize monthly lunch talks with inspiring women from all walks of life in computing: from academia, big corporations and small startups. At the request of students, I also organize a Big Sister/Little Sister support and mentoring programme for students.
Past

Learning New Methods in Proof Planning
 Research fellow on EPSRC Standard Research Grant "Formation of Methods for Proof Planning in Mathematics
". (19982002)
 Staff member on EU 5th Framework Grant "Calculemus: System for Integrated Computation and Deduction". (20002004)
I investigate how to automate on machines the learning of general concepts from examples of specific ones, particularly within a proof planning framework. Rather than constructing proofs that consist of low level inference steps, proof planning systems search for proof plans  high level abstract specification of proofs, much like mathematicians' proofs. I designed a system that can automatically learn proving strategies. I used the existing machine learning techniques that I adapted to the domain of reasoning. This research is novel as it enables reasoning machines to acquire new specialised knowledge about proofs automatically.
You can find out more about this project from the project's official web site.
 Research fellow on EPSRC Standard Research Grant "Formation of Methods for Proof Planning in Mathematics
". (19982002)

AgentOriented Theorem Proving
 Research fellow on EPSRC Standard Research Grant "AgentOriented Theorem Proving". (20002001)
I am also interested in using agent technology to integrate several diverse deduction systems in one framework  such systems turn out to be better suited to support interactive and automatic theorem proving.
You can find out more about this project from the project's official web site.
 Research fellow on EPSRC Standard Research Grant "AgentOriented Theorem Proving". (20002001)
PhD Students
 Advait Sarkar: Interactive data mining and visual analytics. Start Date: October 2013. Jointly supervised with Alan Blackwell.
 Matej Urbas: Mechanising Heterogeneous Reasoning In Theorem Provers Start Date: October 2009.
 Daniel Winterstein: Automating Diagrammatic Reasoning in Continuous Domains. Second Supervisor. Completion Date: August 2004.
Here is some information for prospective PhD students.
Professional Activities
Appointments and Peer Review Affiliations
 AAAI  The American association for artificial intelligence. Member.
 AISB  The society for the study of artificial intelligence and the simulation of behaviour. Member.
 EPSRC Peer Review College. Member since 2002.
 women@CL national network project. Director since 2004.
 International Biennial Conference Series on the Theory and Application of Diagrams. Steering Committee member since 2004.
 Annual series of Workshops on Automated Reasoning: Bridging the Gap between Theory and Practice. Organizing Committee member since 2005.
 WiSETI  "The University of Cambridge Women in Science, Engineering and Technology Initiative". Representative for the Computer Laboratory since 2004.
Conference and Workshop Organization
 Conference Chair. 6th International Conference on the Theory and Application of Diagrams (Diagrams 2010).
 Organizer. PhD Programme at Conferences on Intelligent Computer Mathematics (CICM 2008: MKM + AISC + Calculemus).
 Organizer. Careers workshop "Women in Computing Research" at the 2005 International Joint Conference on Artificial Intelligence (IJCAI 2005).
 Local Chair. 3rd International Conference on the Theory and Application of Diagrams (Diagrams 2004).
 Workshop and Tutorial Chair. 18th Conference on Automated Deduction (CADE18), part of Federated Logic Conference (FLOC 2002).
 Organizer. Symposium on Diagrammatic Reasoning, Automated Reasoning Workshop at the Conference on Artificial Intelligence and the Simulation of Behaviour (AISB 1999).
Membership of International Programme Committees
 11th International Conference on Mathematical Knowledge Management, Intelligent Computer Mathematics (CICM 2012).
 6th International Conference on the Theory and Application of Diagrams (Diagrams 2012).
 3rd International Workshop on Euler Diagrams (ED 2012).
 1st International Workshop on Similarity and Analogybased Methods in AI (SAMAI 2012).
 Visual Representations and Reasoning Workshop at 24th AAAI Conference (AAAI 2010).
 9th International Conference on Mathematical Knowledge Management (MKM 2010).
 6th International Conference on the Theory and Application of Diagrams (Diagrams 2010).
 8th International Conference on Mathematical Knowledge Management (MKM 2009).
 Workshop on Visual Languages and Logic 2009 (VLL 2009).
 7th International Conference on Mathematical Knowledge Management (MKM 2008).
 5th International Conference on the Theory and Application of Diagrams (Diagrams 2008).
 Workshop on Visual languages and Logic 2007 at the 23rd IEEE Symposium on Visual Languages and HumanCentric Computing (VL/HCC'07).
 6th International Conference on Mathematical Knowledge Management (MKM 2007).
 4th International Conference on the Theory and Application of Diagrams (Diagrams 2006).
 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2005).
 3rd International Conference on the Theory and Application of Diagrams (Diagrams 2004).
 9th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2002).
 1st European Workshop on Diagrammatics and Design 2002.
 18th Conference on Automated Deduction (CADE18), part of Federated Logic Conference (FLOC 2002).
 International Joint Conference on Automated Reasoning (IJCAR 2001) Workshop on Future Directions in Automated Reasoning.
 1st International Conference on the Theory and Application of Diagrams (Diagrams 2000).