
Computational Logic and Continuous Mathematics, Pure and Applied
Rob Arthan
Lemma 1 Ltd. & Queen Mary, University of London (UK)
Continuous problem domains are of everincreasing 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.


MathLiterate 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 mathliterate. 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 computeroriented representation, such as LaTeX or a structurebased editor. However, computer recognition of math notation is essential in largescale recognition of mathematical documents; as well, it offers the ability to create peoplecentric user interfaces focused on math notation rather than computercentric user interfaces focused on computeroriented 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.


AbstractionBased 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 machineenabled 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 componentbased 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.
