The Mathematica Journal
Departments
Feature Articles
Columns
New Products
New Publications
Classifieds
Calendar
News Bulletins
Mailbox
Letters
FAQ
Write Us
About the Journal
Staff and Contributors
Submissions
Subscriptions
Advertising
Back Issues
Home
Download this Issue

Theorema's Prove Command

The current provers of Theorema include various predicate logic provers, various induction provers, a set theory prover, and special provers using the Gröbner bases technique, Collins quantifier elimination, and the Zeilberger-Paule approach to handling combinatorial identities. A recent proof method developed by the author, called the "PCS-method", is particularly well-suited for proving formulae with "alternating quantifiers", which typically appear in proofs in analysis. An example of applying this method is given below.

Theorema also includes special tools for mathematical knowledge management, natural language proof presentation, and the generation of new pictorial symbols, called "logicographic symbols".

Here is a typical example of defining a mathematical notion in Theorema by entering it in a Mathematica input cell.

For limit[f, a], read "the sequence f has limit a". Now, one may be interested in proving a proposition on this notion, such as the following one.

Of course, this proposition cannot be proved without any knowledge of auxiliary notions like '+' and so forth. It may be surprising that actually very little knowledge is necessary for proving the proposition. In this example, the following statements are sufficient for the proof.

In Theorema, formulae can be combined in "knowledge bases" using the "Theory" construct, which should be self-explanatory.

Now a proof of the above goal proposition can be generated completely automatically by just entering the following.

The three main arguments of a call to the Theorema command Prove are: the name of the proposition to be proved, the name of the theory (knowledge base) to be used in the proof, and the particular prover by which the proof should be generated. After entering this command, the proof shown in the next section, including the English explanatory intermediate text, will be generated in an extra notebook without any further user interaction.


Copyright © 2001 Wolfram Media, Inc. All rights reserved.

[Article Index][Prev Page][Next Page]