No. 51, April 2001

Contents

From the AAR President
MathXpert As a Theorem Prover
Woody Bledsoe Student Travel Award
Herbrand Award: Amendments to the Selection Procedure
Conference Calls

MathXpert As a Theorem Prover:
Introduction to MathXpert

MathXpert (the software formerly known as Mathpert) is a program designed to help people learn algebra, trigonometry, and calculus. It contains a computer algebra system, a logic module called the prover, a graphics module, and some complex code meant to provide a simple user interface. The program's primary purpose was education, and it is being marketed with that in mind (see the Web site). This article will ignore education, graphics, and user interfaces and will focus on the logical capabilities of MathXpert. We will attempt to answer the AAR president's question, "Is MathXpert a theorem prover, or not?"

A MathXpert session begins with the specification of a topic (for example, solving cubic equations, verifying trigonometric identities, or evaluating integrals--there are about 140 topics altogether). Then the user enters a problem appropriate for that topic. After the problem is accepted, the next task is the generation of a step-by-step solution of the problem. This can take place under user control, with the user choosing the steps and the program executing them. It can also take place in auto mode, in which MathXpert can generate the entire solution. These two modes are roughly analogous to what we mean when we say proof checker and theorem prover. Only auto mode solutions will be discussed in this article, since our topic is theorem-proving.

Here is a sample solution, the output of MathXpert when the input is the arithmetic-geometric mean inequality.

Is this a proof? I am certain it would be accepted as such in most mathematics classes.

One may object, however, that this is not a formal proof; I shall take up below the question whether there is a formal proof here to be extracted. At the moment, the only purpose of displaying this example is to fix the ideas as to what MathXpert actually produces.

The company marketing MathXpert is about to make available MathXpert Online, which neatly separates the auto mode capabilities of MathXpert from all others and makes the auto mode solutions (only) available over the Internet for free. When this service is available, it will be found at the Web site.

Logic and Correct Computation

MathXpert makes the connection between logic and computation by maintaining a list of assumptions. Each (visible) line of computation can be thought of as depending on a list of assumptions. If we put this list of assumptions to the left of , and the visible step A to right of , then we have a sequent , of which is called the antecedent and A the succedent. When computational steps (operations) are applied, they may have side conditions (hypotheses). These have to be verified before the operation can be legitimately applied. This mechanism prevents MathXpert from deriving false conclusions. More details of how side conditions are handled in this sequent-calculus framework can be found in [2].

Other computer algebra systems have nothing like this kind of logical underpinnings and hence can easily be led to deduce false conclusions. Witness this example from Mathematica 4.0.2:

In[3]= Integrate[1/Sin[x], {x, -1, 1}] 
 
Out[3]= 0 

One may well say that correct computation is nice, but it does not make a theorem prover. Of course that is correct, but if we want a theorem prover that can make proofs including computational steps, such as the above example, then the computational steps must be logically correct. Correct computation is a prerequisite to a theorem prover that can take computational steps.

Kinds of Theorems MathXpert Can Prove

Most of the topics available in MathXpert begin with a mathematical expression (such as an integral, limit, derivative, or algebraic expression), and the solution takes steps that rewrite each line to an equal expression. The theorem that is proved is that the original problem equals the last line generated, provided that the assumptions on which the last line depends hold. (These can be seen in MathXpert by choosing View Assumptions.) There are three other types of problems to be considered: solving equations, verifying identities, and "solving" inequalities. When solving equations, MathXpert essentially is asked to find the values of x such that f(x) = 0, and if it succeeds, it gives an explicit disjunction that is equivalent to the existential statement. In the case of trigonometric equations, the solutions are parametrized by new integer parameters; for example, the solution of is .

In MathXpert, to "solve" an inequality for x means to reduce the inequality to a disjunction of inequalities or pairs of inequalities which express the solution set as a union of intervals. This includes as a special case the possibility that the answer might be true, as in the arithmetic-geometric mean example above. This means that the inequality has been proved. Unlike with equations, there is no clear distinction between verifying and solving an inequality.

How the Prover Works

The MathXpert prover can perhaps best be thought of as using rewrite-rule technology combined with evaluation and ad hoc control of the rewrites. It is not purely rewrite rules: the simplest example is the rule that permits rewriting x³ x⁵ as x⁸. Arithmetic is performed on the exponents, which involves evaluation. MathXpert can also evaluate much more complex expressions during application of rewrite rules. Note that some of the more complex rules are not exposed to the (student) user of MathXpert but are used only internally. For example, there are sophisticated algorithms for determining if a polynomial has a zero on a given interval. In general, the proof produced is supposed to be comprehensible to a freshman, so these algorithms are used only to check side conditions.

The Underlying Logic

Part of the prover has to deal with verifying side conditions inside the scope of a bound variable (such as in a limit term or definite integral). In the course of justifying the use of algorithms based on nonstandard analysis for verifying side conditions in a limit term, I set out a formal theory that I believe adequately captures the mathematical realm of MathXpert [1]. The variables can range over integers, real numbers, or complex numbers. The logic must deal correctly with terms that can be undefined such as x, which is accomplished by the use of the Logic of Partial Terms (LPT). It must also include term-formation rules for limits, derivatives, and integrals. It is also possible to use a function variable in MathXpert, although the vast majority of theorems do not use them. Formally speaking, it might be simplest to allow them, and to allow the formation of lambda-terms, because then limits, derivatives, and integrals can be defined by using lambda-terms. Of course, so can quantifiers then, but in practice MathXpert proofs are quantifier free.

The axioms of this theory are numerous: some 1600 mathematical operations are implemented in MathXpert. Of course, it is possible to derive these systematically from a small number of axioms. But the proofs MathXpert actually generates can appeal to any of these 1600 "axioms" at any step. In principle it would be possible to write a program that translated MathXpert proofs automatically into proofs in some simple logical theory whose axioms would amount, in essence, to the axioms of ordered fields complete with respect to zeroes of functions defined in the theory, and the definitions of the trigonometric and exponential functions, and closed under derivatives and integrals of functions defined by terms of the theory. Since there are also integer variables, a few axioms about the integers would be required, but MathXpert does not use induction.

Enabling the Prover to Handle Quantifiers

I combined MathXpert's logical engine with a very simple theorem prover that applies the rules of Gentzen's sequent calculus "backwards". This added the ability to handle quantifiers explicitly, so that, for example, epsilon-delta proofs could be reduced to the necessary inequalities. This combination program, known as Weierstrass, was able [3] to prove the epsilon-delta continuity of several specific functions such as x³ and and to prove the irrationality of e. These proofs depend at some points on some special inference rules for inequalities, but fundamentally they depend on MathXpert's logical engine for the rewriting steps.

Comparison with Otter

MathXpert does not search for a proof--it simply uses its rewrite-style engine. In that sense it is much weaker than Otter, which can generate and examine hundreds of thousands of intermediate deductions. It cannot work with arbitrary theories but only with the fixed mathematical framework used in high-school algebra and freshman calculus. It cannot, for example, deduce the ten Knuth-Bendix axioms that form a complete confluent set for group theory---one cannot even ask the question, since it assumes multiplication is commutative (except for matrices).

On the other hand, it is not quite trivial for most theorem provers (including Otter) to prove the arithmetic-geometric mean inequality, say from the axioms of ordered fields with a square-root function. I do not mean to imply that proving that inequality is a remarkable achievement--of course, the arithmetic-geometric mean inequality falls within the decidable realm of real-closed fields, and so can be proved by the well-known CAD decision algorithm. I propose it as an interesting exercise for AAR members to get their favorite theorem-prover to prove it by its usual logical means. For MathXpert it is just another problem.

Because MathXpert does not search for proofs and cannot deal with an arbitrary first-order theory, it is not a traditional theorem prover, but it does produce proofs. MathXpert's strengths, as a theorem-prover, are first, its ability to take steps involving computation, and second, its ability to handle inequalities.

Notes

The papers listed below and other papers about MathXpert can be downloaded from the Web. Other relevant links can be found on the author's
home page.

References

[1] Beeson, M., Using nonstandard analysis to verify the correctness of computations, International Journal of Foundations of Computer Science 6, no. 3 (1995) 299-338.

[2] Beeson, M., MathXpert: Computer support for learning algebra, trigonometry, and calculus, in: A. Voronkov (ed.), Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence 624, Springer-Verlag, Berlin (1992).

[3] Beeson, M., Automatic generation of epsilon-delta proofs of continuity, in: J. Calmet and J. Plaza (eds.), Artificial Intelligence and Symbolic Computation, Lecture Notes in Artificial Intelligence 1476, pp. 67-83, Springer-Verlag, Berlin (1998).

Woody Bledsoe Student Travel Award:
Call for Nominations

In 2001, IJCAR will take place June 18-23 in Siena, Italy (for further information see the Web site. The winners will be reimbursed (to a maximum of US $600) for their conference registration, transportation, and accomodation expenses. Preference will be given to students who do not have alternative funding. While preference will be given to students who will play an active role in the conference, including all attached workshops and events, also students who do not expect to give presentations, including students who have just begun their research in automated deduction or are considering the field, are encouraged to apply.

A nomination consists of a recommendation letter of up to 300 words from the student's supervisor. Nominations for IJCAR 2001 should be sent by e-mail to
Fabio Massacci, IJCAR 2001 Conference Chair (ijcar-cch@dii.unisi.it) and
Rajeev Gore, Alexander Leitsch, Tobias Nipkow, IJCAR 2001 Program Co-Chairs (ijcar-pch@dii.unisi.it),
with copies to

Ulrich Furbach, CADE Inc. President (uli@informatik.uni-koblenz.de) and
Neil V. Murray, CADE Inc. Treasurer (nvm@cs.albany.edu).

Nominations must arrive no later than May 7, 2001, and the winners will be notified by May 14, 2001. The awards will be presented at IJCAR; in case a winner does not attend, the chairs and trustees may transfer the award to another nominee or give no award.

Herbrand Award: Amendments to the Selection Procedure

FLoC'02: Call for Workshop Proposals

The third Federated Logic Conference (FLOC'02) will be held at the University of Copenhagen, Denmark, in July 2002, hosted at DIKU. Seven conferences will participate in FLoC: Conference on Automated Deduction (CADE), Conference on Computer-Aided Verification (CAV), Conference on Formal Methods (FM), International Conference on Logic Programming (ICLP), IEEE Symposium on Logic in Computer Science (LICS), Conference on Rewriting Techniques and Applications (RTA), and Conference on Analytic Tableaux and Related Methods (TABLEAUX). For more information see http://floc02.diku.dk/.

The organizers have made arrangements to facilitate the running of pre-, post-, and mid-FLoC workshops. Each workshop will have its own registration. It is not necessary to register for FLoC in order to attend workshops. Meeting rooms and accommodations have been reserved at the Hans Christian Orsted Institute as follows:

Pre-FLoC workshops: Saturday July 20-Sunday July 21, 2002.
Mid-FLoC workshops: Thursday July 25-Friday July 26, 2002.
Post-FLoC workshops: Wednesday July 31-Thursday August 1, 2002.

Researchers and practitioners are invited to submit proposals for workshops on topics relating logic (broadly understood) to computer science. Each workshop proposal must indicate one sponsoring conference among the participating conferences. (It is suggested that prospective workshop organizers contact the conference program chair before submitting a proposal.) The sponsoring conference will have to accept financial responsibility for the workshop. The FLoC Organizing Committee will determine the final list of accepted workshops based on the recommendations from the sponsoring conferences and subject to the availability of space and facilities.

Proposals should consist of two parts: (1) a short scientific justification of the proposed topic, its significance, and the particular benefits of a workshop; and (2) an organizational, part including contact information about organizers, proposed format and agenda, procedures for selecting papers and participants, duration (which may vary from one day to two days) and preferred period, and proposed sponsoring conference. Additional organizational plans may include potential invited speakers, demo sessions, and plans for proceedings or other publications.

Proposals are due May 15, 2001. Proposals may be submitted either electronically or in hard copy and should be addressed to the Program Chair of the sponsoring conference as well as to

Sebastian Skalberg (Workshop Chair)
DIKU, University of Copenhagen
Universitetsparken 1
DK-2100 Copenhagen East
Denmark
+45 353 21448 (secretary); +45 353 21403 (office); +45 353 21401 (fax); skalberg@diku.dk

International Workshop on Functional and
(Constraint) Logic Programming

WFLP 2001 combines two annual workshops on declarative programming. The international workshops on functional and logic programming (WFLP) aim at bringing together researchers interested in functional programming, logic programming, as well as their integration. The workshops on (constraint) logic programming (WLP) are the annual meeting of the Society of Logic Programming (GLP e.V.) and bring together researchers interested in logic programming, constraint programming, and related areas like databases and artificial intelligence. This joint workshop seeks to promote the cross-fertilizing exchange of ideas and experiences among researches and students from the different communities. The primary focus is on new and original research results, but submissions describing innovative products, prototypes under development or interesting experiments (e.g., benchmarks) are also encouraged.

Topics of interest are functional programming; logic programming; constraint programming; deductive databases; extensions of declarative languages, objects; multiparadigm declarative programming; foundations, semantics, nonmonotonic reasoning, dynamics; parallelism, concurrency; program analysis, abstract interpretation; program transformation, partial evaluation, meta-programming; specification, verification, declarative debugging; knowledge representation, machine learning; implementation of declarative languages; advanced programming environments and tools; and applications.

Extended abstracts (max. 10 pages) or a system description (max. 3 pages) in postscript format (11pt) should be sent via email to wflp2001@informatik.uni-kiel.de by May 15, 2001. The proceedings with the full versions of all accepted contributions will be published as a Technical Report of the University of Kiel.

For further information, see the Web site.

LPAR'2001

The eighth international conference on Logic for Programming, AI, and Reasoning will be held in La Habana, Cuba, December 3-7, 2001.

Topics of interest include the following: automated reasoning, logic in artificial intelligence, interactive theorem proving, lambda and combinatory calculi, implementations of logic, constructive logic and type theory, design of logical frameworks, logical foundations of programming, program and system verification, model checking, knowledge representation and reasoning, rewriting, constraint programming, and description logics.

Both "theoretical" papers (max. 15 pages) and "experimental" papers (max. 10 pages) are welcome and are due July 15, 2001. Instructions for submission are on the conference Web page.

New Books

Automated Theorem Proving: Theory and Practice

Monty Newborn (McGIll University) has published a new book entitled Automated Theorem Proving: Theory and Practice. The following is the material that appears on the back cover of the book.

As the 21st century begins, the power of our new tool and partner, the computer, is increasing at an astonishing rate. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from facts, or abstractly, to prove theorems, the subject of this book. Automated Theorem Proving describes how this process is performed. It first introduces the mathematical language of predicate calculus and then discusses the basic inferencing rules of binary resolution and binary factoring. Using these rules, two theorem-proving systems are described. The first (HERBY) is based on constructing closed sematic trees, whereas the second (THEO) is based on the classic resolution-refutation approach. These programs are included on the accompanying CD-ROM, which has their source code and runs on both Unix and Linux.

Topics and features:

• clear, concise presentation of the fundamentals
• extensive end-of-chapter exercises, with solutions
• HERBY, an excellent and unique semantic-tree theorem-proving program
• THEO, a strong resolution-refutation theorem-proving program*approximately 200 theorems included on the CD-ROM for experimentation

Elimination Methods

A new book entitled Elimination Methods by Dongming Wang presents a systematic treatment of elimination algorithms that cmpute various decompositions for systems of multivariate polynomials. The proposed algorithms and their underlying theories are based on the previous work of J. F. Ritt, W.-T. Wu, A. Seidenberg, and J. M. Thomas. Of particular interest to AAR readers is Section 7.2, Automated geometry theory proving.

244 pages
Springer, 2001
ISBN 3-211-83241-6
US$69

Symbolic Computation and Automated Reasoning:
The CALCULEMUS-2000 Symposium

While mathematical software packages are commercially successful and widely used, the use of formal methods in hardware and software development is also becoming more and more important and necessary. This has made deduction systems indispensable because of the complexity and sheer size of the reasoning tasks involved. This volume is devoted to the integration of computer algebra systems and deduction systems and the results presented will improve the automated design of hardware and software systems.

The articles in this collection are based on presentations at the 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning on August 6-7, 2000, in St. Andrews, Scotland. Edited by Manfred Kerber and Michael Kohlhase, the volume addresses all aspects relating deduction and computer algebra systems.

288 pages
A. K. Peters, Ltd., 2001
ISBN: 1-56881-145-4
US $60
Web site