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.
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