Intuitive and Formal Representations: The Case of Matrices

A major obstacle for bridging the gap between textbook mathematics and formalising it on a computer is the problem how to adequately capture the intuition inherent in the mathematical notation when formalising mathematical concepts. While logic is an excellent tool to represent certain mathematical concepts it often fails to retain all the information implicitly given in the representation of some mathematical objects. In this paper we concern ourselves with matrices, whose representation can be particularly rich in implicit information. We analyse different types of matrices and present a mechanism that can represent them very close to their textbook style appearance and captures the information contained in this representation but that nevertheless allows for their compilation into a formal logical framework. This firstly allows for a more human-oriented interface and secondly enables efficient reasoning with matrices.

• Type: Conference
• Year: 2004
• Where: MKM
• Authors: Martin Pollet, Volker Sorge, Manfred Kerber
• Keywords: Certain Mathematical Concepts, Mathematical Concepts, Mathematical Notation, MKM 2004