research

Logical Forms in Wit
Daniel Winterstein & Sebastian Mhatre

This paper presents a preliminary theory for the logical structure underlying a certain class of jokes and witty comments. We show that there is a range of jokes which can be understood as intentionally poor speech acts (where the intention is conveyed by a variety of means, including nonsense, parody and self-reference). Constructing such utterances typically requires intelligence and creativity. Hence jokes may have evolved (via mate-selection forces) as a way of demonstrating mental fitness.

The goal of this work is both improving our understanding of humour (via formal theories of jokes), and techniques for the computer recognition and generation of jokes. It therefore focuses on structures that require relatively little world-knowledge. An analysis of several kinds of joke, preliminary to the definition of algorithms for joke generation, is proposed. We identify logical forms that give rise to these jokes, and show how these forms correspond to violations of `the rules of good speech' (e.g. Grice's Maxims). The suggested algorithms have yet to be implemented and tested. Hopefully though, they will extend computer-generation to a wider range of jokes.

A Cooperative Game for Designing/Evolving Visual Languages

This paper presents a method for developing specialised visual languages, based on the parlour game \textit{Pictorial Chinese Whispers}. This is a game which naturally leads to the invention of new representational devices. We adapt it to give a language design game. When played repeatedly, an increasingly sophisticated and reliable representation scheme evolves. The proposed method has several advantages over conventional design methodology (although we also describe some drawbacks). The process is flexible and encourages creative exploration. The work is shared amongst a group, requires no training, and the game aspect makes it enjoyable. There is also an inherent element of empirical testing, so that flaws in the language are exposed. It could therefore be particularly useful for groups without the experience or desire to engage in a conventional design process.
Unpublished, 2005

Ph.D. Thesis: Diagrammatic Reasoning in a Continuous Domain

This project looks at using diagrammatic reasoning to prove mathematical theorems. The work is motivated by a need for theorem provers whose reasoning is readily intelligible to human beings. It should also have practical applications in mathematics teaching.

We focus on the continuous domain of analysis - a geometric subject, but one which is taught using a dry algebraic formalism which many students find hard. The geometric nature of the domain makes it suitable for a diagram-based approach. However it is a difficult domain, and there are several problems, including handling alternating quantifiers, sequences and generalisation. We developed representations and reasoning methods to solve these. Our diagram logic isn't complete, but does cover a reasonable range of theorems. It utilises computers to extend diagrammatic reasoning in new directions including using animation.

This work is tested for soundness, and evaluated empirically for ease of use. We demonstrate that computerised diagrammatic theorem proving is not only possible in the domain of real analysis, but that students perform better using it than with an equivalent algebraic computer system.



Dr.Doodle: A Diagrammatic Theorem Prover
Daniel Winterstein, Alan Bundy & Corin Gurr

This paper presents the Dr.Doodle system, an interactive theorem prover that uses diagrammatic representations. The assumption underlying this project is that, for some domains, diagrammatic reasoning is easier to understand than conventional algebraic approaches - at least for a significant number of people. The Dr.Doodle system was developed for the domain of metric-space analysis (a geometric domain, but traditionally taught using a dry algebraic formalism). Pilot experiments were conducted to evaluate its potential as the basis of an educational tool, with encouraging results.
Published: IJCAR 2004

An Experimental Comparison of Diagrammatic and Algebraic Logics
Daniel Winterstein, Alan Bundy, Corin Gurr & Mateja Jamnik

We have developed a diagrammatic logic for theorem proving, focusing on the domain of metric-space analysis (a geometric domain, but traditionally taught using a dry algebraic formalism). To evaluate its pragmatic value, pilot experiments were conducted using this logic - implemented in an interactive theorem prover - to teach undergraduate students (and comparing performance against an equivalent algebraic logic). Our results show significantly better performance for students using diagrammatic reasoning. We conclude that diagrams are a useful tool for reasoning in such domains.
Published: Diagrams 2004

On Differences Between the Real and Physical Plane
Daniel Winterstein, Alan Bundy, Corin Gurr & Mateja Jamnik

When formalising diagrammatic systems, it is quite common to situate diagrams in the real plane, R2. However this is not necessarily sound unless the link between formal and physical diagrams is examined. We explore some issues relating to this, and potential mistakes that can arise. This demonstrates that the effects of drawing resolution and the limits of perception can change the meaning of a diagram in surprising ways. These effects should therefore be taken into account when giving formalisations based on R2.
Published: Diagrams 2004

Technical Appendix containing various proofs.



Ph.D. research proposal

The aim of this project is to investigate the potential for applying a diagrammatic approach to automated reasoning. It focuses on the domain of mathematical analysis - a geometric subject, usually taught in a purely algebraic way. This is motivated by the aim of producing theorem provers whose proofs can be understood by people. The techniques developed should also have a practical application in mathematics teaching, where hopefully they will complement conventional methods. Such work also furthers understanding of the mathematical nature of diagrams.

Using Animation in Diagrammatic Theorem Proving
Daniel Winterstein, Alan Bundy, Corin Gurr & Mateja Jamnik

Diagrams have many uses in mathematics, one of the most ambitious of which is as a form of proof. The domain we consider is real analysis, where quantification issues are subtle but crucial. Computers offer new possibilities in diagrammatic reasoning, one of which is animation. Here we develop animated rules as a solution to problems of quantification. We show a simple application of this to constraint diagrams, and also how it can deal with the more complex questions of quantification and generalisation in diagrams that use more specific representations. This allows us to tackle difficult theorems that previously could only be proved algebraically.
Published: Diagrams 2002

Developing a Diagrammatic Logic

In my research proposal I demonstrate a diagram based logic for proving theorems in real analysis. Here I present a framework for its formalisation. This note should be read as an extension to my research proposal, which provides motivation, examples of the reasoning in question and an analysis of that reasoning. The reasoning developed is genuinely diagrammatic, and this raises new problems. The result is a logic which is structurally as well as visually different.
NB - This paper is fairly unreadable.

Evaluating Machine Creativity
Alison Pease, Daniel Winterstein & Simon Colton



Diagrammatic Reasoning in a Continuous Domain

This project investigates the formalisation of diagrammatic proofs in a continuous domain.

The aim is to develop a set of diagrams and reasoning rules to allow the mechanised construction of sequences of diagrams constituting a proof. The idea is that one sequence of diagrams can be used to prove many instances of a theorem. The project explores ways for creating a diagrammatic logic to do this.

The reasoning method used is that of production rules. The rules have visual pre- and post- conditions, allowing them to also be expressed diagrammatically. They act by redrawing the working diagram, hence we call them 'redraw rules'. A prototype system is implemented to test the theory.

The domain considered is real analysis - a geometric subject, but one whose dry algebraic formalism is often off-putting to students.



A Proposal for Automating Diagrammatic Reasoning in Continuous Domains
Daniel Winterstein, Alan Bundy & Mateja Jamnik

This paper presents one approach to the formalisation of diagrammatic proofs as an alternative to algebraic logic. An idea of `generic diagrams' is developed whereby one diagram (or rather, one sequence of diagrams) can be used to prove many instances of a theorem. This allows the extension of Jamnik's ideas in the Diamond system to continuous domains.

The domain is restricted to non-recursive proofs in real analysis whose statement and proof have a strong geometric component. The aim is to develop a system of diagrams and redraw rules to allow a mechanised construction of sequences of diagrams constituting a proof. This approach involves creating a diagrammatic theory. The method is justified formally by (a) a diagrammatic axiomatisation, and (b) an appeal to analysis, viewing the diagram as an object in R2. The idea is to then establish an isomorphism between diagrams acted on by redraw rules and instances of a theorem acted on by rewrite rules.

We aim to implement these ideas in an interactive prover entitled Rap (the Real Analysis Prover).
Published: Diagrams 2000