I actually gave a short talk on how to regard Maple as a theorem prover for a course on automated theorem proof I took this past autumn: here are the slides
As DJKeenan said, the closest thing to an automated theorem prover today in Maple is is
and the assume facility. But this tool was never intended for serious use as a theorem prover, and can't really be compared to any theorem provers available today. For one thing, it doesn't have any way of expressing set membership or existential or universal quantification.
A theorem prover would be a nice asset in Maple, or with any computer algebra system. (Indeed, the MathScheme
project at my university has a combined CAS/theorem prover as its goal.)
There are a few obstacles to be overcome prior to the inclusion of a theorem prover in Maple:
1. Consistency of representation.
Different Maple packages date from different eras in Maple's evolution, and the representation of mathematical objects is not always consistent: in many cases, these distinct representations are maintained out of an understandable desire for backwards compatibility.
I would expect a proof language to require more consistency from the language. One way of avoiding this initially is to start with a restricted subset of Maple for which the representation of data is fairly consistent.
2. A robust type system.
Maple is an untyped language. It does have a type system which is very useful for making certain structural distinctions, but there are many things which cannot be distinguished by the checks the type system currently allows. A proof system will need to have all kinds of predicates about the objects concerned, many of which would be best expressed as types.
3. A means of indicating theories.
There is a massive amount of ower and sophistication within Maple's library packages, but no consistent mechanism for indicating the underlying theory upon which a particular algorithm is based and how this theory may relate to other theories.
Programmers and advanced users of Maple know which particular invocations of commands may be used together. They know that symbols in expressions passed to evalc
are understood to be reals, while in other contexts these symbols are taken to be complex numbers. They know that LinearAlgebra
is based on, well, linear algebra, while limit
is based on calculus. However, an automated theorem prover will requires this human knowledge to be systematized and justified.
Indeed, it's highly probable that much of the expressive power of Maple depends on the combination of packages with different underlying theories to positive effect. Some packages may be even based on more advanced mathematics than their authors intended or realized. Thinking deeply about how the underlying theories do relate may produce some very interesting revelations, and maybe even new mathematical knowledge!
On the other hand, "borderline" cases involving the combinations of different theories may well be responsible for outstanding bugs in this and other CASes, so some deep thought here might help fix bugs too.