Skip to main content
SpringerLink
Log in

Automated Reasoning and Bledsoe’s Dream for the Field

  • Chapter
Book cover Automated Reasoning

Part of the book series: Automated Reasoning Series ((ARSE,volume 1))

Abstract

In one sense, this article is a personal tribute to Woody Bledsoe. As such, the style will in general be that of private correspondence. However, since this article is also a compendium of experiments with an automated reasoning program, researchers interested in automated reasoning, mathematics, and logic will find pertinent material here. The results of those experiments strongly suggest that research frequently benefits greatly from the use of an automated reasoning program. As evidence, I select from those results some proofs that are better than one can find in the literature, and focus on some theorems that, until now, had never been proved with an automated reasoning program, theorems that Hilbert, Church, and various logicians thought significant. To add spice to the article, I present challenges for reasoning programs, including questions that are still open.

This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U. S. Department of Energy, under Contract W-31-109-Eng-38.

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. H. P. Barendregt (1981): The Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland.

    MATH  Google Scholar 

  2. M. Davis and H. Putnam (1960): A Computing Procedure for Quantification Theory. J. of the ACM 7, 201–215.

    Article  MathSciNet  MATH  Google Scholar 

  3. E. Dijkstra (1989): Dijkstra’s Reply to Comments. In: A Debate on Teaching Computing Science. C. of the ACM 32(12), 1397–1414.

    Google Scholar 

  4. J. Guard, F. Oglesby, J. Bennett, and L. Settle (1969): Semi-automated Mathematics. J. of the ACM 16, 49–62.

    Article  MATH  Google Scholar 

  5. P. R. Halmos (1960): Naive Set Theory. Princeton: D. Van Nostrand Co., Inc.

    MATH  Google Scholar 

  6. L. Henkin, J. Monk, and A. Tarski (1971): Cylindric Algebras, Part I. Amsterdam: North-Holland

    Google Scholar 

  7. E. Huntington (1933): New Sets of Independent Postulates for the Algebra of Logic, with Special Reference to Whitehead and Russell’s Principia Mathematica. Trans. of the AMS 35, 274–304.

    MathSciNet  Google Scholar 

  8. J. Kalman (1978): A Shortest Single Axiom for the Classical Equivalential Calculus. Notre Dame J. Formal Logic 19(1), 141–144.

    Article  MathSciNet  Google Scholar 

  9. J. Kalman (1986): An ITP Workbook, Technical Report. ANL-86–56, Argonne National Laboratory, Argonne, Illinois.

    Google Scholar 

  10. J. Lukasiewicz (1963): Elements of Mathematical Logic. Oxford: Pergamon Press.

    MATH  Google Scholar 

  11. J. Lukasiewicz (1970): The Equivalential Calculus. In: L. Borkowski, ed.: Jan Lukasiewicz: Selected Works. Amsterdam: North-Holland.

    Google Scholar 

  12. E. Lusk, W. McCune, and R. Overbeek (1982): Logic Machine Architecture: Kernel Functions. In: D. W. Loveland, ed.: Lecture Notes in Computer Science, Vol. 138. New York: Springer-Verlag.

    Google Scholar 

  13. E. Lusk, W. McCune, and R. Overbeek (1982): Logic Machine Architecture: Inference Mechanisms. In: D. W. Loveland, ed.: Lecture Notes in Computer Science, Vol. 138. New York: Springer-Verlag.

    Google Scholar 

  14. E. Lusk and R. McFadden (1987): Using Automated Reasoning Tools: A Study of the Semigroup F2B2. Semigroup Forum 36(1), 75–88.

    Article  MathSciNet  MATH  Google Scholar 

  15. J. McCharen, R. Overbeek, and L. Wos (1976): Complexity and Related Enhancements for Automated Theorem-Proving Programs. Computers and Mathematics with Applications 2, 1–16.

    Google Scholar 

  16. W. McCune and L. Wos (1987): A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. J. Automated Reasoning 3(1), 91–108.

    Article  Google Scholar 

  17. W. McCune (1990): OTTER 2.0 Users Guide, Technical Report. ANL90/9, Argonne National Laboratory, Argonne, Illinois.

    Google Scholar 

  18. W. McCune and L. Wos (1989): The Absence and the Presence of Fixed Point Combinators, Preprint MCS—P87–0689, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois.

    Google Scholar 

  19. W. McCune (1990): Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. J. Automated Reasoning (to appear).

    Google Scholar 

  20. G. Robinson and L. Wos (1969): Paramodulation and Theorem-Proving in First-Order Theories with Equality. In: B. Meltzer and D. Michie, eds.: Machine Intelligence 4. Edinburgh: Edinburgh University Press.

    Google Scholar 

  21. J. Robinson (1965): A Machine-oriented Logic Based on the Resolution Principle. J. of the ACM 12, 23–41.

    Article  MATH  Google Scholar 

  22. J. Robinson (1988): Automatic Deduction with Hyper-Resolution. International J. Computer Mathematics 1, 227–234.

    Google Scholar 

  23. B. Smith (1988): Reference Manual for the Environmental Theorem Prover, An Incarnation of AURA. Technical Report ANL-88–2, Argonne National Laboratory, Argonne, Illinois.

    Google Scholar 

  24. R. Smullyan (1985): To Mock a Mockingbird. New York: Alfred A. Knopf.

    Google Scholar 

  25. R. Smullyan (1987): Private Correspondence.

    Google Scholar 

  26. R. Statman (1986): Private Correspondence with Raymond Smullyan.

    Google Scholar 

  27. A. Tarski (1980): Private Communication.

    Google Scholar 

  28. R. Veroff and L. Wos (1990): The Linked Inference Principle, I: The Formal Treatment. J. Automated Reasoning (to appear).

    Google Scholar 

  29. S. Winker, L. Wos, and E. Lusk (1981): Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I. Mathematics of Computation 37, 533–545.

    MathSciNet  MATH  Google Scholar 

  30. S. Winker (1982): Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions. J. of the ACM 29, 273–284.

    Article  MathSciNet  MATH  Google Scholar 

  31. L. Wos, G. Robinson, and D. Carson (1965): Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. J. of the ACM 12, 536–541.

    Article  MathSciNet  MATH  Google Scholar 

  32. L. Wos, G. Robinson, D. Carson, and L. Shalla (1967): The Concept of Demodulation in Theorem Proving. J. of the ACM 14, 698–709.

    Article  MATH  Google Scholar 

  33. L. Wos and G. Robinson (1973): Maximal Models and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving. In: W. Boone, F. Cannonito, and R. Lyndon, eds.: Word Problems: Decision Problems and the Burnside Problem in Group Theory. New York: North-Holland.

    Google Scholar 

  34. L. Wos, R. Overbeek, E. Lusk, and J. Boyle (1984): Automated Reasoning: Introduction and Applications. Englewood Cliffs, New Jersey: Prentice-Hall.

    Google Scholar 

  35. L. Wos, S. Winker, R. Veroff, B. Smith, and L. Henschen (1984): A New Use of an Automated Reasoning Assistant: Open Questions in Equivalential Calculus and the Study of Infinite Domains. Artificial Intelligence 22, 303–356.

    Article  MATH  Google Scholar 

  36. L. Wos (1987): Automated Reasoning: 33 Basic Research Problems. Englewood Cliffs, New Jersey: Prentice-Hall.

    Google Scholar 

  37. L. Wos and W. McCune (1988): Searching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report. Technical Report ANL-88–10, Argonne National Laboratory, Argonne, Illinois.

    Book  Google Scholar 

  38. L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler (1991): OTTER Experiments Pertinent to CADE-10. Technical Report ANL-89/36, Argonne National Laboratory, Argonne, Illinois.

    Google Scholar 

  39. L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler (1990): Automated Reasoning Contributes to Mathematics and Logic. In: Lecture Notes in Artificial Intelligence, Vol. 449. New York: Springer-Verlag.

    Google Scholar 

  40. L. Wos, R. Overbeek, and E. Lusk (1990): Subsumption, A Sometimes Undervalued Procedure. In: J.-L. Lassez, ed.: Festschrift for J. A. Robinson (to appear).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, USA

    Larry Wos

Authors
  1. Larry Wos
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Sciences Department, University of Texas at Austin, USA

    Robert S. Boyer

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Wos, L. (1991). Automated Reasoning and Bledsoe’s Dream for the Field. In: Boyer, R.S. (eds) Automated Reasoning. Automated Reasoning Series, vol 1. Springer, Dordrecht. https://doi.org/10.1007/978-94-011-3488-0_15

Download citation

  • DOI: https://doi.org/10.1007/978-94-011-3488-0_15

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-010-5542-0

  • Online ISBN: 978-94-011-3488-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation