Articles
--------

63  Slagle, J.R., A Heuristic Program that Solves Symbolic Integration
    Problems in Freshman Calculus.  JACM, v10 n5, 1963, 507-520.

63  Robinson, J.A., Theorem-Proving on the Computer.  JACM, v10 n2, 1963,
    163-174.

65  Robinson, J.A., A Machine-Oriented Logic Based on the Resolution
    Principle, JACM, v12 n1, 1965, 23-41.

65  Slagle, J.A., Experiments with a Deductive Question-Answering Program.
    Communications of the ACM, v8 n12, 1965, 792-798.

67  Slagle, J.A., Automatic Theorem Proving With Renamable and Semantic
    Resolution.  JACM, v14 n4, 1967, 687-697.

68  Green, C.C., B. Raphael, The use of theorem-proving techniques in
    question-answering systems, Proc. ACM Natl. Conf., 1968, 169-181.

70  xxxx, Automatic Deductive Question Answering, Artificial Intelligence?,
    ??, 1970?, 136-142.

70  Yates, R.A., Raphael, B., Hart, T.P., Resolution Graphs.  Artificial
    Intelligence, v1, 1970, 257-289.

70  Kowalski, R., Search Strategies for Theorem-Proving.  Machine
    Intelligence, v5, 1970, 181-201.

71  Kowalski, R., Kuehner, D., Linear Resolution with Selection Function.
    Artificial Intelligence, v2, 1971, 227-260.

75  Kowalski, R., A Proof Procedure Using Connection Graphs.  JACM, v22 n4,
    1975, 572-595.

76  Doyle, J., A Truth Maintenance System.  Artificial Intelligence 12,
    1979, 231-272.

76  McCharen, J.D., R.A. Overbeek, L.A. Wos, Problems and Experiments for and
    wih Automated Theorem-Proving Programs, IEEE Trans. on Comp., v25 n8,
    1976, 773-782.

76  Wilson, G.A., J. Minker, Resolution, Refinements, and Search Strategies:
    A Comparative Study, IEEE Trans. on Comp., v25 n8, 1976, 782-801.

76  Winker, S.K., An Evaluation of an Implementation of Qualified
    Hyperresolution, IEEE Trans. on Comp., v25 n8, 1976, 835-843.

76  Andrews, P.B., Refutations by Matings, IEEE Trans. on Comp., v25 n8,
    1976, 801-807.

76  Sickel, S., A Search Technique for Cluse Interconnectivity Graphs,
    IEEE Trans. on Comp., v25 n8, 1976, 823-835.

78  Doyle, J., A Glimse of Truth Maintenance.  AI Memo 461 MIT.

78  McAllister, D.A., A Three Valued Truth Maintence System.  AI Memo 473
    MIT.

79  Chang, C.L., Slagle, J.R., Using Rewriting Rules for Connection Graphs to
    Prove Theorems.  Artificial Intelligence, v12, 1979, 159-180.

79  Doyle, J., A Truth Maintenance System.  Artificial Intelligence, v12,
    1979, 231-272.

80  Bobrow, D.G., Editor's Preface on TMS.  AI v13 1980.

81  Andrews, P.B., Theorem Proving via General Matings.  JACM, v28 n2, 1981,
    193-214.

81  Bibel, W., On Matrices with Connections.  JACM, v28 n4, 1981, 633-645.

86  Digricoli, V.J., M.C. Harrison, Equality-Based Binary Resolution, JACM,
    v33 n2, 1986, 253-289.

86  Henckel, J.D., SMART - A Resolution Theorem Prover with Simple Truth
    Maintenance System.  Directed study report, Univ. of Michigan, 1986.

87  Murray, N.V., E. Rosenthal, Inference with Path Resolution and Semantic
    Graphs.  JACM, v34 n2, 1987, 225-254.

88  Chvatal, V., Szemeredi, E., Many Hard Examples for Resolution.  JACM, v35
    n4, 1988, 759-768.

88  Stickel, M.E., Resolution Theorem Proving, Annual Review of Computer
    Science, v3, 1988, 285-316.

88  Escalade-Imaz, G., Ghallab, M., A Practically Efficient and Almost Linear
    Unification Algorithm.  Artificial Intelligence, v36, 1988, 249-263.

88  Leung, Y.Y., Lee, D.L., Logic Approaches for Deductive Databases.  IEEE
    Expert, 1988, 64-75.

88  Miller, S.A., Schubert, L.K., Using Specialists to Accelerate General
    Reasoning.  Proc. IJCAI, 1988, 161-165.

88  Munch, K.H., A New Reduction Rule for the Connection Graph Proof
    Procedure.  Journal of Automated Reasoning, v4, 1988, 425-444.

88  Slagle, J.R., Application of a Generalized Network-Based Expert System
    Shell:  Artificial Intelligence Mini-tutorial Part I.  Proc. Symposium on
    the Engineering of Computer-based Medical Systems, 1988, 33-42.

89  Walther, C., Many-Sorted Inferences in Automated Theorem Proving.
    Proc. Sorts and Types in Artificial Intelligence Workshop, 1989.

90  Roach, J.W., Sundararajan, R., Watson, L.T., Replacing Unification by
    Constraint Satisfaction to Improve Logic Program Expressiveness.  Journal
    Automated Reasoning, v6, 1990, 51-75.

91  Hsiang, J., Rusinowitch, M., Proving Refutational Completeness of
    Theorem-Proving Strategies:  The Transfinite Semantic Tree Method.  JACM,
    v38 n3, 1991, 559-587.

91  Bhatta, K.S.H.S.R., Karnick, H., A resolution rule for well-formed
    formulae.  Theoretical Computer Science, v81, 1991, 223-235.

91  Dick, A.J.J., An Introduction to Knuth-Bendix Completion.  The Computer
    Journal, v34 n1, 1991, 2-15.


Books
-----

77  Thomas, J.A., Symbolic Logic, Merrill Publishing Company, Columbus, OH,
    1977.

82  Quine, W.V., Methods of Logic, Fourth Edition, Harvard University Press,
    Cambridge, MA, 1982.

83  Rich, E., Artificial Intelligence, McGraw-Hill Book Company, NY, 1983.

83  Sowa, J., Conceptual Structures:  Information Processing in Mind and
    Machine, Addison-Wesley Publishing Company, Reading, MA, 1983.

84  Wos, L., R. Overbeek, E. Lusk, J. Boyle,  Automated Reasoning:
    Introduction and Applications, Prentice Hall, Englewood Cliffs, NJ, 1984.

86  Genesereth, M., Nils Nilsson, Logical Foundations of Artificial
    Intelligence, Morgan Kaufmann Publishers, Inc., Los Altos, CA, 1986.

88  Wos, L., Automated Reasoning:  33 Basic Research Problems, Prentice Hall,
    Englewood Cliffs, NJ, 1988.

89  Blasius, K.H., H.J. Burckert, Deduction Systems in Artificial
    Intelligence, Ellis Horwood Limited, West Sussex, England, 1989.

89  Thayse, A. (editor), From Modal Logic to Deductive Databases:  Introducing
    a Logic Based Approach to Artificial Intelligence, John Wiley & Sons,
    NY, 1989.