Ontario Research Centre for Computer Algebra

Conferences on Intelligent Computer Mathematics

CICM 2009

Grand Bend, Ontario (CANADA), 5-12 July 2009

Invited Speakers

Computational Logic and Continuous Mathematics, Pure and Applied

Rob Arthan
Lemma 1 Ltd. & Queen Mary, University of London (UK)

Continuous problem domains are of ever-increasing importance in the application of computational logic to problems in systems engineering and to problems in mathematics and theoretical computer science. I will outline some recent work both "pure" and "applied" with issues for mechanized reasoning and computer algebra in mind.

Math-Literate Computers

Dorothea Blostein
School of Computing, Queen's University (Canada)

Math notation is a familiar, everyday tool widely used in society. Computers need math literacy -- the ability to read and write math notation -- in order to assist people with accessing mathematical documents and carrying out mathematical investigations. In this paper, we assess the state of the art, and discuss issues in making computers math-literate. Software for generating math notation is widely used. Software for recognition of math notation is not as widely used: to avoid the intrusiveness and unpredictability of recognition errors, people often prefer to enter and edit math expressions using a computer-oriented representation, such as LaTeX or a structure-based editor. However, computer recognition of math notation is essential in large-scale recognition of mathematical documents; as well, it offers the ability to create people-centric user interfaces focused on math notation rather than computer-centric user interfaces focused on computer-oriented representatio ns. Issues that arise in computer math literacy include the diversity of math notation, the challenges in designing effective user interfaces, and the difficulty of defining and assessing performance.

Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning

Jacques Calmet
Universitaet Karlsruhe (Germany)

OMRS (Open Mechanized Reasoning systems) was designed for Automated Theorem Proving and then extended to Computer Algebra. These are the two domains at the heart of the Calculemus approach. An obvious question is to assess whether such an approach can be extended to new domains either within AI or outside of AI. There have been several attempts to turn the world into a computational system (model of everything, Fredkin's view of the universe as a global cellular automaton, Stephen Wolfram's definition of computing or simply diverse models of the philosophy of sciences). This talk stays away from such general attempts and introduces a framework that is fully set within AI. It extends the basic concepts of OMRS to diverse fields ranging from information technology to sociology through law as illustrated by examples. The main motivation is to claim that whatever the selected approach, Artificial Intelligence is gaining enough strength and power to reach new frontiers and to turn challenges that are not a priori of a purely computational nature into AI domains. Starting from purely mathematical concepts such as Jacobi's or Herbrandt's works and introducing the basic ingredients of mechanized reasoning, we can propose an abstract model for information technology. It is set within technology not philosophy. Using the concept of virtual enterprises (and virtual knowledge communities) that is gaining importance in today globalized economy, we try to illustrate that we can approach problems that where never attempted within AI.

CAMAL 40 Years On -- Is Small Still Beautiful?

John Fitch
University of Bath (UK)

Over forty years ago an algebra system was written in Cambridge, UK, designed to assist in a number of calculations in celestial mechanics and later in relativity. We present the hardware environment and the main design decisions that led this system, later dubbed CAMAL, to be used in many applications for twenty years. Its performance is investigate, both in its own time, and more recently. It is argued that a compact data representation as in CAMAL has real benefits even in today's larger memory world.

Some Traditional Mathematical Knowledge Management

Patrick D.F. Ion
Mathematical Reviews, AMS (USA)

What is mathematical knowledge and how can it be managed? There are not only differing views around on the management aspect but there is no real clarity or consensus on what mathematical knowledge is; indeed there are questions as to what knowledge is and what mathematics is. For the sake of definiteness I will adopt a particular stance from which to work, namely that aspect of organizing the knowledge of mathematics represented by Mathematical Reviews, for which I have worked since 1980. From that platform we can explore and speculate both historically and prospectively. Some new results of bibliometric and other machine-enabled examination of the mathematical literature will also be discussed.

Software Engineering for Mathematics

Georges Gonthier
Microsoft Research Cambridge (UK)

While the use of proof assistants has been picking up in computer science, they have yet to become popular in traditional mathematics. Perhaps this is because their main function, checking proofs down to their finest details, is at odds with mathematical practice, which ignores or defers details in order to apply and combine abstractions in creative and elegant ways. This mismatch parallels that between software requirements and implementation. In this talk we will explore how software engineering techniques like component-based design can be transposed to formal logic and help bridge the gap between rigor and abstraction.

Math Handwriting Recognition in Windows 7 and Its Benefits

Marko Panić
Microsoft Development Center (Serbia)

As of Windows 7, Microsoft provides users with the most natural and efficient way of inputting math handwriting recognition, as part of its operating system. Microsoft has taken a completely new approach to this matter and raised math handwriting recognition to a whole new level in terms of functionality, performance, math area coverage and correction experience. The recognizer, developed at Microsoft Development Center Serbia, is exposed through two UI components: Math Input Panel (a Windows 7 accessory) and Math Input Control (UI control designed for integration into Windows applications, such as those for word processing, computation and note taking).

Assembling the Digital Mathematics Library

David Ruddy
Project Euclid, Cornell University (USA)

The grand vision of a Digital Mathematics Library (DML), organized by a network of institutions that coordinate polices and practices regarding digitization, management, access, and preservation, has not come to pass. The vision was not flawed, but the approach to realizing it was beyond our capacity. We did not, and still do not, possess the technical understanding, the organizational capabilities, or the institutional and political willingness to implement such a vast undertaking in the manner proposed. I suggest that we should abandon the notion of a coordinated and planned approach to building the DML. The future DML, if we can even call it a library, will not be "organized," in any conventional sense of the word. This is not bad news, but a natural evolution in our progress. Recognizing this evolution will point us toward constructive areas for future work.