- 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.
- Links To Paper
- 1st Link
- Bibtex format
- @Misc{EDI-INF-RR-0331,
- author = {
Daniel Winterstein
and Alan Bundy
and Corin Gurr
and Mateja Jamnik
},
- title = {Using Animation in Diagrammatic Theorem Proving},
- year = 2002,
- url = {http://bigred.homelinux.org/~danielw/academic/diagrams2002.ps.gz},
- }
|
