Skip to main content
SpringerLink
Log in

Observations on ATP

  • Chapter
Book cover Computation, Logic, Philosophy

Part of the book series: Mathematics and its Application (China Series) ((MACA,volume 2))

  • 409 Accesses

Abstract

If we compare calculating with proving, four differences strike the eye: (1) Calculations deal with numbers; proofs, with propositions. (2) Rules of calculation are generally more exact than rules of proof. (3) Procedures of calculation are usually terminating (decidable, recursive) or can be made so by fairly well-developed methods of approximation. Procedures of proof, however, are often nonterminating (undecidable or nonrecursive, though recursively enumerable), indeed incomplete in the case of number theory or set theory, and we do not have a clear conception of approximate methods in theorem-proving. (4) We possess efficient calculating procedures, while with proofs it frequently happens that even in a decidable theory, the decision method is not practically feasible. Although shortcuts are the exception in calculations, they seem to be the rule with proofs in so far as intuition, insight, experience, and other vague and not easily imitable principles are applied. Since the proof procedures are so complex or lengthy, we simply cannot manage unless we somehow discover peculiar connections in each particular case.

First published in Computer Programming and Formal Systems, edited by P. Brafford and H. Hirschberg, pp 1–20. © North-Holland Publishing Company, 1963. Reproduced by permission.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ackermann, W., Solvable Cases of the Decision Problem. Amsterdam, 1954.

    MATH  Google Scholar 

  2. Goodstein, R.L., Recursive Number Theory. Amsterdam, 1957.

    MATH  Google Scholar 

  3. Péter, R., Rekursive Funktionen. 2nd edition, Budapest, 1957.

    MATH  Google Scholar 

  4. Quine, W.V., Mathematical Logic. Revised Edition, Cambridge, Mass., 1950.

    Google Scholar 

  5. Surányi, J., Reduktionstheorie des Entscheidungsproblems. Budapest, 1959.

    MATH  Google Scholar 

  6. Davis, M. and H. Putnam, “A Computing Procedure for Quantification Theory.” Journal ACM, vol.7 (1960), pp.201–215.

    Article  MathSciNet  MATH  Google Scholar 

  7. Dunham, B., R. Fridshal, G.L. Sward, “A Nonheuristic Program for Proving Elementary Logical Theorems.” Proceedings I.C.I.F., Paris, 1959 (pub. 1960), p.284.

    Google Scholar 

  8. Dunham, J. H. North, Exploratory Mathematics by Machine (to be published in a symposium volume at Perdue University).

    Google Scholar 

  9. Gelernter, H., “Realization of a Geometry Theorem Proving Machine.” Proceedings I.C.I.F., Paris, 1959 (pub.1960).

    Google Scholar 

  10. Gilmore, P.C., “A Proof Method for Quantification Theory: Its Justification and Realization.” IBM Journal, vol.4 (1960), pp.28–35.

    Article  MathSciNet  MATH  Google Scholar 

  11. Herbrand, J., Recherches sur la Théorie de la Démonstration. Warsaw, 1930.

    MATH  Google Scholar 

  12. Herbrand, J., “Sur le Probléme Fondamental de la Logique Mathématique.” CR, Warsaw, No.24 (1931).

    Google Scholar 

  13. Hintikka, K. J. J., “Vicious Circle Principle and the Paradoxes.” Journal of Symbolic Logic, vol.22 (1957), pp.245–248.

    Article  MathSciNet  MATH  Google Scholar 

  14. Minsky, M., “Steps Toward Artificial Intelligence.” Proceedings I.R.E., vol.49 (1961), pp.8–30.

    Article  MathSciNet  Google Scholar 

  15. Newell, A., J.C. Shaw, H.A. Simon, “Empirical Explorations of the Logical Theory Machine: A Case Study in Heuristics,” Proceedings W.J.C.C., (1957), pp.218–230.

    Google Scholar 

  16. Prawitz, D., H. Prawitz, N. Voghera, “A Mechanical Proof Procedure and its Realization in an Electronic Computer.” Journal ACM, vol.7 (1960), pp.102–128.

    Article  MathSciNet  MATH  Google Scholar 

  17. Prawitz, D., H. Prawitz, N. Voghera, “An Improved Proof Procedure.” Theoria, vol.26 (1960), pp.102–139.

    Article  MathSciNet  MATH  Google Scholar 

  18. Robinson, A., “On the Mechanization of the Theory of Equations.” Bulletins of the Research Council of Israel, vol.9F, No.2 (Nov. 1960), pp.47–70.

    Google Scholar 

  19. Shepherdson, J., The Principle of Induction in Free Variable Systems of Number Theory. (Lecture at the Polish Academy, Spring, 1961, to be published).

    Google Scholar 

  20. Skolem, Th., “Begründung der elementaren Arithmetik.” Kristiania, 1923, 38 pp.

    Google Scholar 

  21. Wang, H., “A Variant to Turing’s Theory of Computing Machines.” Journal ACM, vol.4 (1957), pp.63–92.

    Article  Google Scholar 

  22. Wang, H., “Toward Mechanical Mathematics,” IBM Journal, vol.4 (1960), pp.2–22.

    Article  MATH  Google Scholar 

  23. Wang, H., “Proving Theorems by Pattern Recognition.” Part I, Communications ACM, vol.3 (1960), pp.220–234;

    Article  MATH  Google Scholar 

  24. Wang, H., “Proving Theorems by Pattern Recognition.” Part II, Bell System Technical Journal, vol.40 (1961), pp.1–41.

    Google Scholar 

  25. W. Ackermann, Solvable cases of the decision problem, North-Holland, Amsterdam, 1954.

    MATH  Google Scholar 

  26. N. Bourbaki, Éléments de mathématique, Hermann, Paris.

    Google Scholar 

  27. J.R. Büchi, Turing machines and the Entscheidung sproblem, Notices Amer. Math. Soc, 8(1961), 354.

    Google Scholar 

  28. M. Davis and H. Putnam, A computing procedure for quanification theory, J. Assoc. Comput. Mach., 7(1960), 201–215.

    MathSciNet  MATH  Google Scholar 

  29. B. Dunham, Theorem testing by computer. Lecture at Harvard Computation Laboratory, February 15, 1962.

    Google Scholar 

  30. B. Dunham, R. Fridshal and G. L. Sward, A nonheuristic program for proving elementary logical theorems, Proc. Internat. Conf. on Information Processing, UNESCO, Paris, 1959 (published in 1960), p.284.

    Google Scholar 

  31. B. Dunham, R. Fridshal and J.H. North, Exploratory mathomatics by machine, Proc. Sympos, Decision and Information Processes, Macmillan, New York, 1961.

    Google Scholar 

  32. B. Dunham and J. H. North, Theorem testing by computer, Sympos. Math. Theory Automata, Brooklyn Polytechnic Institute, Brooklyn, N.Y., April, 1962.

    Google Scholar 

  33. G. Frege, Grundgesetze der Arithmetik, Jena, 1893 and 1903.

    MATH  Google Scholar 

  34. J. Friedman, A semi-decision procedure for the functional calculus, J. Assoc. Comput. Mach., 10(1963), 1–24.

    MathSciNet  MATH  Google Scholar 

  35. H. Gelernter, Realization of a geometry theorem proving machine, Proc. Internat. Conf. on Information Processing, UNESCO, Paris, 1959 (published in 1960).

    Google Scholar 

  36. P. C. Gilmore, A proof method for quantification theory: its justification and realization, IBM J. 4(1960), 28–35.

    Article  MathSciNet  MATH  Google Scholar 

  37. H. Grassmann, Lehrbuch der Arithmetik, Berlin, 1861.

    Google Scholar 

  38. J. Herbrand, Recherches sur la théorie de la démonstration, Warsaw, 1930.

    MATH  Google Scholar 

  39. A. S. Kahr, Edward F. Moore and Hao Wang, Entscheidungsproblem reduced to the AEA case, Proc. Nat. Acad. Sci. U.S.A., 48 (1962), 365–377.

    Article  MathSciNet  MATH  Google Scholar 

  40. M. Minsky, Steps toward artificial intelligence, Proc. I.R.E., 49(1961), 8–30.

    Article  MathSciNet  Google Scholar 

  41. A. Newell, J. C. Shaw and H. A. Simon, Empirical explorations of the logical theory machine: a case study in heuristics, Proc. Western Joint Computer Conference, IRE, New York, pp.218–230, 1957.

    Google Scholar 

  42. G. Peano, Formulaire de mathématiques, Turin, 1894–1908.

    Google Scholar 

  43. D. Prawitz, H. Prawitz and N. Voghera, A mechanical proof procedure and its realization in an electronic computer, J. Assoc. Comput. Mach., 7(1960), 102–128.

    MathSciNet  MATH  Google Scholar 

  44. D. Prawitz, An improved proof procedure, Theoria 26(1960), 102–139.

    Article  MathSciNet  MATH  Google Scholar 

  45. W. V. Quine, Mathematical logic, Harvard Univ. Press, Cambridge, Mass., 1951.

    MATH  Google Scholar 

  46. A. Robinson, On the mechanization of the theory of equations, Bull. Res. Council Israel (9F) No.2 (1960), 47–70.

    Google Scholar 

  47. J. B. Rosser, Logic for mathematicians, McGraw-Hill, New York, 1953.

    MATH  Google Scholar 

  48. Th. Skolem, Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich, 38 pp., Skr. Videnskapsselskapet i Kristiania, I. Mat. -Naturv. Klasse No.6, 1923.

    Google Scholar 

  49. J. Suranyi, Reduktionstheorie des Entscheidungsproblems, Ungarischen Akademie, Budapest, 1959.

    MATH  Google Scholar 

  50. S. M. Ulam, A collection of mathematical problems, Interscience, New York, 1960.

    MATH  Google Scholar 

  51. H. Wang, Circuit synthesis by solving sequential Boolean equations, Z. Math. Logik Grundlagen Math. 5(1959), 291–322.

    Article  MathSciNet  MATH  Google Scholar 

  52. H. Wang, Ordinal numbers and predicative set theory, Z. Math. Logik Grundlagen 5(1959), 216–239.

    Article  MATH  Google Scholar 

  53. H. Wang, Toward mechanical mathematics, IBM Journal 4(1960), 2–22.

    Article  MATH  Google Scholar 

  54. H. Wang, Proving theorems by pattern recognition. I, Comm. ACM 3(1960), 220–234

    Article  MATH  Google Scholar 

  55. II, Bell System Tech. J., 40(1961), 1–41.

    Google Scholar 

  56. A. N. Whitehead and B. Russell, Principia mathematica, Cambridge Univ. Press, Cambridge, 1910–1913.

    Google Scholar 

  57. S. Aanderaa, A Deterministic Proof Procedure (manuscript), Harvard, May 1964.

    Google Scholar 

  58. D. G., Bobrow, “Natural Language Input for a Computer Problem-Solving System,” Ph.D. thesis, MIT, September, 1964.

    Google Scholar 

  59. W. S. Brown, The ALPAK System, MM-63–1214–3, Bell Laboratories, April 1963.

    Google Scholar 

  60. T. Chinlund, M. Davis, P. G. Hinman and D. McIlroy, Theorem-Proving by Machine, Bell Laboratories, Spring 1964.

    Google Scholar 

  61. G. E. Collins, Computational Reductions in Tarski’s Decision Method for Elementary Algebra, IBM Corporation, Yorktown Heights, July 1962.

    Google Scholar 

  62. M. Davis, and H. Putnam, “A Computing Procedure for Quantification Theory,” Journal of the Association for Computing Machinery, 7, 1960. pp.201–215.

    MathSciNet  MATH  Google Scholar 

  63. M. Davis, G. Logemann and D. Loveland, “A Machine Program for Theorem-Proving,” Communications of the Association for Computing Machinery, 5, 1962. pp.394–397.

    Article  MathSciNet  MATH  Google Scholar 

  64. M. Davis, “Eliminating the Irrelevant from Mechanical Proofs,” Proceedings of Symposium in Applied Mathematics, American Mathematical Society, v. 15, 1963.

    Google Scholar 

  65. B. Dreben, P. Andrews and S. Aanderaa, “False Lemmas in Herbrand,” Bulletin of the American Mathematical Society, v. 69, 1963. pp.699–706.

    Article  MathSciNet  MATH  Google Scholar 

  66. B. Dreben, and H. Wang, A Refutation Procedure and Its Model-Theoretic Justification (manuscript), Harvard University, November 1964.

    Google Scholar 

  67. B. Dunham, R. Fridshal and G. L. Sward, “A Nonheuristic Program for Proving Elementary Logical Theorems,” Proceedings of the First International Conference on Information Processing, Paris, 1959; pub. Unesco, 1960. pp.282–285.

    Google Scholar 

  68. B. Dunham. R. Fridshal and J. North, Exploratory Mathematics by Machine, Recent Development in Information and Decision Processes, Robert E. Machol and Paul Grey (eds.), Mac-Millan, N. Y., 1962. (Proceedings of a Symposium at Purdue University, April 1961.)

    Google Scholar 

  69. B. Dunham and J. H. North, “Theorem Testing by Computer,” paper presented April 24–26, 1962, Mathematical Theory of Automata, Polytechnic Press, Brooklyn, 1963. pp.173–177.

    Google Scholar 

  70. J. Friedman, “A Semidecision Procedure for the Functional Calculus,” Journal of the Association for Computing Machinery, v. 10, 1963. pp.1–24.

    MathSciNet  MATH  Google Scholar 

  71. J. Friedman, “A Computer Program for a Solvable Case of the Decision Problem,” Journal of the Association for Computing Machinery, v. 10, 1963. pp.348–356.

    MathSciNet  MATH  Google Scholar 

  72. J. Friedman, A New Decision Procedure in Logic and Its Computer Realization, Ph.D. thesis, Harvard University, September 1964.

    Google Scholar 

  73. H. Gelernter, J.R. Hanson and D. W. Loveland, “Empirical Investigations of the Geometry Theorem Machine,” Proceedings of the Western Joint Computer Conference, San Francisco, 1960. pp.143–149.

    Google Scholar 

  74. P. C. Gilmore, “A Proof Method for Quantification Theory—Its Justification and Realization,” IBM Journal of Research and Development, v. 4, 1960. pp.28–35.

    Article  MathSciNet  MATH  Google Scholar 

  75. P. C. Gilmore, An Examination of the Geometry Theorem Machine, IBM Corporation, Yorktown Heights, April 1962.

    Google Scholar 

  76. J. Herbrand, “Recherches sur la Theorie de la Demonstration,” Travaux de la Société des Sciences et des Lettres de Varsovie, C1. III, Math. Phys., v. 33, 1930.

    MATH  Google Scholar 

  77. S. Kanger, “A Simplified Proof Method for Elementary Logic,” Computer Programming and Formal Systems, P. Braffort and D. Hirschberg (eds.), North-Holland Publishing Co., Amsterdam, 1963. pp.87–94 (Proceedings of Seminars at Blaricum, Holland in 1961).

    Chapter  Google Scholar 

  78. S. Kuroda, “An Investigation of the Logical Structure of Mathematics XIII, A Method of Programming Proofs in Mathematics for Electronic Computers,” Magoya Mathematical Journal, v. 16, 1960. pp.195–203.

    MATH  Google Scholar 

  79. D. H. Lehmer, “Some High Speed Logic,” Proceedings Symposium in Applied Mathematics, American Mathematical Society, v.15, 1963.

    Google Scholar 

  80. J. McCarthy, “Computer Programs for Checking Mathematical Proofs,” AMS Symposium on Recursive Function Theory, New York, April 1961.

    Google Scholar 

  81. A. Newell, J. C. Shaw and H. A. Simon, Empirical Explorations of the Logic Theory Machine,” Proceedings of the Western Joint Computer Conference, 1957.

    Google Scholar 

  82. A. Newell, and J. C. Shaw, A Variety of Intelligent Learning in a General Problem Solver, in Self-Organizing Systems, Marshall C. Yovits and Scott Cameron (eds.), New York, Pergamon Press, 1960. pp.153–189.

    Google Scholar 

  83. D. Prawitz, H. Prawitz and N. Voghera, “A Mechanical Proof Procedure and its Realization in an Electronic Computer,” Journal of the Association for Computing Machinery, v. 7, 1960. pp.102–128.

    MathSciNet  MATH  Google Scholar 

  84. D. Prawitz, “An Improved Proof Procedure,” Theoria (a Swedish Journal of Philosophy and Psychology), v. 26, 1960. pp.102–139. (Widener, Phil 29–27(5W.))

    MathSciNet  MATH  Google Scholar 

  85. A. Robinson, “On the Mechanization of the Theory of Equations,” Bulletin of the Research Council of Israel, 9F, 1960. pp.47–70.

    Google Scholar 

  86. A. Robinson, “A Basis for the Mechanization of the Theory of Equations,” Computer Programming

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rockefeller University, New York, USA

    Professor Hao Wang (Famous Mathematical Logician, Mathematician and Philosopher)

Authors
  1. Professor Hao Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1963 North-Holland Publishing Company

About this chapter

Cite this chapter

Wang, H. (1963). Observations on ATP. In: Computation, Logic, Philosophy. Mathematics and its Application (China Series), vol 2. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-2356-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-94-009-2356-0_7

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-010-7561-9

  • Online ISBN: 978-94-009-2356-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation