The primary aim of the MATHsAiD project thus far has been to focus on theorem-discovery; to design and build a tool to automatically discover, prove and identify theorems (lemmas, corollaries, etc.) from a given set of axioms and definitions which are supplied by the user. No other input is required. This tool would, for instance, allow a mathematician to try several versions of a particular definition, and in a relatively small amount of time, be able to see some of the consequences, in terms of the resulting theorems, of each version. Moreover, the automatically discovered theorems could perhaps help the users to discover and prove further theorems for themselves. This system could also easily be used by educators (to generate exercise sets, for instance) and by students as well. In a similar fashion, this tool might also prove useful in enabling automated theorem provers to dispatch many of the more difficult proof obligations arising in software verification, by automatically generating lemmas which are needed by the prover, in order to finish these proofs.
Given a set of axioms and definitions for some particular theory, MATHsAiD analyses the information supplied, and based on this analysis, generates a sequence of sets of hypotheses plus “terms of interest”. This sequence is designed to discover the more “routine” theorems in this theory; i.e., results that one might expect to see in a mathematics textbook. For example, in set theory, given the usual definitions of union and intersection, MATHsAiD discovers, among other things, that these operations are commutative, associative, and each is distributive over the other. For each set of hypotheses/term of interest in the aforementioned sequence, MATHsAiD uses a combination of “generating” and “trivial” proof plans to discover all the more-or-less interesting results it can, subject to numerous constraints. In particular, the “generating” proof plans serve to derive (generate and prove) various conclusions c from the given hypotheses, whereas the “trivial” proof plans act as a constraint, by allowing the assertion of a newly-derived c only if it fails to be proven by any of the “trivial” proof plans. Once the system is no longer able to assert any additional conclusions, either because the combination of “generating” and “trivial” proof plans do not allow such, or because the time limit has expired, the generated conclusions are then passed to a final filtering stage, in which the less interesting ones are weeded out, leaving (hopefully) only the sorts of results that the user desires to see.
A screen shot is provided which shows, amongst other things, one of our favourite results obtained by the system thus far; namely that the Zariski space ζ(M) of a (left) unital module M over a commutative ring R with identity is, in fact, a (left) semimodule over the Zariski topology ζ(R) of R (given an appropriate choice of scalar multiplication). This result first appeared as Theorem 2 in the paper, “An Introduction to Zariski Spaces over Zariski Topologies” (R.L. McCasland, M.E. Moore and P.F. Smith), Rocky Mountain Journal of Mathematics Vol. 28 (1998), 1357-1369.
During the past few years we developed alternative methods for discovering new theorems; in particular we introduced “Theorem-producing rules” (TPRs) and “sketch-plans” (a slight variation of proof-plans). Preliminary results indicate that these new methods are more efficient (than our previous methods) at discovering quality theorems, primarily because they prohibit the generation of most lower-quality results in the first place. A research paper explaining these methods is currently in preparation.
We have also developed certain inter-theory reasoning capabilities within MATHsAiD, designed to identify interesting connections between theories -- even if at first glance those theories appear to be entirely unrelated. The aforementioned Zariski space result is one such example; this result demonstrates a connection amongst several theories, including rings, modules, topologies, semirings and semimodules. Note that such inter-theory results are simply beyond the capability of most first-order resolution theorem provers (for instance).