Computerizing mathematical text, debugging proof assistants and object versus metal level
Fairouz Kamareddine
Heriot-Watt University, UK
: J Comput Eng Inf Technol
Abstract
Mathematical texts can be computerized in many ways that capture differing amounts of the mathematical meaning. At one end, there is document imaging, which captures the arrangement of black marks on paper, while at the other end there are proof assistants (e.g., Mizar, Isabelle, Coq, etc.), which capture the full mathematical meaning and have proofs expressed in a formal foundation of mathematics. In between, there are computer type setting systems (e.g., LATEX and presentation MathML) and semantically oriented systems (e.g., Content MathML, OpenMath, OMDoc, etc.). In this talk, we advocate a style of computerization of mathematical texts which is flexible enough to connect the different approaches to computerization, which allows various degrees of formalization, and which is compatible with different logical frameworks (e.g., set theory, category theory, type theory, etc.) and proof systems. The basic idea is to allow a man-machine collaboration which weaves human input with machine computation at every step in the way. We propose that the huge step from informal mathematics to fully formalized mathematics be divided into smaller steps, each of which is a fully developed method in which human input is minimal. We also propose a method based on constraint generation and solving to debug proof assistants written in SML and reflect on the need and limitation of mixing the object and meta-level.
Biography
Fairouz Kamareddine has been involved in a number of worldwide consultancy assignments, especially on education and research issues working for United Nations and the EU. Her research interest includes Interface of Mathematics, Logic and Computer Science. She has held numerous invited positions at universities worldwide. She has well over 100 published articles and a number of books. She has played leading roles in the development, administration and implementation of interdisciplinary, international, and academic collaborations and networks.
