DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA278899
Title:
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan
Corporate Author:
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Report Date:
1994-01-01
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 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.
Descriptive Note:
Research rept.,
Pages:
0010
Distribution Statement:
Approved for public release; distribution is unlimited.
Contract Number:
F33615-90-C-1465
Contract Number 2:
ARPA ORDER-7597
File Size:
0.34MB
