The use of theorem-proving techniques in question-answering systems

ABSTRACT

For the purpose of this paper, a question-answering system is a computer program that has at least the following three characteristics: (1) The ability to accept statements of fact and store them in its memory (2) The ability to search stored information efficiently and to recognize items that are relevant to a particular query (3) The ability to respond appropriately to a question by identifying and presenting the answer if it is present in memory, and by deducing a reasonable logical response from relevant knowledge if the complete answer is not explictly available.

REFERENCES

• 1: R. F. Simmons, Answering English questions by computer: a survey, Communications of the ACM, v.8 n.1, p.53-70, Jan. 1965 [doi>10.1145/363707.363732]
• 2: K M COLBY H ENEA Heuristic methods for computer understanding of natural language in context-restricted on-line dialogue Dept of Computer Sciences Stanford University 196
• 3: J A CRAIG et al DEACON: direct english access and control AFIPS Proc FJCC Vol 29 1966
• 4: R. E. Levien , M. E. Maron, A computer system for inference execution and data retrieval, Communications of the ACM, v.10 n.11, p.715-721, Nov. 1967 [doi>10.1145/363790.363817]
• 5: J McCARTHY Situations, actions and casual laws Memo No 2 Stanford Artificial Intelligence Project Stanford University July 1963
• 6: R QUILLIAN AFIPS Proc SJCC Vol 30 1967
• 7: R F SIMMONS An approach toward answering english questions from text AFIPS Proc FJCC Vol 29 1966
• 8: James R. Slagle, Experiments with a deductive question-answering program, Communications of the ACM, v.8 n.12, p.792-798, Dec. 1965 [doi>10.1145/365691.365960]
• 9: F B THOMPSON English for computer AFIPS Proc FJCC Vol 29 1966
• 10: Joseph Weizenbaum, ELIZA—a computer program for the study of natural language communication between man and machine, Communications of the ACM, v.9 n.1, p.36-45, Jan. 1966 [doi>10.1145/365153.365168]
• 11: L. Stephen Coles, An on-line question-answering systems with natural language and pictorial input, Proceedings of the 1968 23rd ACM national conference, p.157-167, August 27-29, 1968 [doi>10.1145/800186.810577]
• 12: J L DARLINGTON Machine methods for improving logical arguments expressed in English Mechanical Translation Vol 8 Nos 3 and 4 pp 41-47 June and October 1965
• 13: J MC CARTHY Programs with common sense Memo No 7 Stanford Artificial Intelligence Project Stanford University September 1963
• 14: B RAPHAEL A computer program which 'understands' AFIPS Proc FJCC Vol 26 1964
• 15: B. Raphael, SIR: A COMPUTER PROGRAM FOR SEMANTIC INFORMATION RETRIEVAL, Massachusetts Institute of Technology, Cambridge, MA, 1964
• 16: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 17: A NEWELL Unpublished seminar talk
• 18: Bertram Raphael, Aspects and applications of symbol manpulation, Proceedings of the 1966 21st national conference, p.69-74, January 1966 [doi>10.1145/800256.810683]
• 19: A NEWELL J C SHAW H A SIMON Empirical explorations of the logic theory machine: a case study in heuristics Paper presented at the Western Joint Computer Conference Los Angeles February 28 1957
• 20: F BLACK A deductive question-answering system Harvard University Ph D Thesis 1964
• 21: D C COOPER Theorem proving in computers Advances in Programming and Non-Numerical Computation L FOX ed Pergamon Press 1966
• 22: J A ROBINSON A review f automatic theorem-proving American Mathematical Society Symposia on Applied Mathematics XIX 1967 Rice University (to be published
• 23: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 24: KALISH and MONTAGUE Logic: techniques of formal reasoning Harcourt Brace and World 1964
• 25: L WOS et al The unit preference strategy in theorem proving AFIPS Proc FJCC Vol 26 1964
• 26: T P HART A useful algebraic property of Robinson's unification algorithm Memo No 91 AI Project Project MAC MIT 1965
• 27: James R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM (JACM), v.14 n.4, p.687-697, Oct. 1967 [doi>10.1145/321420.321428]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

Additional Classification:
  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.4 Systems and Software

General Terms:
Theory