Skip to main content
SpringerLink
Log in

Automated Theorem Proving 1965–1970

  • Chapter
Automation of Reasoning

Part of the book series: Symbolic Computation ((1064))

Abstract

In this article we give a critical history of automated theorem proving from 1965 through 1970. By evaluating the contributions of the period, we provide a guide to a study of the field during its development. In order to differentiate between that work which turned out to be significant and that which had lesser impact, we occasionally rely of necessity on developments occurring after 1970. Since we confine our attention to automated theorem proving, certain work in logic occurring in the period in question is ignored. For example, various studies on decidability and complexity are excluded from comment because they are not directly germane. In addition to providing a critique, we have the secondary objective of giving a tutorial. We provide sufficient information and definition to permit one to read this article with minimal recourse to the literature. In this regard we often replace the very rigorous treatment of a concept by a more intuitive description.

The Applied Mathematical Sciences Research Program (KC-04-02) of the Office of Energy Research of the U. S. Department of Energy under contract W-31-109-ENG-38 and in part by the National Science Foundation under grant number MCS-7913252

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

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. Allen, J. and Luckham, D., “An interactive theorem-proving program,” Machine Intelligence, Vol. 5(1970), Meltzer and Michie (eds), American Elsevier, New York, pp. 321–336.

    Google Scholar 

  2. Bibel, W. and Schreiber, J., “Proof search in a Gentzen-like system of first-order logic,” Proc. of the International Computing Symposium (1975), North Holland Publ., pp. 205–212.

    Google Scholar 

  3. Bledsoe, W. and Bruell, P., “A man-machine theorem-proving system,” Artificial Intelligence Journal, Vol. 5 (1974), pp. 51–72.

    Article  MATH  MathSciNet  Google Scholar 

  4. Chinthayamma, “Sets of independent axioms for ternary Boolean algebra,” Notices of the American Mathematical Society, Vol. 16 (1969), p. 654.

    Google Scholar 

  5. Darlington, J., “Some theorem-proving strategies based on the resolution principle,” Machine Intelligence, Vol. 2(1968), Dale and Michie (eds), American Elsevier, New York, pp. 57–71.

    Google Scholar 

  6. Davis, M. and Putnam, H., “A computing procedure for quantification theory,” J. ACM, Vol. 7 (1960), pp. 201–215.

    Article  MATH  MathSciNet  Google Scholar 

  7. Gilmore, P., “A proof method for quantification theory,” IBM Journal of Research and Development, Vol. 4 (1960), pp. 28–35.

    Article  MATH  MathSciNet  Google Scholar 

  8. Green, C., “The application of theorem proving to question-answering systems,” Ph. D thesis, AI Memo-96, Dept. of Computer Science, Stanford University, Stanford, California, June, 1969.

    Google Scholar 

  9. Green, C., “Theorem proving by resolution as a basis for question-answering systems,” Machine Intelligence, Vol. 4(1969), Meltzer and Michie (eds), American Elsevier, New York, pp. 183–205.

    Google Scholar 

  10. Guard, J., Oglesby, F., Bennett, J. and Settle, L., “Semi-automated mathematics,” J. ACM, Vol. 16 (1969), pp. 49–62.

    Article  MATH  Google Scholar 

  11. Henkin, L., “An algebraic characterization of quantifiers,” Fundamenta Mathematicae, Vol. 37 (1950), pp. 63–74.

    MATH  MathSciNet  Google Scholar 

  12. Henschen, L. and Wos, L., “Unit refutations and Horn sets,” J. ACM, Vol. 21 (1974), pp. 590–605.

    Article  MATH  MathSciNet  Google Scholar 

  13. Herbrand, J., “Recherches sur la theorie de la demonstration,” Travaux de la Societe des Sciences et des Lettres de Varsovie, Classe III Science Mathematique et Physiques, 1930.

    Google Scholar 

  14. Herbrand, J., “Investigations in proof theory,” in From Frege to Gödel: A Source Book in Mathematical Logic by J. van Heijenoort, Harvard University Press, 1967, pp. 525–581.

    Google Scholar 

  15. Kowalski, R., “The case for using equality axioms in automatic demonstration,” Proc. of the IRIA Symposium on Automatic Demonstration, Versailles, France, 1968, Springer-Verlag Publ., pp. 112–127.

    Chapter  Google Scholar 

  16. Kowalski, R., “Search strategies for theorem proving,” Machine Intelligence, Vol. 5(1970), Meltzer and Michie (eds), American Elsevier, New York, pp. 181–200.

    Google Scholar 

  17. Kuehner, D., “Some special purpose resolution systems,” Machine Intelligence, Vol. 7(1972), Meltzer and Michie (eds), American Elsevier, New York, pp. 117–128.

    Google Scholar 

  18. Lee, R., “A completeness theorem and a computer program for finding theorems derivable from given axioms,” Ph. D. thesis, U. of California, Berkeley, California, 1967.

    Google Scholar 

  19. Loveland, D., “A linear format for resolution,” Proc. of the IRIA Symposium on Automatic Demonstration, Versailles, France, 1968, Springer-Verlag Publ., pp. 147–162.

    Google Scholar 

  20. Luckham, D., “Refinement theorems in resolution theory,” AI Memo-81, AI Project, Stanford University, Stanford, California, 1969.

    Google Scholar 

  21. Marsden, E., “A note on implicative models,” Notices of the American Mathematical Society, Vol. 18 (1971), p. 89.

    Google Scholar 

  22. McCharen, J., Overbeek, R. and Wos, L., “Problems and experiments for and with automated theorem proving programs,” IEEE Transactions on Computers, Vol. C-25(1976), pp. 773–782.

    Google Scholar 

  23. McCharen, J., Overbeek, R. and Wos, L., “Complexity and related enhancements for automated theorem-proving programs,” Computers and Mathematics with Applications, Vol. 2 (1976), pp. 1–16.

    Article  MATH  Google Scholar 

  24. Nevins, A., “A human-oriented logic for automatic theorem proving,” J. ACM, Vol. 21 (1974), pp. 606–621.

    Article  MATH  MathSciNet  Google Scholar 

  25. Newel, A., Shaw, J. and Simon, H., “Empirical explorations with the logic theory machine,” Computers and Thought, Feigenbaum and Feldman (eds), McGraw Hill Publ., New York, 1963, pp. 109–133.

    Google Scholar 

  26. Norton, L., “Experiments with a heuristic theorem-proving program for predicate calculus with equality,” Heuristics Lab., Div. of Computer Research and Technology, National Institute of Health, Bethesda, Maryland, 1971.

    Google Scholar 

  27. Overbeek, R., “An implementation of hyper-resolution,” Computers and Mathematics with Applications, Vol. 1 (1975), pp. 201–214.

    Article  MATH  MathSciNet  Google Scholar 

  28. Peterson, J., “Shortest single axioms for the equivalential calculus,” Notre Dame Journal of Formal Logic, Vol. 17 (1976), pp. 267–271.

    Article  MATH  MathSciNet  Google Scholar 

  29. Quinlan, J. and Hunt, E., “A formal deductive problem-solving system,” J. ACM, Vol. 15 (1968), pp. 625–646.

    Article  MATH  Google Scholar 

  30. Robinson, G. and Wos, L., “Paramodulation and theorem proving in first-order theories with equality,” Machine Intelligence, Vol. 4(1969), Meltzer and Michie (eds), American Elsevier, New York, pp. 135–150.

    Google Scholar 

  31. Robinson, J., “A machine-oriented logic based on the resolution principle,” J. ACM, Vol. 12 (1965), pp. 23–41.

    Article  MATH  Google Scholar 

  32. Robinson, J., “Automatic deduction with hyper-resolution,” International Journal of Computer Mathematics, Vol. 1 (1965), pp. 227–234.

    MATH  Google Scholar 

  33. Robinson, J., “A review of automatic theorem proving,” Proc. of the Symposia in Applied Mathematics, Vol. 19(1967), American Mathematical Society, Providence, Rhode Island, pp. 1–18.

    Google Scholar 

  34. Skolem, T., “Uber die mathematische logic,” Norsk Matematisk Tidskrift, Vol. 10 (1928), pp. 125–142.

    Google Scholar 

  35. Slagle, J., “Automatic theorem proving with renamable and semantic resolution,” J. ACM, Vol. 14 (1967), pp. 687–697.

    Article  MATH  MathSciNet  Google Scholar 

  36. Slagle, J. and Bursky, P., “Experiments with a multipurpose, theorem-proving heuristic program,” J. ACM, Vol. 15 (1968), pp. 85–99.

    Article  MATH  Google Scholar 

  37. Veenker, G., “Beweisverfahren für die predikatenlogic,” Computing, Vol. 2 (1967), pp. 263–283.

    Article  MATH  MathSciNet  Google Scholar 

  38. Winker, S. and Wos, L., “Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra,” Proc. of the Eighth International Symposium on Multiple-valued Logic, Rosemont, Illinois, 1978, IEEE and ACM Publ., pp. 251–256.

    Google Scholar 

  39. Winker, S., Wos, L. and Lusk, E., “Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I,” to appear in Mathematics of Computation.

    Google Scholar 

  40. Winker, S., “Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions,” to appear in J. ACM.

    Google Scholar 

  41. Wojciechowski, W. and Wojcik, A., “Multiple-valued logic design by theorem proving,” Proc. of the Ninth International Symposium on Multiple-valued Logic, Bath, England, 1979.

    Google Scholar 

  42. Wos, L., Robinson, G. and Carson, D., “Some theorem-proving strategies and their implementation,” Argonne National Laboratory, Technical Memo 72, Argonne, Illinois, 1964.

    Google Scholar 

  43. Wos, L., Carson, D. and Robinson, G., “The unit preference strategy in theorem proving,” Proc. of the Fall Joint Computer Conference, 1964, Thompson Book Company, New York, pp. 615–621.

    Google Scholar 

  44. Wos, L., Carson, D and Robinson, G., “Efficiency and completeness of the set-of-support strategy in theorem proving,” J. ACM, Vol. 12 (1965), pp. 536–541.

    Article  MATH  MathSciNet  Google Scholar 

  45. Wos, L., Robinson, G., Carson, D. and Shalla, L., “The concept of demodulation in theorem proving,” J. ACM, Vol. 14 (1967), pp. 698–704.

    Article  MATH  Google Scholar 

  46. Wos, L., Winker, S., Veroff, R., Smith, B. and Henschen, L., “Questions concerning possible shortest single axioms in equivalential calculus: an application of automated theorem proving to infinite domains,” in preparation.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Argonne National Laboratory, Argonne, Illinois, 60439, USA

    L. Wos & L. Henschen

  2. Northwestern University, Evanston, Illinois, 60201, USA

    L. Wos & L. Henschen

Authors
  1. L. Wos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. L. Henschen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik I, Universität Karlsruhe, Postfach 6380, D-7500, Karlsruhe, West Germany

    Jörg H. Siekmann

  2. Department of Information Science, Victoria University, Wellington, New Zealand

    Graham Wrightson

Rights and permissions

Reprints and permissions

Copyright information

© 1983 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Wos, L., Henschen, L. (1983). Automated Theorem Proving 1965–1970. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-81955-1_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-81957-5

  • Online ISBN: 978-3-642-81955-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation