Abstract
This chapter describes our research into the way in which diagrams convey mathematical meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried to discover how a diagram can convey the meaning of a proof. &/GROVER is a theorem-proving system that interprets diagrams as proof strategies. The diagrams are similar to those that a mathematician would draw informally when communicating the ideas of a proof. We have applied &/GROVER to obtain automatic proofs of three theorems that are beyond the reach of existing theorem-proving systems operating without such guidance. In the process, we have discovered some patterns in the way diagrams are used to convey mathematical reasoning strategies. Those patterns, and the ways in which &/GROVER takes advantage of them to prove theorems, are the focus of this chapter.
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.
Similar content being viewed by others
References
Barker-Plummer, D. and Bailin, S.C. (1992). Proofs and pictures: Proving the diamond lemma with the GROVER theorem proving system. In Working notes of the AAAI symposium on reasoning with diagrammatic representations, Stanford, CA, 25–27 March.
Barker-Plummer, D. and Bailin, S.C. (1997). The role of diagrams in mathematical proofs. Machine Graphics and Vision 6(1):25–56.
Barwise, J. (1993). Heterogeneous reasoning. In G. Allwein and J. Barwise (Eds), Working papers on diagrams and logic. Indiana University Logic Group, pp. 1–13.
Gelernter, H. (1963). Realization of a geometry theorem proving machine. In E. Feigenbaum and J. Feldman (Eds), Computers and thought. New York: McGraw Hill.
Gelernter, H., Hansen, J.R. and Loveland, D.W. (1963). Empirical explorations of the geometry theorem proving machine. In E. Feigenbaum and J. Feldman (Eds), Computers and thought. New York: McGraw Hill.
Gilmore, P. (1970). An examination of the geometry theorem proving machine. Artificial Intelligence 1:171–187.
Jamnik, M., Bundy, A. and Green, I. (1997). Automation of diagrammatic proofs in mathematics. In B. Kokinov (Ed.), Perspectives on cognitive science, Vol. 3. Sofia: NBU Press, pp. 168–175. Also available as Department of Artificial Intelligence Research Paper No. 835.
Jamnik, M., Bundy, A. and Green, I. (1999). On automating diagrammatic proofs of arithmetic arguments. Journal of Logic, Language and Information 8(3):297–321. Also available as Department of Artificial Intelligence Research Paper No. 910.
Nelson, R.B. (1993). Proofs without words. Number 1 in Classroom Resource Materials. Washington, DC: The Mathematical Association of America.
Pastre, D. (1977). Automatic theorem proving in set theory. Technical report, University of Paris (VI).
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag London
About this chapter
Cite this chapter
Barker-Plummer, D., Bailin, S.C. (2002). On the Practical Semantics of Mathematical Diagrams. In: Anderson, M., Meyer, B., Olivier, P. (eds) Diagrammatic Representation and Reasoning. Springer, London. https://doi.org/10.1007/978-1-4471-0109-3_19
Download citation
DOI: https://doi.org/10.1007/978-1-4471-0109-3_19
Publisher Name: Springer, London
Print ISBN: 978-1-85233-242-6
Online ISBN: 978-1-4471-0109-3
eBook Packages: Springer Book Archive