The Shunyata system

• Ammon, K. 1988a. Discovering a proof for the fixed point theorem: A case study. Proceedings of the Eighth European Conference on Artificial Intelligence, August 1–5, Munich, West Germany, pp. 613–618.

  Google Scholar 

• Ammon, K. 1988b. The automatic acquisition of proof methods. Proceedings of the Seventh National Conference on Artificial Intelligence, August 21–26, St. Paul, Minnesota, pp. 558–563.

  Google Scholar 

• Apostol, T. M. 1957. Mathematical Analysis. Reading, Mass.: Addison-Wesley.

  Google Scholar 

• Ballantyne, A. M., and Bledsoe, W. W. 1977. Automatic proofs of theorems in analysis using nonstandard techniques. Journal of the Association of Computing Machinery 24, pp. 353–374.

  Google Scholar 

• Bledsoe, W. W. 1977. Non-resolution theorem proving. Artificial Intelligence 9, pp. 1–35.

  Google Scholar 

• Kaufmann, M. 1989. DEFN-SK: An extension of the Boyer-Moore Theorem Prover to handle first-order quantifiers. Technical Report 43, Computational Logic, Inc., Austin, Texas.

  Google Scholar 

• McCharen, J. D., Overbeek, R. A., and Wos, L. A. 1976. Problems and experiments for and with automated theorem-proving programs. IEEE Transactions on Computers, Vol. C-25, 8 pp. 773–782.

  Google Scholar 

• McCune, W. W. 1990. OTTER 2.0 Users Guide. Report ANL-90/9, Argonne National Laboratory, Argonne, Illinois.

  Google Scholar 

• McCune, W. W. 1991. What's new in OTTER 2.2. Report ANL/MCS-TM-153, Argonne National Laboratory, Argonne, Illinois.

  Google Scholar 

• Shankar, N. 1987. Proof checking metamathematics. Technical Report 9, Computational Logic, Inc., Austin, Texas.

  Google Scholar 

Download references