 |
Current automatic theorem provers, particularly those based on some variant of resolution, have concentrated on obtaining ever higher inference rates by using clever programming techniques, parallelism, etc. We believe that this approach is unlikely to lead to a useful system for actually doing mathematics. The main problem is the large amount of domain knowledge that is required for even the simplest proofs. In this paper, we describe an alternative approach that involves combining an automatic theorem prover with a symbolic computation system. The theorem prover, which we call Analytica, is able to exploit the mathematical knowledge that is built into this symbolic computation system. In addition, it can guarantee the correctness of certain steps that are made by the symbolic computation system and, therefore, prevent common errors like division by an expression that may be zero.
|
|
For the newest resources, visit Wolfram Repositories and Archives »
