Using Animation in Diagrammatic Theorem Proving

Alan Bundy, C. Gurr, M. Jamnik, Daniel Winterstein

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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. Com- puters 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 di- agrams, and also how it can deal with the more complex questions of quantification and generalisation in diagrams that use more specific rep- resentations. This allows us to tackle difficult theorems that previously could only be proved algebraically.
Original languageEnglish
Title of host publicationProceedings for Diagrammatic Representation and Inference, 2nd International Conference, Diagrams 2002
Subtitle of host publicationSecond International Conference, Diagrams 2002 Callaway Gardens, GA, USA, April 18–20, 2002 Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-540-46037-4
ISBN (Print)978-3-540-43561-7, 3-540-43561-1
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Using Animation in Diagrammatic Theorem Proving'. Together they form a unique fingerprint.

Cite this