Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Analytica--A Theorem Prover in Mathematica

Edmund Clarke
Xudong Zhao
Journal / Anthology

Lecture Notes in Artificial Intelligence
Year: 1992
Volume: 607
Page range: 761-765

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.

*Applied Mathematics > Computer Science
*Mathematics > Foundations of Mathematics > Logic
Related items

*Analytica: A Theorem Prover for Mathematica   [in Articles]