This report presents a language, called QA4, designed to facilitate the construction of problem-solving systems used for robot planning, theorem proving, and automatic program synthesis and verification.
Earl D. Sacerdoti, Richard E. Fikes, Rene Reboh, Daniel Sagalowicz, Richard J. Waldinger, & B.M. Wilber
This paper presents a functional overview of the features and capabilities of QLISP, one of the newest of the current generation of very high level languages developed for use in artificial intelligence (AI) research.
This report summaries the results of a three-year project aimed at the design and implementation of computer languages to aid in expressing problem solving procedures in several areas of artificial intelligence including automatic programming, theorem proving, and robot planning.
Cordell Green, Robert A. Yates, Bertram Raphael, & Charles A. Rosen
Research in the development and application of advanced formal theorem-proving techniques. The objective of the proposed work is to design and implement a computer program with general, powerful, and extremely flexible capabilities for both logical inference and data management.
We are submitting a proposal to cover continuing research in the field of self-organizing machines. The four areas of present interest are: Neural Element Development; Integral Geometry Studies; Distributed Memory Studies; Photographic-Optical Simulation of Neural Nets.
The objective of the proposed research is to establish design criteria for an automatic program-synthesizing system. We will devise a natural way to define program-writing problems and describe programming languages, and then improve the known methods of program synthesis and investigate new ones.
Stanford Research Institute proposes herewith a new project to continue and draw together the research that was begun under the two projects mentioned.
This report describes progress toward an "intelligent question-answering system"?a system that can accept facts, retrieve items from memory, and perform logical deductions necessary to answer questions.
Submitting a proposal to extend Contract Nonr 3438 (00) to provide continuing funds for studies of: I) Interpolation or function-modelling in multi-variable systems, II) Learning machine structures composed of cascaded adaptive layers.
Robert A. Yates, Bertram Raphael, & Timothy P. Hart
This paper introduces a new notation, called "resolution graphs," for deduction by resolution in first-order predicate calculus. A resolution graph consists of groups of nodes that represent initial clauses of a deduction and links that represent unifying substitutions.
