Visual Mathematics: Diagrammatic Formalization and Proof Export

@incollection{citeulike:3273918, abstract = {Diagrams have been used for centuries in the visualization of mathematical concepts and to aid the exploration and formalization of ideas. This is hardly surprising given the intuitive appeal of visual languages. Thus it seems very natural to establish how diagrams can play an integral part of mathematical formalization and reasoning, giving them the same status as the symbolic languages that they are used alongside. Indeed, recently we have seen the emergence of diagrammatic reasoning systems that are defined with sufficient mathematical rigour to allow them to be used as formal tools in their own right. Some of these systems have been designed with particular application areas in mind, such as number theory and real analysis, or formal logics. This paper focuses on the use of diagrammatic logics to formalize mathematical theories with the same level of rigour that is present in their corresponding predicate logic axiomatizations. In particular, extensions to the constraint diagram logic are proposed to make it more suitable for use in mathematics. This extended logic is illustrated via the diagrammatic formalization of some commonly occurring mathematical concepts. Subsequently, we demonstrate its use in the proofs of some simple theorems.}, author = {Howse, John and Stapleton, Gem}, citeulike-article-id = {3273918}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-85110-3_39}, doi = {10.1007/978-3-540-85110-3_39}, journal = {Intelligent Computer Mathematics}, keywords = {diagrams, for\_gabe}, pages = {478--493}, posted-at = {2008-09-16 17:29:22}, priority = {0}, title = {Visual Mathematics: Diagrammatic Formalization and Proof}, url = {http://dx.doi.org/10.1007/978-3-540-85110-3_39}, year = {2008} }

TY - CHAP ID - citeulike:3273918 L3 - citeulike-article-id:3273918 N2 - Diagrams have been used for centuries in the visualization of mathematical concepts and to aid the exploration and formalization of ideas. This is hardly surprising given the intuitive appeal of visual languages. Thus it seems very natural to establish how diagrams can play an integral part of mathematical formalization and reasoning, giving them the same status as the symbolic languages that they are used alongside. Indeed, recently we have seen the emergence of diagrammatic reasoning systems that are defined with sufficient mathematical rigour to allow them to be used as formal tools in their own right. Some of these systems have been designed with particular application areas in mind, such as number theory and real analysis, or formal logics. This paper focuses on the use of diagrammatic logics to formalize mathematical theories with the same level of rigour that is present in their corresponding predicate logic axiomatizations. In particular, extensions to the constraint diagram logic are proposed to make it more suitable for use in mathematics. This extended logic is illustrated via the diagrammatic formalization of some commonly occurring mathematical concepts. Subsequently, we demonstrate its use in the proofs of some simple theorems. JF - Intelligent Computer Mathematics EP - 493 TI - Visual Mathematics: Diagrammatic Formalization and Proof SP - 478 KW - diagrams KW - for_gabe AU - Howse, John AU - Stapleton, Gem PY - 2008/// UR - http://dx.doi.org/10.1007/978-3-540-85110-3_39 ER -