**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] |