Advertisement

A Biographical Sketch of W. W. Bledsoe

  • Anne Olivia Boyer
  • Robert S. Boyer
Part of the Automated Reasoning Series book series (ARSE, volume 1)

Abstract

W. W. Bledsoe is a major figure in the evolution of the new scientific field artificial intelligence and one of the founding fathers of the related scientific field automated reasoning. Into the following biographical sketch of Bledsoe we weave personal, educational, historical, social, and scientific commentary. At the time we write, Bledsoe is an active contributor to science and education at the University of Texas at Austin. We hope that our fondness for Bledsoe, whom we have known well for twenty-three years, has not clouded our assessment of his many achievements. We are certain that we have failed to treat adequately many aspects of Bledsoe’s life prior to our first meeting him in 1966, and sadly fear that lack of space and lack of investigative effort cause us to omit quite a few interesting aspects of his career since then. We hope, however, that this short sketch of Bledsoe will please his friends and perhaps provide some useful information for a future biographer or historian of science.

Keywords

Facial Recognition American Mathematical Society Product Measure Theorem Prove Automate Reasoning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Robert Anderson (1970): Completeness Results for E-Resolution. Proc. AFIPS 1970 Spring Joint Computer Conf., 36, 653–6.Google Scholar
  2. [2]
    Robert Anderson (1970): Some Theoretical Aspects of Automatic Theorem Proving. Ph. D. Dissertation, University of Texas at Austin.Google Scholar
  3. [3]
    A. Michael Ballantyne and W. W. Bledsoe (1977): Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques. Journal of the Association for Computing Machinery 24(3), 353–374.MathSciNetzbMATHCrossRefGoogle Scholar
  4. [4]
    A. M. Ballantyne and W. W. Bledsoe (1982): On Generating and Using Examples in Proof Discovery. In: J. Hayes and D. Michie, eds.: Machine Intelligence 10. Harwood: Chichester. 3–39.Google Scholar
  5. [5]
    W. W. Bledsoe (1952): Neighborly Functions. Proceedings of the American Mathematical Society 3(1), 144–115.CrossRefGoogle Scholar
  6. [6]
    W. W. Bledsoe (1952): Some Aspects of Covering Theory. Proceedings of the American Mathematical Society 3(5), 804–812.MathSciNetzbMATHCrossRefGoogle Scholar
  7. [7]
    W. W. Bledsoe, M. J. Norris, and G. F. Rose (1954): On a Differential Inequality. Proceedings of the American Mathematical Society 5(6), 934–939.MathSciNetzbMATHCrossRefGoogle Scholar
  8. [8]
    W. W. Bledsoe, et al. (1955): A Systems Study Comparing Various Fuzing Possibilities for the Atlas ICBM. Sandia Corporation Technical Memorandum 155–55–51, Ref. Sym: 1923 (266), August 4, 1955.Google Scholar
  9. [9]
    W. W. Bledsoe and A. P. Morse (1955): Product Measures. Transactions of the American Mathematical Society 79(1), 173–215.MathSciNetzbMATHCrossRefGoogle Scholar
  10. [10]
    W. W. Bledsoe (1957): Program for Computing Probabilities of Fallout from a Large-Scale Thermonuclear Attack, SC-4109 (TR) Systems Analysis, Sandia Corporation. Available from the Office of Technical Services, Department of Commerce, Washington, D. C.Google Scholar
  11. [11]
    W. W. Bledsoe and I. Browning (1959): Pattern Recognition and Reading by Machine. Proceedings of the Eastern Joint Computer Conference, 225–232.Google Scholar
  12. [12]
    W. W. Bledsoe (1961): Further Results on the N-tuple Pattern Recognition Method. IRE Transactions on Electronic Computers EC-10(1), 96–97.Google Scholar
  13. [13]
    W. W. Bledsoe (1961): A Basic Limitation on the Speed of Digital Computers. IRE Transactions on Electronic Computers EC-10(3), 530.CrossRefGoogle Scholar
  14. [14]
    W. W. Bledsoe (1961): Lethally Dependent Genes Using Instant Selection. Technical Report PRI 1, Panoramic Research Inc.Google Scholar
  15. [15]
    W. W. Bledsoe (1961): The Use of Biological Concepts in the Analytical Study of Systems. Technical report PRI 2, Panoramic Research, Inc. A talk presented to the Operations Research Society of America, National Meeting, San Francisco, CA, November 10, 1961.Google Scholar
  16. [16]
    W. W. Bledsoe and C. L Bisson (1962): Improved Memory-Matrices for the N-tuple Pattern Recognition Method. IRE Transactions on Electronic Computers EC-11, 414–415.CrossRefGoogle Scholar
  17. [17]
    W. W. Bledsoe and A. P. Morse (1963): A Topological Measure Construction. Pacific Journal of Mathematics 13(4), 1067–1084.MathSciNetzbMATHGoogle Scholar
  18. [18]
    W. W. Bledsoe et al. (1964): Facial Recognition Project Report. Technical report PRI 10, Panoramic Research, Inc.Google Scholar
  19. [19]
    W. W. Bledsoe (1965): The Model Method in Facial Recognition. Technical Report PRI 15, Panoramic Research, Inc. Not publicly available.Google Scholar
  20. [20]
    W. W. Bledsoe (1965): Two-dimensional Terrain Following a “Back and Fill” Method. Technical report PRI 23, Panoramic Research, Inc.Google Scholar
  21. [21]
    W. W. Bledsoe (1965): Simulation of Three-Dimensional Navigation. Technical report PRI 24, Panoramic Research, Inc.Google Scholar
  22. [22]
    W. W. Bledsoe and Helen Chan (1965): A Man-Machine Facial Recognition System—Some Preliminary Results. Technical report PRI 19A, Panoramic Research, Inc. Not publicly available.Google Scholar
  23. [23]
    W. W. Bledsoe (1966): Some Results on Multicategory Pattern Recognition. Journal of the Association for Computing Machinery 13(2), 304–316.zbMATHCrossRefGoogle Scholar
  24. [24]
    W. W. Bledsoe (1966): Man-machine Facial Recognition. Technical Report PRI 22, Panoramic Research, Inc.Google Scholar
  25. [25]
    W. W. Bledsoe and E. J. Gilbert (1967): Automatic Theorem Proof-Checking in Set Theory—A Preliminary Report. Research Report SCRR-67–525. Sandia Laboratories.Google Scholar
  26. [26]
    W. W. Bledsoe (1968): Semiautomatic Facial Recognition. Technical Report SRI Project 6693. Stanford Research Institute, Menlo Park, California. Not publicly available.Google Scholar
  27. [27]
    W. W. Bledsoe (1970): An Inequality about Complex Numbers. American Mathematical Monthly 77(2), 180–182.MathSciNetzbMATHCrossRefGoogle Scholar
  28. [28]
    R. Anderson and W. W. Bledsoe (1970): A Linear Format for Resolution with Merging and a New Technique for Establishing Completeness. Journal of the Association for Computing Machinery 17, 525–534.MathSciNetzbMATHCrossRefGoogle Scholar
  29. [29]
    W. W. Bledsoe (1971): Splitting and Reduction Heuristics in Automatic Theorem Proving. Artificial Intelligence 2, 55–77.zbMATHCrossRefGoogle Scholar
  30. [30]
    W. W. Bledsoe and C. E. Wilks (1972): On Borel Product Measures. Pacific Journal of Mathematics 42(3), 569–579.MathSciNetzbMATHGoogle Scholar
  31. [31]
    W. W. Bledsoe, R. S. Boyer, and W. H. Henneman (1972): Computer Proofs of Limit Theorems. Artificial Intelligence 3, 27–60.MathSciNetzbMATHCrossRefGoogle Scholar
  32. [32]
    R. H. Bing, W. W. Bledsoe, and R. D. Mauldin (1974): Sets Generated by Rectangles. Pacific Journal of Mathematics 51(1), 27–36.MathSciNetzbMATHGoogle Scholar
  33. [33]
    W. W. Bledsoe and Peter Bruell (1974): A Man-Machine Theorem-Proving System. Artificial Intelligence 5, 51–72.MathSciNetzbMATHCrossRefGoogle Scholar
  34. [34]
    W. W. Bledsoe (1977): Non-resolution Theorem Proving. Artificial Intelligence 9, 1–35.MathSciNetzbMATHCrossRefGoogle Scholar
  35. [35]
    W. W. Bledsoe and Mabry Tyson (1977): Typing and Proof by Cases in Program Verification. In: D. Michie and E. W. Elcock, eds.: Machine Intelligence 8. Chichester: Horwood. 30–51.Google Scholar
  36. [36]
    W. W. Bledsoe (1979): A Maximal Method for Set Variables in Automatic Theorem-proving. In: J. E. Hayes, D. Michie, and L. I. Mikulich, eds.: Machine Intelligence 9. Chichester: Horwood. 55–100.Google Scholar
  37. [37]
    W. W. Bledsoe and Mabry Tyson (1979): Conflicting Bindings and Generalized Substitutions. Proceedings of the Fourth International Workshop on Automated Deduction.Google Scholar
  38. [38]
    W. W. Bledsoe and Larry M. Hines (1980): Variable Elimination and Chaining in a Resolution-Based Prover for Inequalities. Proceedings of the 5th Conference on Automated Deduction, Les Arcs, France, (eds. W. Bibel and R. Kowalski). Springer, 70–87.Google Scholar
  39. [39]
    W. W. Bledsoe (1983): Using Examples to Generate Instantiations of Set Variables. Proceedings of the Eigth International Joint Conference on Artificial Intelligence, 892–901.Google Scholar
  40. [40]
    W. W. Bledsoe and D. W. Loveland, eds. (1984): Automated Theorem Proving: After 25 years (Contemporary Mathematics Volume 29). Providence, Rhode Island: American Mathematical Society.zbMATHGoogle Scholar
  41. [41]
    W. W. Bledsoe (1984): Some Automatic Proofs in Analysis. In: [40]. 89–118.Google Scholar
  42. [42]
    W. W. Bledsoe (1986): I Had a Dream: AAAI Presidential Address, 19 August 1985. The AI Magazine 7(1), 57–61.Google Scholar
  43. [43]
    W. W. Bledsoe, K. Kunen, and R. Shostak (1985): Completeness Results for Inequality Provers. Artificial Intelligence Journal 27, 255–288.MathSciNetzbMATHCrossRefGoogle Scholar
  44. [44]
    W. W. Bledsoe and L. J. Henschen (1985): What is Automated Theorem Proving? Journal of Automated Reasoning 1, 23–28.MathSciNetGoogle Scholar
  45. [45]
    W. W. Bledsoe (1986): Some Thoughts on Proof Discovery. Proceedings of the 1986 Symposium on Logic Programming, Salt Lake City, 2–10. Also Technical Report AI-208–86. Microelectronics and Computer Technology Corporation, Austin, Texas.Google Scholar
  46. [46]
    W. W. Bledsoe and T. C. Wang (1987): Hierarchical Deduction. Journal of Automated Reasoning 3, 35–77.MathSciNetzbMATHCrossRefGoogle Scholar
  47. [47]
    W. W. Bledsoe and R. Hodges (1988): A Survey of Automated Deduction. In: H. Shrobe, ed.: Exploring Artificial Intelligence, Survey of Talks from the National Conference on Artificial Intelligence, Seattle, 1987. 483–543.Google Scholar
  48. [48]
    R. S. Boyer (1971): Locking: A Restriction of Resolution. Ph. D. Dissertation, University of Texas at Austin.Google Scholar
  49. [49]
    R. S. Boyer and J. S. Moore (1979): A Computational Logic. New York: Academic Press.zbMATHGoogle Scholar
  50. [50]
    R. S. Boyer and J. S. Moore (1988): A Computational Logic Handbook. New York: Academic Press.zbMATHGoogle Scholar
  51. [51]
    C. Chang and R. Lee (1973): Symbolic Logic and Mechanical Theorem-Proving. New York: Academic Press.zbMATHGoogle Scholar
  52. [52]
    D. I. Good, R. L. London, and W. W. Bledsoe (1975): An Interactive Program Verification System, IEEE Transactions on Software Engineering 1(1), 59–67.CrossRefGoogle Scholar
  53. [53]
    D. I. Good, Ann E. Siebert, and Lawrence M. Smith (1982): Message Flow Modulator—Final Report, Institute for Computing Science and Computer Applications, University of Texas at Austin, ICSCA-CMP34.Google Scholar
  54. [54]
    D. I. Good (1985): Mechanical Proofs about Computer Programs. In: C. A. R. Hoare and J. C. Shepherdson, eds.: Mathematical Logic and Programming Languages. Prentice-Hall. 55–75.Google Scholar
  55. [55]
    Dallas Lankford (1972): Equality Atom Term Locking. Ph. D. Dissertation. University of Texas at Austin.Google Scholar
  56. [56]
    James B. Morris (1969): A Proof Procedure for the First Order Predicate Calculus with Equality. Ph. D. Dissertation. University of Texas at Austin.Google Scholar
  57. [57]
    James B. Morris (1969): E-Resolution: Extension of Resolution to Include the Equality Relation. Proceedings of the International Joint Conference on Artificial Intelligence, Washington, D. C., 287–294.Google Scholar
  58. [58]
    A. P. Morse (1965): A Theory of Sets. New York: Academic Press.zbMATHGoogle Scholar
  59. [59]
    A. Newell, J. Shaw, and H. Simon (1957): Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristics. In: E. Feigenbaum and J. Feldman, eds.: Computers and Thought. McGraw-Hill: New York. 109–133.Google Scholar
  60. [60]
    A. Robinson (1963): Nonstandard Analysis. Amsterdam: North-Holland.Google Scholar
  61. [61]
    J. R. Shoenfield (1967): Mathematical Logic. Reading: Addison-Wesley.zbMATHGoogle Scholar
  62. [62]
    D. Simon (1990): Checking Number Theory Proofs in Natural Language. Ph. D. Dissertation. University of Texas at Austin.Google Scholar
  63. [63]
    M. Smith, A. Siebert, B. DiVitto, and D. Good (1981): A Verified Encrypted Packet Interface, Association for Computing Machinery SIG-SOFT, 6(3).Google Scholar
  64. [64]
    J. R. Ullman (1969): Experiments with the N-tuple Method of Pattern Recognition. IEEE Transactions on Computers C-18(12), 1135–1137.MathSciNetCrossRefGoogle Scholar
  65. [65]
    J. R. Ullman (1971): Reduction of the Storage Requirements of Bledsoe and Browning’s N-tuple Method of Pattern Recognition. Pattern Recognition 3, 297–306.MathSciNetCrossRefGoogle Scholar
  66. [66]
    J. R. Ullman (1973): Pattern Recognition Techniques. London: Butter-worths.Google Scholar
  67. [67]
    W. J. LeVeque (1962): Elementary Theory of Numbers. Mineola, N. Y.: Dover.zbMATHGoogle Scholar

Copyright information

© Springer Science+Business Media Dordrecht 1991

Authors and Affiliations

  • Anne Olivia Boyer
    • 1
  • Robert S. Boyer
    • 1
  1. 1.AustinUSA

Personalised recommendations