Skip to content

Dr Gem Stapleton

Reader

contact:
Computing, Engineering and Mathematics
Moulsecoomb
Brighton
BN2 4GJ

Telephone: +44 (0)1273 642410

Email: G.E.Stapleton@brighton.ac.uk

This web page contains the following information about my research and teaching:

PhD Studentship

Are you interested in studying for a PhD with me? Currently, there is a studentship advertised in the area of information visualization, focusing on automated diagram drawing. This project will extend my research on Euler diagram drawing to include the layout of graphs. Full details on the project, including the application process, can be found here. If you are considering applying then please email me to discuss this project and your application. The deadline for applications is June 8, 2012.

This PhD position has now been filled. However, there are lots of other possible projects in any of the areas in which I conduct research. You are welcome to email me if you would like to discuss the possibilities.

Research Interests

I am a member of the Visual Modelling Group at Brighton. My research interests are in the field of visual languages. Specifically, I am interested in establishing important properties of diagrammatic logics, such as their expressiveness, decidability and completeness. I have also conducted research on automated theorem proving using diagrams, for which I was awarded Best Paper at Diagrams 2004 (with Flower and Masthoff).Recently, my research has considered how one might model ontologies using diagrammatic logics.

A major theme of my work has been to develop the theoretical underpinnings for automated Euler diagram drawing methods. The latest version of the software for drawing Euler diagrams with circles can be freely downloaded from here, with other drawing software and information available from www.eulerdiagrams.com . If you make use of the software please consider citing the associated papers.

You can see my Google Scholar page here.

Funded Research Projects

  • Sketching Euler Diagrams. I am Principal Investigator on this EPSRC funded project, which ran from 2010 until 2011. It devised the first sketch recognition tools for Euler diagrams, and is collaborative with Dr Beryl Plimmer (University of Auckland), Nokia Research (Helsinki), and Dr Peter Rodgers (University of Kent); Aidan Delaney is a Co-Investigator at Brighton. At present, the sketching tools are being extended to spider diagrams.
  • Defining Regular Languages with Diagrams. This EPSRC funded project, on which I was the Principal Investigator, ran from 2010 to 2011. The research produced pushed forward the boundaries of what could be expressed diagrammatically, by developing diagrammatic logics with the expressiveness of (at least) monadic second-order logic over an ordered universe. This project employed Dr Peter Chapman as the RA.
  • Visualisation with Euler diagrams. I was a Co-Investigator on this EPSRC funded project, which ran jointly with the University of Kent from January 2007 until August 2010. The primary goal of this project was to devise methods for automatically drawing Euler diagrams. At Brighton, Prof. John Howse was PI and Dr Andrew Fish was the RA. At Kent, Peter Rodgers was the PI and Dr Leishi Zhang was the RA.
  • The Mathematics of Diagrammatic Logical Systems. From September 2005 until August 2007, I held a Leverhulme Trust Early Career Fellowship. During this Fellowship, I devised automated theorem proving techniques for diagrammatic logics (specifically Euler diagrams), established expressiveness results for diagrammatic logics, and looked at reasoning with such logics.
  • Reasoning with Diagrams. The key goals of this project were to devise diagrammatic logics suitable for specifying, and reasoning about, software models in a formal, yet accessible, manner. The project ran jointly with the University of Kent. At Brighton, Prof. John Howse was PI and Dr John Taylor, Dr Jean Flower and Richard Bosworth were Co-Is, with Dr Andrew Fish employed as the RA. I was an RA on this EPSRC funded project, employed at the University of Kent, working under the direction of Dr Peter Rodgers (PI) and Prof. Simon Thompson (Co-I). Whilst the project ran from 2002 until 2005, I was employed for the final six months only when the original RA left the project. This project was awarded Outstanding overall by the EPSRC.

Awards and Prizes

Roles in the Community

Research Students

  • Mithileysh Sathiyanarayanan. Project: Automatic Visualization of Grouped Networks, starting October 2012.
  • Mohanad Alqadah. Project: Usabilty of Diagrams for Privacy Engineering, starting October 2012.
  • Andrew Blake. Project: Usabilty of Euler Diagrams, started June 2011 (part time).
  • Dr Aidan Delaney. Project: Relationships between Diagrammatic Logics and Formal Language Theory, completed March 2012.
  • Dr Jim Burton. Project: Generalized Constraint Diagram: The Classical Decision Problem in a Diagrammatic Reasoning System, completed May 2010.

Peer Reviewing

I have served on the following Program Committees:

I have also regularly reviewed for the IEEE Symposium on Visual Languages and Human-Centric Computing (2005-2010), as well as for a number of other conferences and journals.

Research Seminars

I have delivered seminars on diagrammatic reasoning and diagram layout at various Universities, including Auckland (NZ), Cambridge (UK), Manchester (UK), Stanford (USA), Monash (Australia), Madrid (Spain) and Jadavpur (India). In addition, I delivered a tutorial on these topics at Nokia Research (Helsinki). The audiences included researchers interested in, for example, AI, automated reasoning, philosophy, and software specification. These seminars explored the evolution of techniques used for formalizing and investigating diagrammatic logics based on Euler diagrams and ended with some discussion on future directions.

Teaching

Over the years I have taught on the mathematics undergraduate courses as well as postgraduate software engineering courses. These days, I mainly teach only computer science undergraduates. In addition, I have delivered postgraduate courses on research methods and project planning to research students across the University.

During 2012/13, I am delivering modules covering topics on:

  • specification and reasoning,

For those with access to studentcentral, my current teaching materials can be found there. In the past, I have taught the following subjects:

  • logic,
  • graph theory,
  • group theory,
  • ring theory,
  • fields,
  • set theory,
  • coding theory,
  • artificial intelligence,
  • foundational mathematics,
  • calculus,
  • statistics,
  • programming,
  • reasoned programming, and
  • research project planning,
  • research methods,
  • object oriented modelling.
Finally, I used to be Course Leader for the University Research Training Framework.

Qualifications

Publications

Many of my publications are available by clicking on the appropriate links below. If you want a copy of a paper that is not downloadable, please feel free to email and ask me for a copy.

Editorial

  1. M. Erwig, G. Stapleton, G. Costagliola (eds). Proceedings of the 2012 IEEE Symposium on Visual Languages and Human-Centric Computing, IEEE, 2012.
  2. G. Stapleton, G Vitiello, M. Sebillo (eds), Special Issue of the Journal of Visual Languages and Computing on Visual Analytics and Visual Semantics, June 2011.
  3. G. Stapleton (ed), Proceedings of Visual Languages and Computing 2009. Knowledge Systems Institute, 2009.
  4. G. Stapleton, J. Howse, and J. Lee (eds), Diagrammatic Representation and Inference: Fifth International Conference, Diagrams 2008, Proceedings. Springer, LNAI 5223, 2008.

Tutorials

  1. J. Howse, G. Stapleton, Formal Visual Modelling. MODELS: ACM/IEEE 14th International Conference on Model Driven Engineering Languages and Systems, Wellington, New Zealand, October 2011. Cancelled due to illness.
  2. J. Howse, P. Rodgers, G. Stapleton, Euler Diagram Drawing for Information Visualization. Diagrams 2010, Portland, Oregon, USA, August, 2010.
  3. J. Howse, P. Rodgers, G. Stapleton, Automated Diagram Drawing . IEEE Symposium on Visual Languages and Human-Centric Computing, Portland, Oregon, USA, IEEE, September, 2009.

Journal Publications

  1. J. Burton, G. Stapleton, J. Howse. Generalized Constraint Diagrams and the Classical Decision Problem. Journal of Logic and Computation, accepted February 2012
  2. G. Stapleton, J. Flower, P. Rodgers, J. Howse. Automatically Drawing Euler Diagrams with Circles. Journal of Visual Languages and Computing, 23(3):163–193, 2012.
  3. G. Stapleton, P. Rodgers, J. Howse A General Method for Drawing Area-Proportional Euler Diagrams. Journal of Visual Languages and Computing, 22(6):426-442, 2011
  4. G. Stapleton, L. Zhang, J. Howse, P. Rodgers. Drawing Euler Diagrams with Circles: The Theory of Piercings, IEEE Transactions on Visualization and Computer Graphics, 17(7):1020-1032, 2011.
  5. J. Burton, G. Stapleton, A. Hamie, A Decision Proceedure for a Decidable Fragment of Generalized Constraint Diagrams. Journal of Visual Languages and Computing, Special Issue on Visual Languages and Logic, 22(1):90-105, 2011.
  6. G. Stapleton, P. Rodgers, J. Howse, L. Zhang. Inductively Generating Euler Diagrams, IEEE Transactions on Visualization and Computer Graphics, 17(1):88-100, 2011.
  7. G. Stapleton, J. Howse, P. Rodgers. A Graph Theoretic Approach to General Euler Diagram Drawing, Theoretical Computer Science, 411(1), 91-112, 2010.
  8. G. Stapleton, J. Taylor, S. Thompson and J. Howse, The Expressiveness of Spider Diagrams Augmented with Constants. Journal of Visual Languages and Computing, 20(1):30-49, 2009.
  9. G. Stapleton and A. Delaney, Evaluating and Generalizing Constraint Diagrams. Journal of Visual Languages and Computing, Special Issue containing extended versions of the Best Papers from VL/HCC 2007, 19(4):499-521, 2008.
  10. G. Stapleton, J Masthoff, J. Flower, A. Fish and J. Southern. Automated Theorem Proving in Euler Diagram Systems. Journal of Automated Reasoning, 39(4):431-470, 2007.
  11. G. Stapleton, J. Howse and J. Taylor. A Decidable Constraint Diagram Reasoning System. Journal of Logic and Computation, 15(6:975-1008, 2005.
  12. J. Howse, G. Stapleton and J. Taylor. Spider Diagrams. LMS Journal of Computation and Mathematics, 8:145-194, 2005.
  13. G. Stapleton, S. Thompson, J. Howse and J. Taylor, The Expressiveness of Spider Diagrams. Journal of Logic and Computation, 14(6:857-880, 2004.

Book Chapters

  1. G. Stapleton, J. Howse, S. Thompson, J. Taylor, P Chapman, On the Completeness of Spider Diagrams Augmented with Constants, Accepted for Visual Reasoning with Diagrams, 2011.

Conference and Workshop Publications

  1. J. Nicholson, A. Delaney, G. Stapleton. Linking Codecharts with Programs. Accepted for Visual Languages and Human-Centric Computing 2012.
  2. A. Blake, G. Stapleton, P. Rodgers, L. Cheek, J. Howse. Does the Orientation of an Euler Diagram Affect User Comprehension? 18th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing, Knowledge Systems Instuite, pages 195-190, 2012. Awarded Best Paper
  3. J. Nicholson, A. Delaney, G. Stapleton. Formalizing the Syntax of Codecharts. Accepted for Visual Languages and Computing 2012.
  4. P. Rodgers, J. Flower, G. Stapleton. Introducing 3D Venn and Euler Diagrams. Euler Diagrams 2012, CEUR Vol 854, pages 92-106, 2012.
  5. J. Burton, G. Stapleton, J. Howse. Completeness Proof Strategies for Euler Diagram Logics. Euler Diagrams 2012, CEUR Vol 854, pages 2-16, 2012
  6. M. Urbas, M. Jamnik, G. Stapleton, J. Flower. Speedith: A Diagrammatic Reasoner for Spider Diagrams. 7th International Conference on the Theory and Application of Diagrams 2012, Springer, pages 163-177, 2012.
  7. J. Burton, G. Stapleton, J. Howse. Completeness Proofs for Diagrammatic Logics. 7th International Conference on the Theory and Application of Diagrams 2012, Springer, pages 318-320, 2012.
  8. G. Stapleton, J. Howse, P. Chapman, I. Oliver, A. Delaney. What can Concept Diagrams Say? Accepted for 7th International Conference on the Theory and Application of Diagrams 2012, Springer, pages 291-293, 2012.
  9. J. Howse, G. Stapleton, K. Taylor, P. Chapman. Visualizing Ontologies: A Case Study. International Semantic Web Conference 2011, Bohn, Germany, Springer, pages 257-272, 2011.
  10. P. Chapman, G. Stapleton, J. Howse, I. Oliver. Deriving Sound Inference Rules for Concept Diagrams. IEEE Symposium on Visual Languages and Human-Centric Computing, Pittsburgh, USA, IEEE, September, pages 87-94, 2011.
  11. M. Wang, B. Plimmer, P. Schmieder, G. Stapleton, P. Rodgers, A. Delaney. SketchSet: Creating Euler Diagrams using Pen or Mouse. IEEE Symposium on Visual Languages and Human-Centric Computing, Pittsburgh, USA, IEEE, September, pages 75-82, 2011.
  12. G. Stapleton, P. Rodgers. Drawing Euler Diagrams with Circles and Ellipses. IEEE Symposium on Visual Languages and Human-Centric Computing, Pittsburgh, USA, IEEE, September, pages 209-212, 2011.
  13. G. Stapleton, A. Delaney, P. Rodgers, B. Plimmer. Recognising Sketches of Euler Diagrams Augmented with Graphs. Visual Languages and Computing, Florence, Italy, Knowledge Systems Institute, September, pages 279-284, 2011.
  14. J. Howse, G. Stapleton, I. Oliver. Visual Reasoning about Ontologies. International Semantic Web Conference, China, November, CEUR volume 658, pages 5-8, 2010.
  15. A. Delaney, B. Plimmer, G. Stapleton, P. Rodgers. Recognising Sketches of Euler Diagrams Drawn with Ellipses. Visual Languages and Computing, USA, Knowledge Systems Institute, September, pages 305-310, 2010.
  16. P. Chapman, G. Stapleton. On the Relative Expressiveness of Second-Order Spider Diagrams and Regular Expressions. Visual Languages and Computing, USA, Knowledge Systems Institute, September, pages 283-288, 2010.
  17. P. Chapman, G. Stapleton. Introducing Second Order Spider Diagrams for Defining Regular Languages. IEEE Symposium on Visual Languages and Human-Centric Computing, Madrid, Spain, pages 159-167, IEEE, September, 2010.
  18. P. Rodgers, G. Stapleton, J. Howse, L. Zhang. Euler Graph Transformations for Euler Diagram Layout. IEEE Symposium on Visual Languages and Human-Centric Computing, Madrid, Spain, pages 111-118 IEEE, September, 2010.
  19. P. Chapman, G. Stapleton, Creating a Second Order Diagrammatic Logic 6th International Conference on the Theory and Application of Diagrams 2010, Portland, USA, pages 298-300, Springer, August, 2010.
  20. G. Stapleton, L. Zhang, J. Howse, P. Rodgers, Drawing Euler Diagrams with Circles 6th International Conference on the Theory and Application of Diagrams 2010, Portland, USA, pages 23-38, Springer, August, 2010.
  21. A. Delaney, G. Stapleton, J. Taylor, S. Thompson, Fragments of Spider Diagrams of Order and their Relative Expressiveness 6th International Conference on the Theory and Application of Diagrams 2010, Portland, USA, pages 69-83, Springer, August, 2010.
  22. P. Rodgers, J. Flower, G. Stapleton, J. Howse, Drawing Area-Proportional Venn-3 Diagrams with Convex Curves In proceedings of Diagrams 2010, Portland, USA, pages 54-68 Springer, August, 2010.
  23. J. Howse, P. Rodgers, G. Stapleton. Levels of Syntax in Euler Diagram Logics. World Congress and Summer School on Universal Logic, Special Session on Logic Diagrams, 2010
  24. I. Oliver, J. Howse, G. Stapleton, E. Nuutila, S. Torma. Visualising and Specifying Ontologies using Diagrammatic Logics. In proceedings of 5th Australasian Ontologies Workshop, Melboune, Australia, CRPIT vol. 112, December, pages 37-47, 2009. Awarded Best Paper
  25. J. Howse, S. Schuman, G. Stapleton, I. Oliver. Diagrammatic Formal Specification of a Configuration Control Platform. 2009 Refinement Workshop, pages 87-104, ENTCS, November, 2009.
  26. I. Oliver, J. Howse, G. Stapleton, E. Nuutila, S. Torma. A Proposed Diagrammatic Logic for Ontology Specification and Visualization. 8th International Semantic Web Conference (Posters and Demos), October, 2009.
  27. J. Burton, G. Stapleton, A. Hamie. Transforming Constraint Diagrams. In proceedings of Visual Languages and Logic, Corvallis, USA, pages 62-80, CEUR Series vol. 510, September, 2009.
  28. J. Howse, P. Rodgers, G. Stapleton. Changing Euler Diagram Properties by Edge Transformation of Euler Dual Graph. In proceedings of IEEE Symposium on Visual Languages and Human-Centric Computing, Oregon, USA, pages 177-184, IEEE, September, 2009.
  29. P. Rodgers, J. Flower, G. Stapleton, J. Howse, Some Results for Drawing Area Proportional Venn3 with Convex Curves. In proceedings of Information Visualization, Barcelona, IEEE, pages 667-672, July, 2009.
  30. G. Stapleton, M. Jamnik, and J. Masthoff, On the Readability of Diagrammatic Proofs. Proceedings of Automated Reasoning Workshop, pages 37-38, April, 2009.
  31. G. Stapleton, J. Howse, P. Rodgers, and L. Zhang, Generating Euler Diagrams from Existing Layouts. In Proceedings of Layout of (Software) Engineering Diagrams, Herrsching, pages 16-31, ECEASST vol 13, September, 2008.
  32. G. Stapleton, A. Fish and P. Rodgers. Abstract Euler Diagram Isomorphism. In Proceedings of 14th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, Boston, USA, pages 310-317, Knowledge Systems Institute, September, 2008.
  33. G. Stapleton. Spider Diagrams Augmented with Constants: A Complete System. In Proceedings of 14th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, Boston, USA, pages 292-299, Knowledge Systems Institute, September, 2008.
  34. J. Howse, and G. Stapleton. Visual Mathematics: Diagrammatic Formalization and Proof. Proceedings of International Conference on Mathematical Knowledge Management, Birmingham, UK, pages 478-493, Springer, July, 2008.
  35. P. Rodgers, L. Zhang, G. Stapleton, and A. Fish, Embedding Wellformed Euler Diagrams. Proceedings of Information Visualization, London, UK, pages 585-593, IEEE, July, 2008.
  36. G. Stapleton, P. Rodgers, J. Howse and J. Taylor, Properties of Euler Diagrams. Proceedings of Layout of Software Engineering Diagrams, Coeur d'Alene, Idaho, USA, pages 2-16, ECEASST vol 7, September, 2007.
  37. A. Delaney and G. Stapleton, Spider Diagrams of Order. In proceedings of Visual Languages and Logic, Coeur d'Alene, Idaho, USA, pages 27-39, CEUR Series vol. 274, September, 2007.
  38. G. Stapleton and A. Delaney, Towards Overcoming Decificiences in Constraint Diagrams. Proceedings of IEEE Symposium on Visual Languages and Human-Centric Computing, Coeur d'Alene, Idaho, USA, pages 33-40, IEEE, September, 2007.
  39. A. Delaney and G. Stapleton, On the Descriptional Complexity of a Diagrammatic Notation. In Proceedings of 13th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, San Francisco, USA, pages 195-202, Knowledge Systems Institute, 2007.
  40. G. Stapleton and J. Masthoff, Incorporating Negation into Visual Logics: A Case Study Using Euler Diagrams. In Proceedings of 13th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, San Francisco, USA, pages 187-194, Knowledge Systems Institute, 2007.
  41. G. Stapleton, Diagrammatic Logics: Past, Present and Future. Invited contribution to the International Conference on Logic, Navya Nyaya and Applications: A Homage to Bimal Krishna Mitilal, Calcutta, India, pages 4-15, January, 2007.
  42. G. Stapleton and J. Howse, Enhancing the Expressiveness of Spider Diagram Systems. In Proceedings of 12th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, Grand Canyon, USA, pages 129-138, Knowledge Systems Institute, 2006.
  43. A. Fish and G. Stapleton, Formal Issues in Languages Based on Closed Curves In Proceedings of 12th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, Grand Canyon, USA, pages 161-167, Knowledge Systems Institute, 2006.
  44. G. Stapleton, J. Howse and K. Toller, Generalizing Spiders. In proceedings of 4th International Conference, Diagrams 2006, Stanford, USA, pages 148-150, Springer-Verlag, June, 2006.
  45. A. Fish and G. Stapleton, Defining Euler Diagrams: Simple or What? In proceedings of 4th International Conference, Diagrams 2006, Stanford, USA, pages 109-111, Springer-Verlag, June, 2006.
  46. G. Stapleton, S. Thompson, A. Fish, J. Howse and J. Taylor, A New Language for the Visualization of Logic and Reasoning,  In proceedings of 11th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, Banff, Canada, pages 287-292, Knowledge Systems Institute, 2005.
  47. G. Stapleton, J. Howse and K. Toller, On Spiders’ Feet. Extended abstract in proceedings of 2nd International Workshop on Euler Diagrams, Paris, September 2005.
  48. A. Fish and G. Stapleton, Defining Euler Diagrams: Choices and Consequences. Extended abstract in proceedings of 2nd International Workshop on Euler Diagrams, Paris, September 2005.
  49. G. Stapleton, A Survey of Reasoning Systems Based on Euler Diagrams. Euler Diagrams 2004, Brighton, UK, September, 2004, ENTCS, 134, pages 127-151, Elsevier Science, 2005.
  50. J. Flower, J. Masthoff and G. Stapleton, Generating Proofs with Spider Diagrams Using Heuristics. In proceedings of 10th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, San Francisco, USA, pages 279-285, Knowledge Systems Institute, September, 2004.
  51. G. Stapleton, J. Howse, J. Taylor and S. Thompson, The Expressiveness of Spider Diagrams Augmented with Constants.In proceedings of IEEE Symposium on Visual Languages and Human-Centric Computing, Rome, Italy, pages 91-98, IEEE, September, 2004.
  52. G. Stapleton, J. Howse, J. Taylor and S. Thompson, What Can Spider Diagrams Say? In proceedings of 3rd International Conference, Diagrams 2004, Cambridge, UK, pages 112-127, Springer-Verlag, March, 2004.
  53. J. Flower, J. Masthoff and G. Stapleton, Generating Readable Proofs: A Heuristic Approach to Theorem Proving with Spider Diagrams. In proceedings of 3rd International Conference, Diagrams 2004, Cambridge, UK, pages 166-181, Springer-Verlag, March, 2004. Awarded Best Paper.
  54. J. Flower and G. Stapleton, Automated Theorem Proving with Spider Diagrams. In proceedings of Computing: The Australasian Theory Symposium 2004, Dunedin, New Zealand, pages 116-132, ENTCS, Elsevier Science, 2004.
  55. G. Stapleton, J. Howse and J. Taylor, A Constraint Diagram Reasoning System.In proceedings of 9th International Conference on Distributed Multimedia Systems, Visual Languages and Computing, Florida, USA, pages 263-270, Knowledge Systems Institute, September, 2003.
  56. J. Howse, G. Stapleton, J. Flower and J. Taylor, Corresponding Regions in Euler Diagrams In proceedings of Diagrams 2002, Georgia, USA, pages 76-90, Springer-Verlag, April 2002.

Technical Reports

  1. G. Stapleton, How to Use Edith: The Euler Diagram Theorem Prover, 2007.
  2. G. Stapleton, Euler Diagram Reasoning, 2007.
  3. J. Howse, R. Bosworth, A. Fish, G. Stapleton, J. Taylor, P. Rodgers and S. Thompson, Euler Diagram Based Notations, 2006.
  4. G. Stapleton, J. Masthoff, J. Flower, A. Fish and J. Southern, Appendices for Automated Theorem Proving in Euler Diagram Systems, 2006.
  5. G. Stapleton, Reasoning with Constraint Diagrams: 20 Page summary of PhD Thesis, 2004.

Other

  1. G. Stapleton, Visualizing Information using Extended Euler Diagrams, presented at a BBSRC/AHRC Workshop on the Challenges of Visualizing Biological Data, 2010.
  2. G. Stapleton, Final Report Summary: The Mathematics of Diagrammatic Logical Systems, 2007.
  3. G. Stapleton, Reasoning with Constraint Diagrams, PhD Thesis, Published by the British Computer Society, 2005.
  4. J. Howse, R. Bosworth, A. Fish. J. Taylor, P. Rodgers, G. Stapleton and S. Thompson, Reasoning with Diagrams: Final Report, 2005.