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. 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.
This would probably not be suitable for domains which involve precise time calculations, as these would be hard to judge in an animation. For qualitative reasoning though, or as part of a mixed system, it seems an interesting line for future research.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Barwise & J. Etchemendy “Heterogeneous Logic” in Diagrammatic Reasoning: Cognitive and Computational Perspectives. AAAI Press/The MIT Press, 1995.
A. Bierce “Fantastic Fables: The Flying Machine” 1899. Project Gutenberg e-text 1995, ftp://ftp.ibiblio.org/pub/docs/books/gutenberg/etext95/fanfb10.txt
J. Howse, F. Molina & J. Taylor “On the Completeness and Expressiveness of Spider Diagram Systems” proceedings of the 1st International Conference on Theory and Application of Diagrams. pp26–41, Springer-Verlag, 2000.
B. Fraser “Structuralism” course notes, Cambridge University. Available online at http://www.classics.cam.ac.uk/Faculty/structuralism.html, 1999.
J. Gil, J. Howse & S. Kent “Towards a Formalization of Constraint Diagrams” Symposium on Visual Languages and Formal Methods. IEEE, 2001.
J. Gil & Y. Sorkin “The Constraint Diagrams Editor” Available online at http://www.cs.technion.ac.il/Labs/ssdl/research/cdeditor, 1999-2000.
C. Gurr, J. Lee & K. Stenning “Theories of Diagrammatic Reasoning: Distinguishing Component Problems” in Minds & Machines 8(4) pp533–557, Kluwer Academic, 1998.
E. Hammer “Reasoning with Sentences and Diagrams” in “Working Papers on Diagrams and Logic” editors G. Allwein & J. Barwise, Indiana University Logic Group, 1993.
P.J. Hayes & G.L. Laforte “Diagrammatic Reasoning:Analysis of an Example” in “Formalizing Reasoning with Visual and Diagrammatic representations: Papers from the 1998 AAAI Fall Symposium” editors G. Allwein, K. Marriott & B. Meyer, 1998.
G. Klima “Existence and Reference in Medieval Logic” in “New Essays in Free Logic” editors A. Hieke & E. Morscher, Kluwer Academic, 2001.
T.W. Körner “Analysis” lecture notes, Cambridge University. Available online at http://ftp.dpmms.cam.ac.uk/pub/twk/Anal.ps, 1998.
L.K. Schubert “Extending the Expressive Power of Semantic Networks” in Artificial Intelligence. 7(2) pp163–198, Elsevier, 1976.
A. Sloman “Interactions Between Philosophy and A.I.: The Role of Intuition and Non-Logical Reasoning in Intelligence” proceedings 2nd International Joint Conference on Artificial Intelligence, 1971.
D. Winterstein “Diagrammatic Reasoning in a Continuous Domain” CISA Ph.D. Research Proposal, Edinburgh University. Available online at http://www.dai.ed.ac.uk/homes/danielw/academic, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Winterstein, D., Bundy, A., Gurr, C., Jamnik, M. (2002). Using Animation in Diagrammatic Theorem Proving. In: Hegarty, M., Meyer, B., Narayanan, N.H. (eds) Diagrammatic Representation and Inference. Diagrams 2002. Lecture Notes in Computer Science(), vol 2317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46037-3_5
Download citation
DOI: https://doi.org/10.1007/3-540-46037-3_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43561-7
Online ISBN: 978-3-540-46037-4
eBook Packages: Springer Book Archive