Automated Reasoning pp 1-29 | Cite as

# A Biographical Sketch of W. W. Bledsoe

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- [1]Robert Anderson (1970): Completeness Results for E-Resolution. Proc. AFIPS 1970 Spring Joint Computer Conf., 36, 653–6.Google Scholar
- [2]Robert Anderson (1970): Some Theoretical Aspects of Automatic Theorem Proving. Ph. D. Dissertation, University of Texas at Austin.Google Scholar
- [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]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]W. W. Bledsoe (1952): Neighborly Functions. Proceedings of the American Mathematical Society 3(1), 144–115.CrossRefGoogle Scholar
- [6]W. W. Bledsoe (1952): Some Aspects of Covering Theory. Proceedings of the American Mathematical Society 3(5), 804–812.MathSciNetzbMATHCrossRefGoogle Scholar
- [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]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]W. W. Bledsoe and A. P. Morse (1955): Product Measures. Transactions of the American Mathematical Society 79(1), 173–215.MathSciNetzbMATHCrossRefGoogle Scholar
- [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]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]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]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]W. W. Bledsoe (1961): Lethally Dependent Genes Using Instant Selection. Technical Report PRI 1, Panoramic Research Inc.Google Scholar
- [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]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]W. W. Bledsoe and A. P. Morse (1963): A Topological Measure Construction. Pacific Journal of Mathematics 13(4), 1067–1084.MathSciNetzbMATHGoogle Scholar
- [18]W. W. Bledsoe et al. (1964): Facial Recognition Project Report. Technical report PRI 10, Panoramic Research, Inc.Google Scholar
- [19]W. W. Bledsoe (1965): The Model Method in Facial Recognition. Technical Report PRI 15, Panoramic Research, Inc. Not publicly available.Google Scholar
- [20]W. W. Bledsoe (1965): Two-dimensional Terrain Following a “Back and Fill” Method. Technical report PRI 23, Panoramic Research, Inc.Google Scholar
- [21]W. W. Bledsoe (1965): Simulation of Three-Dimensional Navigation. Technical report PRI 24, Panoramic Research, Inc.Google Scholar
- [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]W. W. Bledsoe (1966): Some Results on Multicategory Pattern Recognition. Journal of the Association for Computing Machinery 13(2), 304–316.zbMATHCrossRefGoogle Scholar
- [24]W. W. Bledsoe (1966): Man-machine Facial Recognition. Technical Report PRI 22, Panoramic Research, Inc.Google Scholar
- [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]W. W. Bledsoe (1968): Semiautomatic Facial Recognition. Technical Report SRI Project 6693. Stanford Research Institute, Menlo Park, California. Not publicly available.Google Scholar
- [27]W. W. Bledsoe (1970): An Inequality about Complex Numbers. American Mathematical Monthly 77(2), 180–182.MathSciNetzbMATHCrossRefGoogle Scholar
- [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]W. W. Bledsoe (1971): Splitting and Reduction Heuristics in Automatic Theorem Proving. Artificial Intelligence 2, 55–77.zbMATHCrossRefGoogle Scholar
- [30]W. W. Bledsoe and C. E. Wilks (1972): On Borel Product Measures. Pacific Journal of Mathematics 42(3), 569–579.MathSciNetzbMATHGoogle Scholar
- [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]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]W. W. Bledsoe and Peter Bruell (1974): A Man-Machine Theorem-Proving System. Artificial Intelligence 5, 51–72.MathSciNetzbMATHCrossRefGoogle Scholar
- [34]W. W. Bledsoe (1977): Non-resolution Theorem Proving. Artificial Intelligence 9, 1–35.MathSciNetzbMATHCrossRefGoogle Scholar
- [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]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]W. W. Bledsoe and Mabry Tyson (1979): Conflicting Bindings and Generalized Substitutions. Proceedings of the Fourth International Workshop on Automated Deduction.Google Scholar
- [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]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]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]W. W. Bledsoe (1984): Some Automatic Proofs in Analysis. In: [40]. 89–118.Google Scholar
- [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]W. W. Bledsoe, K. Kunen, and R. Shostak (1985): Completeness Results for Inequality Provers. Artificial Intelligence Journal 27, 255–288.MathSciNetzbMATHCrossRefGoogle Scholar
- [44]W. W. Bledsoe and L. J. Henschen (1985): What is Automated Theorem Proving? Journal of Automated Reasoning 1, 23–28.MathSciNetGoogle Scholar
- [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]W. W. Bledsoe and T. C. Wang (1987): Hierarchical Deduction. Journal of Automated Reasoning 3, 35–77.MathSciNetzbMATHCrossRefGoogle Scholar
- [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]R. S. Boyer (1971): Locking: A Restriction of Resolution. Ph. D. Dissertation, University of Texas at Austin.Google Scholar
- [49]R. S. Boyer and J. S. Moore (1979): A Computational Logic. New York: Academic Press.zbMATHGoogle Scholar
- [50]R. S. Boyer and J. S. Moore (1988): A Computational Logic Handbook. New York: Academic Press.zbMATHGoogle Scholar
- [51]C. Chang and R. Lee (1973): Symbolic Logic and Mechanical Theorem-Proving. New York: Academic Press.zbMATHGoogle Scholar
- [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]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]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]Dallas Lankford (1972): Equality Atom Term Locking. Ph. D. Dissertation. University of Texas at Austin.Google Scholar
- [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]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]A. P. Morse (1965): A Theory of Sets. New York: Academic Press.zbMATHGoogle Scholar
- [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]A. Robinson (1963): Nonstandard Analysis. Amsterdam: North-Holland.Google Scholar
- [61]J. R. Shoenfield (1967): Mathematical Logic. Reading: Addison-Wesley.zbMATHGoogle Scholar
- [62]D. Simon (1990): Checking Number Theory Proofs in Natural Language. Ph. D. Dissertation. University of Texas at Austin.Google Scholar
- [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]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]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]J. R. Ullman (1973): Pattern Recognition Techniques. London: Butter-worths.Google Scholar
- [67]W. J. LeVeque (1962): Elementary Theory of Numbers. Mineola, N. Y.: Dover.zbMATHGoogle Scholar