Edinburgh Research Explorer

Using Animation in Diagrammatic Theorem Proving

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

http://www.inf.ed.ac.uk/publications/report/0331.html
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
Pages46-60
Number of pages15
ISBN (Electronic)978-3-540-46037-4
ISBN (Print)978-3-540-43561-7, 3-540-43561-1
DOIs
StatePublished - 2004

Publication series

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

Abstract

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.

Download statistics

No data available

ID: 403737