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

    I am looking into combining diagrammatic reasoning with existing symbolic reasoning techniques, like different types of logic, and formalise this so-called 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.

    Here is the project proposal.


  • 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" (1995-1998).

    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 so-called "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).











  • Women and Computing Research
    Women@CL

    I direct women@CL national network (co-founded 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 start-ups. 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 ". (1998-2002)
    • Staff member on EU 5th Framework Grant "Calculemus: System for Integrated Computation and Deduction". (2000-2004)

    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.


  • Agent-Oriented Theorem Proving

    • Research fellow on EPSRC Standard Research Grant "Agent-Oriented Theorem Proving". (2000-2001)

    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.


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


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 (CADE-18), 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 Analogy-based 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 Human-Centric 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 (CADE-18), 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).