CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
One way of building more powerful theorem provers is to use techniques from symbolic computation. The challenge problems in this paper are taken from Chapter 2 of Ramanujans Notebooks. They were selected because they are non-trivial and require the use of symbolic computation techniques. We have developed a theorem prover based on the symbolic computation system Mathematical that can prove all the challenge problems completely automatically. The axioms and inference rules for constructing the proofs are also briefly discussed.