














Inventory 
box 
96349/1 (05086932) 


Theses and dissertations 




Hines, Larry M., "Building in Axioms and Lemmas,"
1988 




Moriconi, Mark, Steven, "A System for Incrementally
Designing and Verifying Programs,"
1977 




Minor, John, t., "Proving a Subset of SecondOrder Logic
with FirstOrder Proof Procedures,"
1979 




Marinov, Vesko, G., "Maximal Clause Length Resolution,"
1973 




Wang, TieCheng, "Semantically Guided Hierarchical
Deduction and Equality Conditional Resolution,"
1986 




Tyson, William, Mabry, "APRVR: A PriorityOrdered Agenda
Theorem Provider,"
1981 




Kartha, G., Neelakantan, "A Mathematical Investigation
of Reasoning About Actions,"
1995 




Anderson, Robert, Brockett, "Some Theoretical Aspects of
Automatic Theorem Proving,"
1970 




Feng, Gouhui, "Validating Formal Specifications with
HOL,"
1994 




Morris, James, Bertram, "A Proof Procedure for the
FirstOrder Predicate Calculus with Equality,"
1969 




Boyer, Robert, S., "Locking: A Restriction of
Resolution,"
1971 (2 copies) 




Wilks, Charles, Edward, "The Regularity of a Product
Measure Using Regular Conditional Measure,"
1969 




Simon, Donald, Lee, "Checking Number Theory Proofs in
Natural Language,"
1990 




Darden, Stephen, Charles, "A Contextual Recognition
System For Formal Languages,"
1969 




Enfield, Morris, Conrad, Jr., "Automatic Chromosome
Karyotyping Using Moment Invariant Pattern Recognition,"
1968 




Duplissey, Claude, Vernon, "Theory and Applications of
Measurable Cardinals,"
1967 




Williamson, Hugh, Jackson, "A Survey of the Riemann
Stietjes Integral and Its Generalization,"
1967 




Sorensen, Villy, J., "Polytene Chromosome Processing By
Computer,"
1974 




Ulrich, John, Wade, "A Computational Theory of Planar
Imbedding,"
1968 
box 
96349/2 (05086783) 


Duke University talk,
April 13, 1992 



Report of the 1992 Mathematics and Computer Science Review
Committee, draft number 2,
November 11, 1992 



American Association for Artificial Intelligence92
workshop program; "Artificial Intelligence and Automated Program
Understanding,"
July 1216, 1992 



American Association for Artificial Intelligence92 Tenth
National Conference on Artificial Intelligence: program,
July 1216, 1992 



CADE11,
June 1519, 1992 



Mario Garcia 



American Association for Artificial Intelligence Fellows
Committee,
1991 



National Science Foundation proposal,
1992 



Institute for Information Technology and Applications,
draft,
December 5, 1991 



Cade11 refereereports,
January, 1992 



"Frontiers in Computing,"
November 1516, 1991 



John McCarthy's festschrift,
September 4, 1994 



International Institute for Effective Communication(s),
James, Rogers Fox,
Summer 1990March 1992 



International Joint Conference on Artificial Intelligence,
August 1991 



Argonne National Laboratory, Japanese/American Workshop on
Automated Reasoning,
June 25, 1991 



Oberwolfach Conference, PDK,
May 1991 



National Science Foundation,
19931996 



Interactive proofpresentation paper,
April 18, 1991 



National Science Foundation proposal,
19901993 



National Science Foundation proposal,
19911993 



National Science Foundation reports,
1990 



National Science Foundation proposal, Computer and
Computation Research Committee,
December 19881989 



Mathematics and Computer Science Division, The University
of Chicago, review,
1991 



Artificial Intelligence in software engineering,
19851989 



Canadian Institute for Advanced Research,
1990 



Kaiserslauten talk, "The Dream and Reality of Artificial
Intelligence,"
October 1989 



Computer Science 395t: class presentation,
December 1989December 1991 



International Symposium on Artificial Intelligence talk:
"Some Concerns in Automated Theorem Proving,
October 27, 1989 



CADE 10: "Some Adventures with Automated Proof Discovery
in Higher Order Logic,"
July 26, 1990 



"Artificial Intelligence: Where are We Going?"
October 26, 1988 



CADE 10 meeting program,
July 2427, 1990 



National Science Foundation proposal,
19861989 



Microelectronics and Computer Technology Corporation
transparencies 



"Expert Systems in the Marketplace,"
October 26, 1988 



International Symposium on Artificial Intelligence talks,
Monterey,
19851988 



MITREspeaker,
February 19, 1987 



First International Symposium on Artificial Intelligence,
Monterey, Mexico,
October 2528, 1988 



GTE Technology Conference, Newport, Rhode Island,
October 13, 1987 



Artificial Intelligence qualifying exam,
Spring 1975 



Challenge Problems in Elementary Calculus,
1990 
box 
96349/3 (05086626) 


National Science Foundation, reviews 



Computer Sciences Research Reviews,
October 19, 1987 



ATP papers,
1985 



Application for candidacy, Chen, MinTsuei,
September 1982 



Expert systems lists,
19841987 



"Software for Strategic Systems,"
May 1415, 1987 



American Association for Artificial Intelligence,
1987 



NCR trip,
June 15, 1987 



American Association for Artificial Intelligence,
nominations,
19861987 



Carnegie Mellon University, "Artificial Intelligence at
Microelectronics and Computer Technology Corporation,"
February 18, 1987 



Carnegie Mellon University talk,
February 18, 1987 



ATP bank account,
1985 



Inquiries on ATP prize,
19841985 



American Mathematical Society meeting,
January 913, 1985, ATPprize committee
luncheon,
October 22, 1984 



Mathematical Association of AmericaTexas Section,
April 4, 1987 



National Science Foundation presentation: "Artificial
Intelligence Research at Microelectronics and Computer Technology Corporation,
January 8, 1987 



Charles Babbage Institute: The Center for the History of
Information Processing, Engineering Research Associates,
19851986 



Some Thoughts on Proof Discovery Slides and Notes,
July 22, 1986 



MITRE conference: "Managing Information Resources,"
February 1620, 1987 



Proteus,
May 1986 



American Association of Artificial Intelligence meeting,
August 1015, 1986 



Logic in Computer Science Conference,
June 1618, 1986 



Chapter five of the BledsoeBallantyne book,
Spring 1986 



"Computer Aided Design: Analogical Reasoning for Design,"
1985 



Church of Jesus Christ of LatterDay Saints Artificial
Intelligence meeting,
October 1985 



Completeness Results for Inequality Provers,
1985 



Fermilab,
October 9, 1985 



International Institute for Effective Communication, James
Rogers Fox,
1988 



ATP Prize Committee,
19801985 



Microelectronics and Computer Technology Corporation
correspondence,
19841985 



BRI staff meetings,
1985 



Artificial Intelligence staff meetings,
1985 



Task Force meeting: "Future and Impacts of Artificial
Intelligence,"
August 2123, 1987 



Groundprover,
July 1986 



Analogy references,
1986 



The Use of Analogy in Automatic Proof Discovery
(Preliminary Report),
March 1985 



Porrf Parsing,
1987 



Analogy,
January 1987 



Analogy,
Summer 1986 
box 
96349/4 (05087254) 


ATP problems,
19831990 



Research problems and ideas,
1985 



Curriculum vitae,
19841990 



Vita,
19901994 



ATP book Ballantine and Bledsoe,
January 1984 



Publishing agreement,
1987 



Ph.d., committees,
1992 



Matt Wilding, "MechanicallyChecked FloatingPoint Program
Correctness Proofs,"
June 5, 1990 



Students,
1990 



Larry Van Sickle,
1992 



G. Neelakantan Kartha,
1992 



Marty Mayberry,
1994 



Benjamin Shults,
1995 



Munidar Paul Singh,
1992 



Markus Kaltenbach,
1995 



Larry Van Sickle,
1993 



Norman McCain,
1991 



Robert L. Akers,
1990 



Kenneth S. Murray,
1989 



Ray Mooney,
1991 



Analogy project proposal for summer 1987,
1987 



Shaun Cooper,
19871989 



William Pierce,
19881992 



Artificial Intelligence: An International Journal,
19851990 



Journal of Automated Reasoning,
19841990 



National Science Foundation proposal,
19931996 



National Science Foundation capitalization grant,
19911992 



University of Texas at Austin, chair budget,
19871988 



University of Texas at Austin, budget council meetings,
19931994 



University of Texas at Austin, Undergraduate Studies
Committee,
1991 



University of Texas at Austin, Chair Committee,
19901992 



University of Texas at Austin, Graduate Studies Committee,
19881990 



University of Texas at Austin, undergraduate computer
science programs,
1990 



American Association for Artificial Intelligence
conference notes,
19911993 



International Joint Conference on Artificial Intelligence,
19911993 



National Science Foundation Science and Technology
Research Centers,
19871988 



University of Texas at Austin, College Promotion and
Tenure Committee,
1990 



National Conference of Christians and Jews, Inc.,
19881989 



National Conference of Christians and Jews, Inc.,
19871988 



University of Texas at Austin, Government Relations
Committee,
1988 



National Conference of Christians and Jews, Inc.,
1989 



Mailing lists,
1990 



Population distribution map of the United States,
1950 



Academic Computing: A TenYear Development Plan,
March 1978 



Letters of reference,
19921995 



National Science Foundation,
1994 



Analogy in Automated Theorem Proving,
1994 



National Science Foundation proposal review,
1991 



Miscellaneous correspondence,
19911995 



University of Texas at Austin, Chair Committee,
1989 



Miscellaneous correspondence,
19921993 



Miscellaneous correspondence,
1993 



University of Texas at Austin, Chair Committee,
1987 



Bruce Porter,
1989 



Meigo L. K. Chen,
1993 
box 
96349/5 (05086637) 


Reprints of articles, book chapters, conference
proceedings,
19591986 



William Bevier,
1983 



Ernie Cohen,
1984 



Ph.d committees,
19831984 



ChuaHuang, Huang,
1985 



David Plummer,
1985 



Munjid Musallam,
19851986 



Donald Simon,
1982 



TieChang Wang,
1986 



Myung Kim,
1986 



MinTsuei Chen,
19821986 



Bishop Brock,
1987 



William Pierce,
1987 



Automatic theorem proving, prizes,
1982 



Automatic theorem proving, conference 



Automatic theorem proving, prizes,
1983 



Larry Hines,
1985 



William Bulko,
1985 



Ph.d. committee,
19721982 



IMPLY documentation,
19881989 



EX51,
1989 



Committee to select the dean of Natural Sciences,
19761977 



Ground prover and inequality proofs,
1989 



Computer programs,
1989 



Modelsettheory,
1989 



Resolution program,
1989 



Hand resolution,
1989 



Resolution CLISP,
1986 



Dagstuhl speech: "Some Thoughts on Automated Proof
Discovery Especially HOL and Analysis,"
1993 



Argonne National Laboratory Conference,
1992 



Dagstuhl speech, notes,
1993 



National Science Foundation, budgets,
1992 



CADE 10 speech: "Some Adventures with Automated Proof
Discovery in Higher Order Logic,"
1990 



American Association for Artificial Intelligence
appointments,
1992 



American Association for Artificial Intelligence,
Strategic Planning Committee,
1993 
box 
96349/6 (05085951) 


International Joint Conference on Artificial Intelligence,
1983 



References,
1983 



AM5,
1980 



University of Austin at Texas, Chair Committee,
1983 



Planning meeting for an annual review of Computer Science,
19831984 



International Joint Conference on Artificial Intelligence,
prize planning,
1983 



International Joint Conference on Artificial Intelligence,
conference paper,
1983 



Presentation to Microelectronics and Computer Technology
Corporation,
1983 



CarnegieMellon University visit,
1983 



Automated reasoning papers,
1984 



University of Texas at Austin, Chair Committee,
19831984 



IMPLY papers,
1983 



National Science Foundation proposal,
1983 



POINCARE papers,
1982 (2 files) 



AM5 examples,
1982 



ATTAINS minimum,
1980 



Solving for variable instantiates,
19801981 



China trip,
1982 



AMS paper,
19791983 



PV prize,
1983 



National Science Foundation site visit,
1982 



RES 20 Steering Committee,
1981 



Woodlands artificial intelligence,
1982 



Automatic Theorem Proving papers from China,
19811982 



Problem examples,
1982 



Automatic theorem proving, prizes,
1981 



Automatic theorem proving, Prize Committee,
19791980 



Automatic theorem proving, prizes,
1980 



Automatic theorem proving, Prize Committee,
19791981 



Computer protocol,
1979 



Tony Morse dinner,
19801981 
box 
96349/7 (05086615) 


Automatic Proofs of Theorems in Analysis Using Nonstandard
Techniques,
1977 



Offprints, book chapters,
19691984 



Offprints, book chapters,
19711986 



Offprints, book chapters,
19671987 



Offprints, book chapters,
19741985 



Offprints, book chapters,
19701995 



"Splitting and Reduction Heuristics in Automatic Theorem
Proving,"
1971 



"A Maximal Method for Set Variables in Automatic
Theoremproving,"
1977 



"Conflicting Bindings and Generalized
Substitutions" 



"Computer Proofs of Limit Theorems,"
1972 



"Nonresolution Theorem Proving,"
1977 



Offprints, book chapters,
1990 



Offprints, book chapters,
1993 



Offprints, book chapters,
19861993 



Offprints, book chapters,
19851991 



Offprints, book chapters,
19911993 



Offprints, book chapters,
19701989 



"The UT Interactive Prover,"
1978 



Offprints, book chapters,
19601978 



Offprints, book chapters,
1965 



Offprints, book chapters,
19651967 



Offprints, book chapters,
19521972 



Offprints, book chapters,
19611962 



Pattern Recognition and Reading By Machine 



Offprints, book chapters,
19531962 



"Optimizing of NTuple Memory Matrices Using Gradient
Technique,"
1962 



"The Use of Biological Concepts in the Analytical Study of
Systems,"
1961 



"Lethally Dependent Genes Using Instant Selection,"
1961 



"A Topological Measure Construction,"
1962 



"Facial Recognition Project Report,"
1964 



NTuple papers,
19601968 
box 
96349/8 (05086284) 


ATP 1: "A Linear Format for Resolution with Merging and
New Technique for Establishing Completeness,"
1970 



ATP 2: Splitting and Reduction Heuristics in Automatic
Theorem Proving,
1971 



ATP 3: "Computer Proofs of Limit Theorems,"
1971 



ATP 4: "A ManMachine Theorem Proving System,"
1971 



ATP 5: "Locking: A Restriction on Resolution,"
1971 



ATP 7: "Graphing Methods for Topological Proof,"
1973 



ATP 8: "A Description of the Functions of the ManMachine
Topology Theorem Prover,"
1973 



ATP 9: "Some Ideas on Automatic Theorem Proving,"
1973 



ATP 10: "Discussions on Automatic Theorem Proving,"
1973 



ATP 12: "Locking and Equality Atom Term Locking for
Resolution and Paramodul,"
1973 



ATP 14: "Program Correctness,"
1974 



ATP 15: "Typing and Proofs by Cases in Program
Verification,"
1975 



ATP 16: "Semiautomatic Syntheses of Inductive Predicates,"
1974 



ATP 17: "The UT Interactive Prover,"
1975 



ATP 17a: "The UT Interactive Prover,"
1978 



ATP 17b: "The UT NaturalDeduction Prover,"
1983 



ATP 18: "The SupInf Method in Presberger Arithmetic,"
1974 



ATP 19: "Canonical Form Of a set of Models,"
1974 



ATP 20: "Toward the Interactive Synthesis of Assertions,"
1974 



ATP 21: "Complete sets of Reductions for Computational
Logic,"
1975 



ATP 22: "A Note of Burstall's Structural Induction,"
1974 



ATP 23: "Automatic Proofs of Theorems in Analysis Using
NonStandard Analysis Techniques,"
1977 



ATP 24: "Some Notes on Computer Generation of Counter
Examples in Topology,"
1975 



ATP 26: "An Algebraic Simplifier" 



ATP 27: "National Science Foundation Progress Report,"
19741975 



ATP 29: "NonResolution Theorem Proving,"
1977 



ATP 30: "NonStandard Analysis, Part II. The Meta
Theorist,"
1981 



ATP 31: "Some Thoughts on ATP in Data Base Design and
Use,"
1977 



ATP 31: "A Note on the Modification Method and Uniform
Replacement,"
1976 



ATP 32: "Canonical Inference,"
1975 



ATP 33: "A Maximal Method for Set Variables in Automatic
Theorem Proving,"
1977 



ATP 33a: "A Maximal Method for Set Variables in Automatic
Theorem Proving,"
1977 



ATP 34: "Automatic Theorem Proving,"
1978 



ATP 38: "The Refutation Completeness Of Permutative
Narrowing and Blocked Resolution,"
1977 



ATP 40a: "A Prover for General Inequalities,"
1978 



ATP 40a: "A Prover for General Inequalities,"
1979 



ATP 40s: "A Prover for General Inequalities,"
February 1979 



ATP 41: "Unskolemizing,"
1978 



ATP 42: "Agenda Handling and Other Routines for the New
Prover,"
1978 



ATP 44a: "On Generation of Counterexamples,"
1979 



ATP 45: "The Control Structure of IMPLY,"
1978 



ATP 46: "Theorem Proving in a Program Verification
Context,"
1977 



ATP 47: "Conflicting Bindings and Generalized
Substitutions,"
1978 



ATP 48: "The Refutation Completeness of Blocked
Permutative Narrowing and Resolution,"
1978 



ATP 49: "The Overdirector,"
1979 



ATP 51: "Some Results Better Using Counterexamples to
Shorten Proofs,"
1979 
box 
96349/9 (05085962) 


ATP 52: "A Resolutionbased Prover for General
Inequalities,"
1979 



ATP 53: "An Agenda Driven Theorem Prover,"
1979 



ATP 54: "Proving a Subset of SecondOrder Logic with
FirstOrder Proof Procedures,"
1979 



ATP 55: "Two Theorems on Improving the SUPINF
Process" 



ATP 56a: "Variable Elimination and Changing
ResolutionBased Prover for Inequalities,"
1980 



ATP 57: "Some Completeness Results on Variable Elimination
for an Inequality Prover,"
1980 



ATP 59: "New Decision Algorithms for Finitely Presented
Commutative Semigroups,"
1979 



ATP 60: "Some Completeness Results for A Class of
Inequality Provers,"
1981 



ATP 61: "A Completeness Theorem for Multiple Chaining,"
1980 



ATP 63: "Proof Checking Proposal,"
1981 



ATP 64: "On Generating and Using Examples in Proof
Discovery,"
1981 



ATP 65: "Completeness Results for Inequality Provers,"
1982 



ATP 66: "A PriortyOrdered Agenda Theorem Prover,"
1981 



ATP 67: "Using Examples to Generate Instantiations for Set
Variables,"
1982 



ATP 68: "Function Symbol Elimination,"
1982 



ATP 69: "Automatic Theorem Proving Talk Given to CAMI
Meeting,"
1982 



ATP 70 



ATP 71: "Some Automatic Proofs in Analysis,"
1982 



ATP 72: "Ground Resolution Using AntiClauses,"
1983 



ATP 73: "A Description for Calculations Related to the
Poincare Conjecture,"
1983 



ATP 74: "Completeness of Input Resolution with Instance
Subsuming,"
1983 



ATP 75 



ATP 76: "Proving Elementary Geometry Theorems Using Wu's
Algorithm,"
1983 



ATP 78, 79: Wang, TieCheng 



ATP 80: "Designing Examples of Sematically Guided
Hierarchical Deduction,"
1984 



ATP 81, 82 



ATP 84 



ATP 85a, 88, 88b 



ATP 89e, 90, 91, 96 



ATP 97, 98, 99, 100 
box 
96349/10 (05086794) 


Lecture notes: 




Math 427L,
spring 1973 




Math 427L,
spring 1982 (2 folders) 




Math 665a,
fall 1978 




Math 427K,
fall 1981 




Math 665a,
fall 1971 




Math 304E(52225), RLM 5124,
spring 1982 




Math 305G,
fall 1977 




Math 305G (50760),
spring 1980 




Math 305G,
fall 1982 




Math 325 (48595),
fall 1979 




Math 608Ea,
fall 1978 




Math 608Eb (51220),
spring 1980 




Math 608Eb (52065),
spring 1983 




Math 608Eb (52490),
spring 1984 




Computer Science 304F,
fall 1980 




Math 318K (54095),
fall 1983 




Math 808A (52295),
fall 1980 




Math 808B (5277085),
spring 1981 
box 
96349/11 (05083640) 


International Institute for Effective Communication(s),
1991 



Journal Of Automated Reasoning,
1989 



Kaiserlauten transparencies,
1989 



University of Texas at Austin, full professor review,
1989 



Artificial intelligence planning,
1989 



Mathematics and Artificial Intelligence,
fall 1990 



Argonne National Laboratory,
1991 



Argonne National Laboratory,
1989 



LICS,
1989 



Letters of recommendation,
19701976 



University of Texas at Austin, full professor review,
1989 



American Association for Artificial Intelligence
Symposium,
1989 



International Joint Conference on Artificial Intelligence,
1989 



General ATP transparencies,
1988 



American Association for Artificial Intelligence: "A
Survey of Automated Deduction,"
1987 



ISMIS,
1987 



American Association of Artificial Intelligence,
1987 



Survey sources 



Bruce Porter, tenure review,
1989 



CADE9 reviews,
1988 



Survey papers,
1988 



International Joint Conference on Artificial Intelligence,
1987 



Fall Joint Computer Conference,
1987 



"Some Thoughts of Artificial Intelligence,"IEEE Computer
Society,
1987 



University of Chapel Hill symposium,
1987 



Texas Instrument speech, notes and transparencies,
1987 



National Science Foundation/CER meeting, notes and
transparencies,
1987 



University of Texas at Austin grade change forms,
1983 



University of Texas at Austin miscellaneous file,
1987 



National Science Foundation, committee meeting,
1987 



Carnegie Mellon University, speaker,
1987 



National Science Foundation,
19831986 



Office of Naval Research proposal,
1987 
box 
96349/12 (05083708) 


Student computer assignments,
1991 (7 file folders) 



Artificial Intelligence and Expert Systems Fundamentals:
exercises,
1988 



Computer Science 336, transparencies and lecture notes,
fall 1989 



Computer Science 336, class photographs,
fall 1989 



Computer Science 336, class handouts,
1989 



Student computer science projects,
1990 



Civil defense research project,
1959 



Ideas, counter examples, special problems of Bledsoe,
19521968 



Bledsoe personal papers,
19631971 



Sandia Corporation papers,
1961 



Papers on facial recognition,
19641987 



Sandia Corporation research report,
1957 



Computer programs,
1981 



OA completeness and validity ideas,
1971 



University of Texas at Austin budget councils rules,
1969 



Class notes: Math 395c/Computer Science 395t,
spring 1979 



Herb Federer reprints,
1967 



Class notes: Math 362k,
fall 1974 



List of ATP reports,
19861994 



Notebooks 




Math 210B,
spring 1949 




Math 205A 




Math 210B, chapters 7, 8, 9, 10 




Math 210A, chapters 2, 3,
19491950 




Math 210B, chapters 4, 5, 6,
19491950 




Math 210A, chapters 0, 1, 2,
19491950 
box 
96349/13 (05086262) 


Bledsoe memorials,
1996 



Automated Reasoning: Essays in Honor
of Woody Bledsoe, edited by Robert S. Boyer,
1991 



Lists of people and addresses (5 file folders) 



Computer articles,
19731975 



Computer expenses,
1986 



Computer programs 



Allocationsponsored, computer costs,
1985 



Allocationsponsered 



Computer accountMASH,
1986 



Bledsoe account MAED,
1985 



Dave Plummer (Edinburgh),
1984 



Research DEC20, financial statements,
1985 



Computer expenses,
1984 



Research papers,
19881989 



Research papers,
19871988 



Publication bibliography,
1987 



Lists of publications,
19851986 



Bledsoe addresses,
1982 



Publication bibliography update,
1993 



Research papers and technical reports,
19871991 



Institut National de Recherche en Informatique et en
Automatique newsletters 



Publication bibliographies,
1990 



Technical reports, Carnegie Mellon University,
1990 



Technical reports,
19901994 



Technical reports,
19891994 
box 
96349/14 (05086127) 


Papers of others, PS 
box 
96349/15 (05087094) 


University of Minnesota speech,
1985 



Mathematics Prize receipts,
19831984 



Letters of correspondence: 




GHI,
1985 




DEF,
1985 




ABC,
1985 




JKL,
1985 




MNO,
1985 




PQR,
1985 




STU,
1985 




VWXYZ,
1985 




M,
1984 




N,
1984 




O,
1984 




P,
1984 




Q,
1984 




R,
1984 




S,
1984 




T,
1984 




U,
1984 




V,
1984 




W,
1984 




XYZ,
1984 




F,
1984 




D,
1984 




C,
1984 




B,
1984 




A,
1984 




G,
1984 




H,
1984 




E,
1984 




J,
1984 




K,
1984 




L,
1984 



Boeing speech,
1986 



American Association of Artificial Intelligence,
1985 



ATP 585F, projects,
1993 



Course notes 



Automatentheorie und Formale
Sprachen, Michael Richter 
box 
96349/16 (05086433) 


Papers of others, DL 
box 
96349/17 (05086444) 


Papers of others, LO 
box 
96349/18 (05083683) 


Research papers: 




Lincoln study,
19671978 




Substitution,
1968 




Schematic resolution,
1968 




Schematic substitution,
1969 




Fortran,
1982 




19691970 notes 




Computer programs,
1972 




Facial recognition,
1991 




One atom locking,
1973 




Edinburgh speech,
1973 




Operating instructions,
1973 




Semiautomatic theory proving (topology),
1972 




Derivative theories,
1972 




Morse code,
1967 




Chromosome band structure,
1967 




Chromosome project,
1972 




Design papers,
1972 




Chromosome structure,
1972 




Morse code,
1966 




Automatic theory proving, checking,
1967 




Elementary algebra proofchecking,
1968 




Borel rectangles,
1972 




Automatic theorem proofchecking in set theory,
1968 




Automatic theorem proving,
1969 




Automatic theorem proving seminar,
19681969 



Computer Science 395T/ Math 395C,
spring 1976 



Computer Science 395T/ Math 395C,
spring 1975 
box 
96349/19 (05083672) 


Analogy,
summer 1986 



Analogy,
fall 1986 



Analogy,
summer 1986 



Multiple entry plans,
1985 



Cleaning and double entry,
1985 



Analogy,
JuneOctober 1985 



Analogy,
March 1985 



Analogy,
March 1985 



Analogy in automatic theorem proving,
1985 



Handanalogy,
1985 



University of Minnesota analogy speech 



Analogy,
August 1984 



IMPLY/LSP,
1986 



New prover,
March 1976 



Yet to prove,
1973 



Course evaluation,
fall 1976 



Course evaluation,
spring 1974 



Course evaluation,
fall 1974 



Course evaluation,
spring 1976 



Course evaluation,
19711972 



Course evaluation,
spring 1981 



Course evaluation,
fall 1978 



Course evaluation,
fall 1979 



Microelectronics and Computer Technology Corporation
technical report,
1985 



Forcing and limit heuristic,
19701971 



Building families,
19741975 



American Association for Artificial Intelligence,
1984 



Army Research Office proposal,
1983 



National Institutes for Health budget,
1972 



ROBOT proposal,
1981 



American Association for Artificial Intelligence,
presidential address,
1985 



Rutgers panel,
May 12, 1985 



Machine learning workshop,
June 1985 



International Joint Conference on Artificial Intelligence
meeting,
1985 



American Association for Artificial Intelligence council
meeting,
August 1985 



Automatic theorem proving prize committee,
1984 



Automatic theorem proving prize committee,
1985 



Automatic theorem proving prize committee,
1983 
box 
96349/20 (05083650) 


Class work: 




Examinations: 





Computer Science 343 





Mathematics 365C 




Exercises: 





Computer Science 336,
spring 1989 





Computer Science 336,
fall 1988 




Transparencies 




Elaine Rich's Artificial Intelligence course
transparencies 




Computer Science 343, old handouts,
fall 1991 




Beliefs among agents,
1991 




Computer Science 343: notes, papers 
box 
96349/21 (05083639) 


Talks and lectures: 




Peking lecture notes 




University of Texas at Austin, speech notes 




Speech,
September 25, 1967 




Pattern recognition speech 




Peking speech transparencies 




Reduction transparencies 




Automatic theorem proving speech
transparencies 




9.7 examples 




CADE 6 speech,
1982 




Nonstandard analogy,
1984 




Peking transparencies 




BoyerMoore prover transparencies 




Intentional logic transparencies 




S and P problems 




Reasoning in expert systems 




Project synthesis 




Wu's method 




Automatic theorem proving,
spring 1981 




Natural systems: IMPLY 




Automatic theorem proving, at the University of Texas at
Austin 




Symbolics talk 




Computer Science graduate student's speech 




Some proofs in analysis, transparencies 




NTSU talk,
February 1982 




China: extra transparencies 




SRI talk,
July 1981 




ISI/SRI talks,
1978 




Pi MU Epsilon talk,
1981 




Automatic theorem proving conference,
1979 




CADE 5 talk,
July 1980 




AMSReno talk,
April 1981 




ONR panel talk,
April 1979 




Higher order matching,
spring 1976 




Presberger talk,
1975 




General inequalities talk,
September 1977 




Physics seminar talk: "Artificial Intelligence,"
March 1977 




Automatic theorem proving IV 




Talk on artificial intelligence: Town and Gown,
November 1978; Mensa,
October 1977 




Northern Illinois talk,
March 1979 




National Science Foundation,
March 1978 




Carnegie Mellon University,
April 1978 




Canada talks,
1977 




Rice talk,
1974 




Automatic theorem proving transparencies 




Syracuse talk,
1976 




Basic principles transparencies 




International Joint Conference on Artificial
Intelligence transparencies,
1973 




Dallas talk,
1974 




Talks,
1976 




Carnegie Mellon University talks,
1976 




SRI artificial intelligence seminar,
1974 




MIT, automatic theorem proving seminar,
1971 
box 
96349/22 (05086943) 


Class work: 




Computer Science 343,
fall 1987 




Computer Science 343, lecture notes,
fall 1987 




Knowledge representation 




Problem solving 




Language 




Knowledge acquisition 




Vision 




Output 




Support material for Computer Science 343,
fall 1987 




Computer Science 343,
fall 1983 




"Protos: An ExemplarBased Learning
Apprentice" 




QED file 




Computer Science 336,
fall 1989 
box 
96349/23 (05083661) 


Class work: 




Computer Science 395T/Mathematics 395C,
spring 1984 




Prover notes 




Automatic Theorem Proving,
May 1986 




Manmachine 




Typing and proof by cases,
1975 




Automatic Theorem Proving class extra 




Computer Science 383,
fall 1990 




Class pictures, Computer Science 395T, Math 395C,
1989 




Computer Science 343,
fall 1990 




Computer Science 345,
fall 1988 



Recommendations for Bu, Min, Neely, Just, Rana,
Guam 



Learning 



International Joint Conference on Artificial Intelligence,
1982 



9.5 Hines 



IMPLY transparencies,
1986 



Set variables,
1981 



IMPLY1.LSP,
1985 



Analogy
1983 



IMPLY output,
1986 



Facial recognition,
1966 



Other natural systems 



IMPLY2.LSP,
1986 



Agenda examples 



International Joint Conference on Artificial Intelligence,
1983 



IMPLY.LSP transparencies,
1986 



Expert systems,
1982 



Prover (general), Bledsoe and Hines 



IMPLY documentation transparencies 



Set variables 



Higher order logic 



Automatic theorem proving extra 
box 
96349/24 (05083694) 


Research paper 



Completed STR+VE paper,
1980 



National Science Foundation panel report,
1979 



Variableelimination, shielding term chaining
completeness,
January 1980 



Automatic theorem proving 51,
August 1979 



Number theory,
November 1979 



Examples,
1980 



Tree reorder theories,
1980 



Automatic theorem proving seminar,
1980 



Full set,
June 1980 



Graphs and chains,
1980 



Upperlevel prover,
1979 



Solve paper,
April 1974 



Grant proposal,
fall 1979 



Continuous of continuous,
August 1979 



AB1AB13 



Resolution stuff,
1979 



Solve 



Resolution program,
1979 



Complete sets of deductions,
1979 



Resolution paper,
1979 



Computer Science degree plan 



Evolution IDEA 



Facial recognition,
1969 



BledsoeHart paper 



Chromosome project,
1969 



Budgets 



New completeness proofs for ground resolution 



Ethan Platt 



Canonical and minimal 



Faces,
19681969 



Regular conditional probabilities 
box 
96349/25 (05086105) 


Artificial Intelligence seminar,
1966 



Distributed systems proposal,
1978 



Theorem proving ARPA proposal,
1978 



Atlanta workshop,
1978 



Policy Committee,
1974 



Applied Committee,
1973 



Department chairmans meetings 



Department meeting 



Full professors 



Committees 



National Science Foundation proposal,
1977 



Proposal,
19771978 



Computer runs and talk,
1979 



Set variables,
November 1979 



Heuristics,
1978 



Automatic theorem proving papers 



CE and John Minor's theorems,
1978 



Old
1978 



General inequalities,
1978 



General inequalities,
1977 



Rules,
1977 



Large IMPLY,
19771978 



Name entry ports,
1977 



Reentrant subgoals,
1977 



Extra inequalities,
1977 



Higher order in IMPLY,
June 1976 



Examples of higher order,
Spring 1976 



Matrix calculations: higher order,
July 1976 



HeineBorel,
1976 



Old and details,
Spring 1976 



Artificial intelligence group,
1976 



Prover,
May 1975 



Dissertation topics and ideas,
1975 



AOT,
December 1976 



ISI,
July 1975 



Plan,
19731975 
box 
96349/26 (05086648) 


Personal papers 



Book folder 



BledsoeBallantyne book 



Automated theorem proving book,
1973 



Automated theorem proving book,
1986 



Curriculum vita 



National Science Foundation,
19801981 



American Association for Artificial Intelligence Strategic
Committee,
1985 



American Association for Artificial Intelligence tutorial
plan,
1985 



INTRELL,
1985 



International Joint Conference on Artificial Intelligence,
committee meeting,
1985 



Mauldin,
1985 



Douglas Lenat: University of Texas at Austin, appointment,
1984 



Monthly reports 



American Association for Artificial Intelligence
committees,
1984 



International Conference in Fifth Generation Computer
Systems,
1984 



"Computer: Automated Theorem Proving" 



Microelectronics and Computer Technology Corporation
people,
19841985 



Buffalo talk,
April 1978 



KA book,
1984 



Artificial intelligence staff meetings 



Austin Rotary Club address,
June 1984 



Europe trip,
1984 



Artificial intelligence talks 



Honeywell talks,
1984 



Science futures talk,
May 1984 



Microelectronics and Computer Technology Corporation talk,
April 1983 



American Association for Artificial Intelligence,
1985 



American Association for Artificial Intelligence,
presidential address,
1985 



Outlines 



University of Maryland talk,
1985 



University of Maryland trip,
March 1985 



University of Maryland, Wang's talk,
1985 



University of Minnesota,
1985 



University of Minnesota, "Directions of Artificial
Intelligence,"
May 1985 



Express LSP,
1985 



Bledsoe papers 
box 
96349/27 (05086273) 


Function Symbol Elimination,
1982 



Panel membership and proposal lists 



Robert Neveln 



Dean selection committee,
1987 



National Science Foundation,
1981 



MI 10,
1981 



American Association for Artificial Intelligence,
1982 



Artificial intelligence meeting,
1978 



Chainer,
1979 



John Minor,
1979 



Resolution and general inequalities,
1979 



Expected cost,
1979 



Counterexamples,
1978 



Prover,
1978 



Toplevel prover,
1978 



Steering committee,
1981 



Reductions,
1981 



Ekman,
1981 



SRI trip,
summer 1981 



Reno meeting,
April 1981 



WISE.PRV.3 



Automatic theorem proving 60,
1981 



MI 10,
spring 1981 



Bledsoe papers 



Volume paper 



Automatic theorem proving volume,
1983 



Book contract 



Associates 



Automatic theorem proving,
1983 
box 
96349/28 (05086954) 


El Paso talk,
1972 



Carnegie Mellon talk,
1973 



Talks on automatic theorem proving 



August 1974 



Examples,
AugustSeptember 1969 



Matching 



Locking 



Reviews 



National Science Foundation proposal,
1967 



Mu completion measures,
1969 



General inequality theorem prover: STR+VE 



Inequality provers 



Variations of resolutions 



The UT Interactive Prover,
1978 



Class work: 




Mathematics 427K,
fall 1972 




Computer Science 304F,
fall 1980 




Mathematics 427L,
1974 




Old handouts 




Computer Science 395T,
spring 1988 




Automated theorem proving class material 




Automated theorem proving,
1988 




Logic 




Completeness proof,
1988 




Completeness transparencies,
1986 




Computer Science 395T,
spring 1986 




Automated theorem proving class speakers 
box 
96349/29 (05086422) 


Papers of others, TZ 



Miscellaneous 



Ph.D. thesis, Berkeley,
1953 



Austin Magazine,
July 1984 



Math 210: "Real Variables Problems" 



On a Stieltjes Integral,
Joseph Weihe,
1955 



Bledsoe papers,
19661989 



IMPLY documentation 
box 
96349/30 (05086772) 


Oversized materials: 




Microfiche 




Discussions: Architecture Machine Group,
1983 (Video laser disc) 




3.5 in discs 




3.5 in floppy discs 




1 mathematics tape 




Man machine facial recognition notes and transparencies,
1990 




Symposium materials 




Computer printouts 
box 
96349/31 (05086116) 


Mauldin,
1984 



Problems 15,
1983 



Machine intelligence paper 



Sphere construction problem 



Original figures 



Splitting and reduction paper,
1978 



Set variables 



International Joint Conference on Artificial Intelligence,
1983 



Automatic theorem proving 42,
1978 



Automatic theorem proving 41,
1978 



Borel paper, multiple versions 



Sets generated by rectangles,
1973 



Inequality about complex numbers,
1969 



Galley proofs for product measures 



Some aspects of covering theory 



On a differential inequality 



Neighborly functions 



Pattern recognition and reading by machine 



Locating features 



Some results on multicategory pattern recognition,
1966 



Final draftlimits 



Manmachine paper 



Manmachine facial recognition 



American Association for Artificial Intelligence,
1982 



Nonlinear,
1981 



Facial recognition,
April 1982 



Directedresolution,
January 1981 



Solving for set variables,
1981 



Kerr's paper,
1982 



Michael Starbird's protocols 



Wednesday noon seminar,
1981 



National Science Foundation,
19791980 



Proof checking proposal,
1981 



DEC 2060,
January 1980 



DEC 2060 Steering Committee 



PRI:18 Bisson,
1965 



PRI:19, PRI:19A Chan and Bledsoe 



PRI:20 Bisson 
box 
96349/32 (05087108) 


Correspondence 
box 
96349/33 (05087265) 


Papers of others, AC 
box 
96349/34 (05087119) 


Theses and dissertations: 




James Daniel Christian, "HighPerformance Permutative
Completion,"
1989 




Nicholas Freitag McPhee, "Mechanically Proving Geometry
Theorems Using Wu's Method and Collins' Method,"
1993 




Brad Brand Blumenthal, "Applying Design Replay to the
Domain of Metaphoric Human Interface Design,"
1990 




"The Formal Specification and Verification of the FM9001
Microprocessor,"
1993 




Forest Baskett, "Mathematical Models of Multiprogrammed
Computer Systems,"
1970 




William D. Young, "A Verified Code Generator for a
Subset of Gypsy,"
1988 




Munindar Paul Singh, "A Theory of Actions, Intentions,
and Communications for Multiagent Systems,"
1992 




Yuan Yu, "Automated Proofs of Object Code for a Widely
Used Microprocessor,"
1992 




Hwee Tou Ng, "A General Abductive System with
Application to Plan Recognition and Diagnosis,"
1992 




Neil Allen Iscoe, "DomainSpecific Programming: An
ObjectOriented and KnowledgeBased Approach to Specification and Generation,"
1990 




James Lawrence Hall, "Topological Product Measures,"
1967 




Claude Vernon Duplissey, "Theory and Applications of
Measurable Cardinals,"
1967 




Stephen Alan Underwood, "Visual Learning and Recognition
by Computer,"
1972 




Gordon Shaw Novak, "Computer Understanding of Physics
Problems Stated in Natural Language,"
1976 




Sakthi Subramanian, "A Mechanized Framework for
Specifying Problem Domains and Verifying Plans,"
1993 




John Wilson Roach, "Determining the ThreeDimensional
Motion and Model of Objects from a Sequence of Images,"
1980 




Bill Delano Anderson, "Extensions and Projections in
Spaces of Continuous Functions,"
1970 




Daniel Louis Dvorak, "Monitoring and Diagnosis of
Continuous Dynamic Systems Using Semiquantitative Simulation,"
1992 
box 
96349/35 (05087276) 


Fhlcompleteness,
19831985 



Fhl,
1983 



IMPLY2, Fhl.LSP,
1983 



Fhl, resolution,
March 1983 



Fhl, resolution,
JuneDecember, 1983 



Schlumberger,
1982 



National Science Foundation site visit,
January 1982 



Proposal 



Bledsoe correspondence: 




19721973 




19731974 




19741975 




19751976 



Artificial intelligence,
1975 



International Joint Conference for Artificial
Intelligence,
1977 



Reviews 



Recommendation letters 
box 
96349/36 (05088020) 


Correspondence: 




1965 




1978 




1970 




1971 




1972 




1973 




1977 




1968 




1969 




19661968 




19741975 




19741977 




PRI 




Recognition research 




Church of Jesus Christ of LatterDay Saints 




Bremerman, Hans 




Advanced Research Projects Agency 




A. B. Dick Company 




Market Compilation and Research Bureau 




Equitable Life Assurance Society of the United
States 




Granger Associates 




McCall Corporation 




State of New York, identification and intelligence
project 




Old recruiting 




Undergraduate teaching and suggestions 




Course outlines 




Mathematics Department committees 




National Institutes of Health 




Committee A 




College of Science 




Statistics meeting 




Teaching Assistants meeting 




New building 




Advisor's meeting 




Department meeting 




Mathematics chairman meeting 




Curriculum,
1968 




Teaching assistant's reports 




University of Texas at Austin 
box 
96349/37 (05088010) 


Correspondence: 




University of California,
19501953 




Old Ph.D. committee 




Stone Wilson 




Artificial Intelligence Journal 




Artificial Intelligence Journal
reviews 




Dean Selection Committee 




Dr. Stone's papers 




National Institutes of Health,
May 1966 




Department policy 




Automatic theorem proving proposal for the National
Science Foundation,
19721974 




Budget 




National Science Foundation,
19741977 




International Joint Conference on Artificial
Intelligence,
1981 




CADE5,
1980 




Automatic theorem proving workshop,
1979 




Automatic theorem proving conference,
1978 




International Joint Conference on Artificial
Intelligence,
1977 




Deduction workshop,
1977 




International Joint Conference on Artificial
Intelligence meetings,
1977 




International Joint Conference on Artificial
Intelligence,
1975 




IEEE Workshop on Automated Theorem Proving,
1975 




International Joint Conference on Artificial
Intelligence papers,
1979 




NATO ASI,
July 1975 




OBERWALFACH,
1976 




National Science Foundation,
1980 




Computer programs 




Papers of others 




Population, genetics, miscellaneous 




Program geometry, 3D recognition 




Logs 




00, J. L. 




Glint,
1966 




Chromosomes 




3D report 
box 
2.325/OD4 


Oversized material: 




Poster of the University of Texas at Austin campus,
1983 
box 
2/Film D2D4 


Joel Moses' calculus film 



2 unidentified films 