Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan
Abstract
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 Mathematical that can prove all the challenge problems completely automatically. The axioms and inference rules for constructing the proofs are also briefly discussed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1994
- Accession Number
- ADA278899
Entities
People
- Edmund M. Clarke
- Xudong Zhao
Organizations
- Carnegie Mellon University