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.
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
Copyright © 2001 Wolfram Media, Inc. All rights reserved.