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.

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.

**Technical Appendix** containing various proofs.

NB - This paper is fairly unreadable.

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.

`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
R^{2}. 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*