Intelligent Computer Mathematics

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 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 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 representations. 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.

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. 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.

Despite its mathematical origins, progress in computer assisted reasoning has mostly been driven by applications in computer science, like hardware or protocol security verification. Paradoxically, it has yet to gain widespread acceptance in its original domain of application, mathematics; this is commonly attributed to a “lack of libraries”: attempts to formalize advanced mathematics get bogged down into the formalization of an unwieldly large set of basic resuts.

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.

Nowadays, writing a math paper in a word processing application or performing calculations in a computational engine often requires spending a considerable amount of time creating math expressions using either a complex UI model with a multitude of drop-down buttons or a complicated and difficult to remember linear format input. 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 problem and raised math handwriting recognition to a whole new level in terms of functionality, performance and area coverage.

Since discussions of a Digital Mathematics Library (DML) were first formalized, it has been recognized that such a collection would be federated, consisting of a “network of institutions.” Implicit in this conception, and explicit in much of the early DML planning documents, is the assumption that this network would be organized in some manner-coordinated and held together by formally accepted policies and practices regarding collection, management, access, and preservation.

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. I 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 investigated, both in its own era, and more recently. It is argued that a compact data representation as in CAMAL has real benefits even in today’s larger memory world.

We present a specialised (polynomial-based) rule for the propositional logic called the

Independence Rule

, which is useful to compute the conservative retractions of propositional logic theories. In this paper we show the soundness and completeness of the logical calculus based on this rule, as well as other applications. The rule is defined by means of a new kind of operator on propositional formulae. It is based on the

boolean derivatives

on the polynomial ring

${\mathbb F}_2[{\bf x}]$

.

Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.

How do we recognize when an answer is “right”? This is a question that has bedevilled the use of computer systems in mathematics (as opposed to arithmetic) ever since their introduction. A computer system can certainly say that some answers are definitely wrong, in the sense that they are provably not an answer to the question posed. However, an answer can be mathematically right without being pedagogically right. Here we explore the differences and show that, despite the apparent distinction, it is possible to make many of the differences amenable to formal treatment, by asking “under which congruence is the pupil’s answer equal to the teacher’s?”.

It can be useful to consider complex matrix expressions as circuits, interpreting matrices as parts of a circuit and composition as the “wiring,” or flow of information. This is especially true when describing quantum computation, where graphical languages can vastly reduce the complexity of many calculations [3,9]. However, manual manipulation of graphs describing such systems quickly becomes untenable for large graphs or large numbers of graphs. To combat this issue, we are developing a tool called Quantomatic, which allows automated and semi-automated explorations of graph rewrite systems and their underlying semantics. We emphasise in this paper the features of Quantomatic that interact with a computer algebra system to discover graphical relationships via the unification of matrix equations. Since these equations can grow exponentially with the size of the graph, we use this method to discover small identities and use those identities as graph rewrites to expand the theory.

Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows a much better performance than EAT due, among other reasons, to a smart encoding of degeneracy lists as integers. In this paper, we give a complete automated proof of the correctness of this encoding used in Kenzo. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp. The most interesting idea, from a methodological point of view, is our use of EAT to build a model on which the verification is carried out. Thus, EAT, which is logically simpler but less efficient than Kenzo, acts as a mathematical model and then Kenzo is formally verified against it.

Methods for deciding quantifier-free non-linear arithmetical conjectures over ℝ are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over ℝ is decidable, it is fundamentally infeasible: any general decision method for this problem is worst-case exponential in the dimension (number of variables) of the formula being analysed. This is unfortunate, as many practical applications of real algebraic decision methods require reasoning about high-dimensional conjectures. Despite their inherent infeasibility, a number of different decision methods have been developed, most of which have “sweet spots” – e.g., types of problems for which they perform much better than they do in general. Such “sweet spots” can in many cases be heuristically combined to solve problems that are out of reach of the individual decision methods when used in isolation.

RAHD

(“Real Algebra in High Dimensions”) is a theorem prover that works to combine a collection of real algebraic decision methods in ways that exploit their respective “sweet-spots.” We discuss high-level mathematical and design aspects of

RAHD

and illustrate its use on a number of examples.

In previous work we have developed procedures to analyse, compute with and reason about abstract matrices, that is, matrices represented with symbolic dimensions and with a mixture of terms and ellipsis symbols to describe their structure. A central component in this are the so-called “support functions”, which enable the representation of abstract matrices in closed forms. A key issue in making reasoning about such structures effective is controlling the complexity of the internal term structure of the closed form, which, in turn, hinges critically on the design of the support functions used.

Our earlier support functions were simple, easy to work with and sufficient to capture arithmetic of general partitioned matrices fully. They explicitly represent each potential homogeneous region, usually a triangle or a rectangle, of an abstract matrix with a single term. However, adding or multiplying a sequence of matrices can result in exponentially many different cases of possible regions that have to be represented, and the existence of many of these is mutually exclusive. As this representation can become unwieldy in certain situations, we experiment with a different type of support function that allows us to represent only one of the possible cases explicitly, and have all other cases captured by the representation implicitly.

In this paper we discuss this new support function and develop the full abstract matrix addition algorithm for this representation. We show that we indeed obtain much more concise and intuitive closed forms, retaining the properties necessary for reasoning with abstract matrices and being able to recover the human readable region structure from the combination of abstract matrices under addition. This representation reduces the time and space complexity of performing

K

abstract matrix additions from

O

(

N

dK

) to

O

(

K

d

N

d

), for

d

the number of boundary directions (1 ≤ 

d

 ≤ 4) and

N

the maximum number of boundaries in any direction in the argument matrices.

A test in terms of invariants for the existence of a factorization of a bivariate, non-hyperbolic third-order Linear Partial Differential Operator (LPDO) which has a given factorization of its principal symbol is found. The invariants that are used are with respect to known gauge transformations, which is together with constructive factorization itself are essentially involved in modern exact integration algorithms. The invariants, and even a generating system of those were found in previous paper using Moving Frames methods.

In order to find the expressions in terms of invariants that guarantee the existence of a factorization of a certain type, we show that the operation of taking the formal adjoint can be also defined in terms of invariants, that is for equivalence classes of LPDOs, and explicit formulae defining this operation in the space invariants are obtained. The operation of formal adjoint is highly interesting for factorization of LPDOs for if the initial operator has a factorization, its adjoint has also one, and they are related. (informally, the factorization types are symmetric).

As a variation on the known theme of Gödel numberings, isomorphisms defining data type transformations in a strongly typed functional language are organized as a finite groupoid using a higher order combinator language that unifies popular data types as diverse as natural numbers, finite sequences, digraphs, hypergraphs and finite permutations with more exotic ones like hereditarily finite functions, sets and permutations.

Recent work has detailed the conditions under which univariate Laurent polynomials have functional decompositions. This paper presents algorithms to compute such univariate Laurent polynomial decompositions efficiently and gives their multivariate generalization.

One application of functional decomposition of Laurent polynomials is the functional decomposition of so-called “symbolic polynomials.” These are polynomial-like objects whose exponents are themselves integer-valued polynomials rather than integers. The algebraic independence of

X

,

X

n

,

$X^{n^2/2}$

,

etc

, and some elementary results on integer-valued polynomials allow problems with symbolic polynomials to be reduced to problems with multivariate Laurent polynomials. Hence we are interested in the functional decomposition of these objects.

Many approaches have been proposed over the years for the recognition of mathematical formulae from scanned documents. More recently a need has arisen to recognise formulae from PDF documents. Here we can avoid ambiguities introduced by traditional OCR approaches and instead extract perfect knowledge of the characters used in formulae directly from the document. This can be exploited by formula recognition techniques to achieve correct results and high performance.

In this paper we revisit an old grammatical approach to formula recognition, that of Anderson from 1968, and assess its applicability with respect to data extracted from PDF documents. We identify some problems of the original method when applied to common mathematical expressions and show how they can be overcome. The simplicity of the original method leads to a very efficient recognition technique that not only is very simple to implement but also yields results of high accuracy for the recognition of mathematical formulae from PDF documents.

Hilbert’s concept of formal proof is an ideal of rigour for mathematics which has important applications in mathematical logic, but seems irrelevant for the practice of mathematics. The advent, in the last twenty years, of proof assistants was followed by an impressive record of deep mathematical theorems formally proved. Formal proof is practically achievable. With formal proof, correctness reaches a standard that no pen-and-paper proof can match, but an essential component of mathematics — the insight and understanding — seems to be in short supply. So, what makes a proof understandable? To answer this question we first suggest a list of symptoms of understanding. We then propose a vision of an environment in which users can write and check formal proofs as well as query them with reference to the symptoms of understanding. In this way, the environment reconciles the main features of proof: correctness and understanding.

Mathematical Knowledge Management (MKM), as a field, has seen tremendous growth in the last few years. This period was one where many research threads were started and the field was defining itself. We believe that we are now in a position to use the MKM body of knowledge as a means to define what MKM is, what it worries about, etc. In this paper, we review the literature of MKM and gather various metadata from these papers. After offering some definitions surrounding MKM, we analyze the metadata we have gathered from these papers, in an effort to cast more light on the field of MKM and its evolution.

We document the creation of a new set of OpenMath content dictionaries to support the expression of quantities and units under the International System of Units (SI). While preserving many of the concepts embodied in the original content dictionaries, these new content dictionaries provide a foundation for quantities and units that is compliant with international standards. We respond to questions raised in prior efforts to create content dictionaries for units and dimensions by proposing and applying some rationalized criteria for the creation of content dictionaries in general. The results have been released and submitted to the OpenMath website as contributed content dictionaries.

One of the fundamental and seemingly simple aims of mathematical knowledge management (MKM) is to develop and standardize formats that allow to “represent the meaning of the objects of mathematics”. The open formats OpenMath and MathML address this, but differ subtly in syntax, rigor, and structural viewpoints (notably over calculus). To avoid fragmentation and smooth out interoperability obstacles, effort is under way to align them into a joint format OpenMath/MathML 3. We illustrate the issues that come up in such an alignment by looking at three main areas: bound variables and conditions, calculus (which relates to the previous) and “lifted”

n

-ary operators.

Active mathematical documents are distinguished from traditional paper-oriented ones by their ability to interactively adapt to a reader’s inputs. This includes changes in the presentation of the content of the document as well as changes of that content itself.

We have developed the JOBAD architecture, a client/server infrastructure for active mathematical documents. A server-side module generates active documents, which a client-side JavaScript library makes accessible for user interaction. Further server-side modules – in the same backend, or distributed web services – dynamically respond to callbacks invoked when the user interacts with the client. These three components are tied together by the JOBAD active document format, which backwards-compatibly enhances MathML by information about interactivity.

JOBAD is designed to be modular in the specific web services offered. As examples, we present folding and elision in mathematical expressions, type and definition lookup of symbols, as well as conversion of physical units. We evaluate our framework with a case study where a large collection of lecture notes is served as an active document.

Interactive exercises play a major role in an adaptive learning environment

ActiveMath

. They serve two major purposes: training the student and assessing his current mastery, which provides a basis for further adaptivity. We present the current state of the knowledge representation format for interactive exercises in

ActiveMath

. This format allows for representing multi-step exercises, that contain different interactive elements. The answer of the learner can be evaluated semantically. Various types of feedback and hint hierarchies can be represented. Exercise language possesses a construction for specifying additional components generating (parts of) the exercise. One example of such component is a Randomizer, which allows for authoring parametrized exercises. Another example is so-called Domain Reasoner Generator, that automatically generates exercise steps and refined diagnosis upon the learner’s answer. This turns ActiveMath system into an ITS as soon as some Domain Reasoner is connected to it. Finally, several tutorial strategies can be applied to the same exercise. This strategies control feedback and the way the exercise is navigated by the learner, and can adapt to the learner.

Effective communication and collaboration of symbolic and quantitative knowledge requires the digitization of mathematical expressions. The multi-dimensionality of mathematical notation creates a challenge for mathematical software editors. There are two different approaches for handling the multi-dimensionality of mathematical notation: either using a two-dimensional writing environment in which symbols can be placed freely (unit-based) or using an environment in which single-dimensional structural elements can be nested (structure-based). The structure-based approach constrains how users write expressions. These constraints may conflict with how mathematics is normally written. A study is reported that examines how users write mathematical expressions using two graphic based editors: one that is structure-based and one that allows the free-form manipulation of selected symbols in a diagrammatic fashion (unit-based). The results are contrasted with how users handwrite mathematics in a physical medium and implications are drawn for future software design.

Interactive exercise assistants support students in practicing exercises, and acquiring procedural skills. Many mathematical topics can be practiced in such assistants. Ideally, an interactive exercise assistant not only validates final answers, but also comments on intermediate steps submitted by a student, provides hints on how to proceed, and presents worked-out examples. For these purposes, fine control over the symbolic simplification procedures of the underlying mathematical machinery is needed.

In this paper, we introduce views for mathematical expressions. A view defines an equivalence relation by choosing a canonical form of mathematical expressions. We use views to track and recognize intermediate answers, to help in presenting expressions to a user, and to control the granularity of the steps in worked-out examples. We develop the concept of a view, discuss the laws it satisfies, and show how views are composed, which means that they can be used for multiple exercise classes.

Since Mathematics really is about what mathematicians do, in this paper, we will look at the mathematical practice of

framing

, in which an object of interest is viewed in terms of well-understood mathematical structures. The new perspective not only allows to deepen the understanding of a resp. object, it also facilitates new insights. We propose a model for framing in the context of theory graphs, and show how framing can be exploited to enhance the interaction with MKM systems. We use the framing extension of our

SACHS

system — a semantic help system for

MS Excel

— as a concrete example.

Spreadsheets are mathematical documents that are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. In this paper we show that spreadsheets are interesting applications for MKM techniques which can alleviate usability and maintenance problems as spreadsheet-based applications grow evermore complex and long-lived. We present the software and information architecture of a semantic enhancement of MS Excel spreadsheets that aims at compensating the computational bias in spreadsheets.

Converting mathematical documents from a human-friendly natural language to a form that can be readily processed by computers is often a tedious, manual task. Translating between varied computerised forms is also a difficult problem. MathLang, a system of methods and representations for computerising mathematics, tries to make these tasks more tractable by breaking the translation down into manageable portions. This paper presents a method for creating rules to translate documents from MathLang’s internal representation of mathematics to documents in the language of the Isabelle proof assistant. It includes a set of example rules applicable for a particular document. The resulting documents are not completely verifiable by Isabelle, but they represent a point to which a mathematician may take a document without the involvement of an Isabelle expert.

The semantic web ontology languages RDFS and OWL are widely used but limited in both their expressivity and their support for modularity and integrated documentation. Expressivity, modularity, and documentation of formal knowledge have always been important issues in the MKM community. Therefore, we try to improve these ontology languages by well-tried MKM techniques.

Concretely, we propose embedding the language concepts into

OMDoc

to make use of its modularity and documentation infrastructure. We show how

OMDoc

can be made compatible with semantic web ontology languages, focusing on knowledge representation, modular design, documentation, and metadata. We evaluate our technology by re-implementing the Friend-of-a-friend (FOAF) ontology and applying it in a novel metadata framework for technical documents (including ontologies).

This paper presents a proof language based on the work of Sacerdoti Coen [1,2], Kirchner [3] and Autexier [4] on

${{\bar\lambda\mu\tilde{\mu}}}$

, a calculus introduced by Curien and Herbelin. [5,6] Just as

${{\bar\lambda\mu\tilde{\mu}}}$

preserves several proof structures that are identified by the

λ

-calculus, the proof language presented here aims to preserve as much proof structure as reasonable; we call that property being

logically saturated

. This leads to several advantages when the language is used as a generic exchange language for proofs, as well as for other uses.

We equip the calculus with a simple rendering in pseudo-natural language that aims to give people tools to read, understand and exchange terms of the language. We show how this rendering can, at the cost of some more complexity, be made to produce text that is more natural and idiomatic, or in the style of a declarative proof language like Isar or Mizar.

The extraction of the relations of nested table headers to content cells is automated with a view to constructing narrow domain ontologies of semi-structured web data. A taxonomy of tessellations for displaying tabular data is developed.

X-Y tessellations

that can be obtained by a divide-and-conquer method are asymptotically only an infinitesimal fraction of all partitions of a rectangle into rectangles.

Admissible

tessellations are the even smaller subset of all partitions that correspond to the structures of published tables and that contain only rectangles produced by successive guillotine cuts. Many of these can be processed automatically. Their structures can be conveniently represented by X-Y trees, which facilitate relating hierarchical row and column headings to content cells. A formal grammar is proposed for characterizing the X-Y trees of layout-equivalent admissible tessellations. Algorithms are presented for transforming a tessellation into an X-Y tree and hence into multidimensional, layout- independent Category Trees (Wang abstract data types).

Representation theory is a branch of algebra that allows the study of groups through linear applications, i.e. matrices. Thus problems in abstract groups can be reduced to problems on matrices. Representation theory is the basis of character theory. In this paper we present a formalization of finite groups representation theory in the

Coq

system that includes a formalization of Maschke’s theorem on reducible finite group algebra.

The lack of an assistance support may result in disturbance of coauthors by beginners who ask for help when they are in trouble to produce or reuse shared resources. Additionally, collaborators may not be sure if their respective production is consistent with the collaborative common contribution. We tackle this issue by developing a group awareness knowledge based system that takes the responsibility to automatically evaluate and reuse mathematical formulae, and deduces which participant is a possible expert to help others.

Recent work on computer recognition of handwritten mathematical symbols has reached the state where geometric analysis of isolated characters can correctly identify individual characters about 96% of the time. This paper presents confidence measures for two classification methods applied to the recognition of handwritten mathematical symbols. We show how the distance to the nearest convex hull of nearest neighbors relates to the classification accuracy. For multi-classifiers based on support vector machine ensembles, we show how the outcomes of the binary classifiers can be combined into an overall confidence value.

Mathematical Knowledge can be encoded by means of Open Mathematical Documents (OMDoc) to interface both Computer Algebra and Proof Assistant systems. In this paper, we show how a unique OMDoc structure can be used to dynamically generate, both a Graphical User Interface for a Computer Algebra system and a script for a Proof Assistant. So, the OMDoc format can be used for representing different aspects. This generic approach has been made concrete through a first prototype interfacing the Kenzo Computer Algebra system and the ACL2 Theorem Prover, both based on the Common Lisp programming language. An OMDoc repository has been developed allowing the user to customize the application in an easy way.

In this short communication we want to give an overview of how OpenMath is used in the European project “SCIEnce” [12]. The main aim of this project is to allow unified communication between different computer algebra systems (CASes) or different instances of one CAS. This may involve one or more computers, clusters, and even grids.

The main topics are the use of OpenMath to marshal mathematical objects for transport between different CASes, an alternative textual OpenMath representation more suitable for human reading and writing, and finally the publicly released Java Library developed for the project.

Taking the specific problem domain of indefinite integration, we describe the on-going development of a repository of mathematical knowledge based on transformation rules. It is important that the repository be not confused with a look-up table. The database of transformation rules is at present encoded in Mathematica, but this is only one convenient form of the repository, and it could be readily translated into other formats. The principles upon which the set of rules is compiled is described. One important principle is minimality. The benefits of the approach are illustrated with examples, and with the results of comparisons with other approaches.

Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering of MathML Presentation, and by the automatic handling of overloading by means of a flexible disambiguation mechanism. We show how to use these features to obtain a simple learning environment for natural deduction, without modifying the source code or Matita.