Most conventional computer information-retrieval systems are limited by rigid data structures and inflexible query languages. In this paper we will describe an approach to combining and extending recently developed question-answering techniques to reasonably large data files.
Certain similarities between program verification and program synthesis are pointed out. The analogy is illustrated using a "bubble-sort" program. Recent work has shown that automatic deductive methods may be applied to the problems of program verification and program synthesis.
In this note we shall sketch the outline of a simple information-processing model of operant behavior. This model can be viewed as an elaboration of one suggested originally by Deutsch (1960); the present exposition, however, uses terms and concepts of computer science.
An elementary outline of the theorem-proving approach to automatic program synthesis is given, without dwelling on technical details. The method is illustrated by the automatic construction of both recursive and iterative programs operating on natural numbers, lists, and trees.
Waldinger has proposed a scheme for getting around these problems by extending the logic to handle sets and tuples (still keeping an explicit state variable around).
The method employed uses regions as basic data and progresses by successive partitioning of the picture toward an interpretable "goal partition", which is then explored by a heuristic decision tree.
The frame problem has taken on new significance during recent attempts to develop artificially intelligent systems. The problem deals with the difficulty of creating and maintaining an appropriate informational context or "frame of reference" at each stage in certain problem-solving process.
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.
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.
