State-space problem-reduction, and theorem proving—some relationships

ABSTRACT

This paper suggests a bidirectional relationship between state-space and problem-reduction representations. It presents a formalism based on multiple-input and multiple-output operators which provides a basis for viewing the two types of representations in this manner. A representation of the language recognition problem which is based on the Cocke parsing algorithm is used as an illustration. A method for representing problems in first-order logic in such a way that the inference system employed by a resolution-based theorem prover determines whether the set of clauses is interpreted in the state-space mode or in the problem-reduction mode is presented. The analogous concepts in problem-reduction and theorem proving, and the terminology used to refer to them, are noted. The relationship between problem-reduction, input resolution, and linear resolution is is discussed.

REFERENCES

• 1: C. L. Chang, The Unit Proof and the Input Proof in Theorem Proving, Journal of the ACM (JACM), v.17 n.4, p.698-707, Oct. 1970 [doi>10.1145/321607.321618]
• 2: Chang, C.L., and Slagle, J.R. An admissible and optimal algorithm for searching AND/OR graphs Artificial Intelligence J. 2, 2 (Fall 1971), 117-128.
• 3: John Cocke, Programming languages and their compilers: Preliminary notes, Courant Institute of Mathematical Sciences, New York University, 1969
• 4: Ernst, G.W., and Newell, A. GPS--A Case Study in Generalit), and Problem Solving, Academic Press, New York, 1969.
• 5: Fikes, R.E., and Nilsson, N.J. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence. 2, (197l), 189-208.
• 6: Green, C.C. Application of theorem proving to problem solving. In: Proc. Intern. Joint Conf. on Artificial Intelligence, D.E. Walker and L.M. Norton (eds.), Washington, D.C., 1969, pp. 219-239.
• 7: Hewitt, C. Description and theoretical analysis (using schemata) of planner: A language for proving theorem and manipulating models in a robot. AI TR-258, MIT, Cambridge, Mass., 1972.
• 8: Kowalski, R. Search strategies for theorem proving. In Machine Intelligence 5, B. Meltzer and D. Michie (eds.), American Elsevier, New York, 1970, pp. 181-200.
• 9: Kowalski, R. "AND-OR graphs, theorem-proving graphs and hi-directional search. In Machine Intelligence 7, B. Meltzer and D. Michie (eds.), American Elsevier, New York, 1973.
• 10: Kowalski, R. Predicate logic as programming language. Memo No. 20, U. of Edinburgh, Dep. of Computational Logic; also Proc. of IFIP Congress 1974.
• 11: Kowalski, R., and Kuehner, D. Linear resolution with selection function. Artificial Intelligence J. 2, 3/4 (Winter 1971), 221- 260.
• 12: Kuehner, D. Some special purpose resolution systems. In Machine Intelligence 7, B. Meltzer and D. Michie (eds.), American Elsevier, New York, 1973, pp. 117-128.
• 13: Loveland, D.W. A linear format for resolution. In Proc. IRIA 1968 Syrup. Auto. Demonstration, Lecture Notes on Math., no. 125, Springer-Verlag, New York, 1970,
• 14: Loveland, D.W., and Stickel, M.E. A hole in goal trees: Some guidance from resolution theory. Proc. Third Intl. Conf. on Artificial Intelligence, Stanford, Calif., 1973, pp. 153-161.
• 15: Luckham, D. Refinement theorems in resolution theory. In Proc. IRIA 1968 Syrup. Auto. Demonstration, Lecture Notes on Math., no. 125, Springer-Verlag, New York, 1970.
• 16: E. E. Sibert , D. Michie, Some Binary Derivation Systems, Journal of the ACM (JACM), v.21 n.2, p.175-190, April 1974 [doi>10.1145/321812.321813]
• 17: Minker, J., McSkimin, J.R., and Fishman, D.H. MRPPS-- An interactive refutation proof procedure system for questionanswering, lnternat. J. of Comput. and htJbrm. Sci. 3, 2, 1974.
• 18: Minker, J., and VanderBrug, G.J. Representations of the language recognition problem for a theorem prover. U. of Marylang TR- 199, Sept. 1972; to appear in lnternat. J. of Comput. and bffbrm. Sci. 3, 3, 1974.
• 19: Nils J. Nilsson, Problem-Solving Methods in Artificial Intelligence, McGraw-Hill Pub. Co., 1971
• 20: Pohl, I. Bi-directional search. In Machhle bltelligenee 6, B. Meltzer and D. Michie (eds.), American Elsevier, New York, 1971, pp. 127-140.
• 21: Raphael, B. The frame problem in problem-solving systems. In Artificial Intelligence and Heuristic Programming, N.V. Findler and B. Meltzer (eds.), Springer-Verlag, New York, 1971, pp. 159- 169.
• 22: Robinson, J.A. Automatic deduction with hyperresolution. Internat. J. of Comput. Math. 1, 3 (1965), 227-234.
• 23: Robinson, J.l., and Marks, S.L. A system for automatic analysis of English text. RM-4654-PR, The RAND Corp., Sept. 1965.
• 24: Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.7 Natural Language Processing
          Subjects: Speech recognition and synthesis

General Terms:
Algorithms, Design, Human Factors, Languages, Theory

Keywords:
artificial intelligence, language recognition, problem-reduction representation, state-space representation, theorem proving