Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan

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 Ramanujan''s 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 Mathematica, that can prove all the challenge problems completely automatically. The axioms and inference rules for constructing the proofs are also briefly discussed.