Technology
A note on mechanizing higher order logic
It seems most unlikely that one could in general write purely applicative Schonfmkel descriptions', like (5), of functions already known to one in some other form. Fortunately there is a general procedure -- the Schonfmkel procedure -- which, when applied to any expression written in the more intuitive lambda-calculus notation, will produce a correct translation of it into the Schonfinkel notation.
REALIZATION OF A GENERAL GAME-PLAYING PROGRAM
Institut Blaise Pascal, C.N.R.S., 23, Rue du Maroc, 75, Paris XIX, France We study some aspects of a general game-playing program. Such a program receives as data the rules of a game: an algorithm enumerating the moves and an algorithm indicating how to win. The program associates to each move the conditions necessary for this move to occur. It must find how to avoid a dangerous move. We describe the part of the program playing the combinatorial game in order to win: how it can find the moves which lead to victory and what are the only opponent's moves with which he does not lose. This program has been tried with various games: chess, tictac-too, etc. 1. INTRODUCTION My aim was to realize a program playing several games. The rules of the particular game which it must play are given as data. If we want to have a performing program, it must be capable of studying these rules.
Heuristic DENDRAL: A Program for Generating Explanatory Hypotheses in Organic Chemistry
Buchanan, B. G., Sutherland, G. L., Feigenbaum, E. A.
"A computer program has been written which can formulate hypotheses from a given set of scientific data. The data consist of the mass spectrum and the empirical formula of an organic chemical compound. The hypotheses which are produced describe molecular structures which are plausible explanations of the data. The hypotheses are generated systematically within the program's theory of chemical stability and within limiting constraints which are inferred from the data by heuristic rules. The program excludes hypotheses inconsistent with the data and lists its candidate explanatory hypotheses in order of decreasing plausibility. The computer program is heuristic in that it searches for plausible hypotheses in a small subset of the total hypothesis space according to heuristic rules learned from chemists."In Meltzer, B., Michie, D., and Swann, M. (Eds.), Machine Intelligence 4, pp. 209-254. Edinburgh University Press
Theorem-proving by resolution as a basis for question answering systems
This paper shows how a question-answering system can be constructed usingfirst-order logic as its language and a resolution-type theorem-prover as itsdeductive mechanism. A working computer-program, Q A3, based on theseideas is described. The performance of the program compares favorably withseveral other general question-answering systems.Reprinted in B. L. Webber and N. J. Nilsson (eds.), Readings in Artificial Intelligence, pp, 202-222, San Francisco: Morgan Kaufmann, 1981 Machine Intelligence 4, pp. 183-205 Meltzer, B. and Michie, D.(eds.). Edinburgh: Edinburgh University Press.
Heuristic Programming: Ill Structured Problems
This is a reprint of a chapter that first appeared in 1968 in a collection of papers on operations research [1]. The chapter was written to survey the progress in heuristic processes since an earlier 1968 paper on the same topic [2]. In the current collection, it serves as something of a historical introduction to the SOAR system, which occupied Newell and his students for many years. Even though SOAR did not exist at the time this chapter was written, one finds some of the threads that are later to be drawn together into the construction of SOAR. Newell explores so-called weak methods, which trade power for general applicability.
Applications of theorem-proving to problem-solving
In this section we discuss how theorem-proving methods are being tested for several applications in the Stanford Research Institute Artificial Intelligence Group's Automaton (robot). We emphasize that this section describes work that is now in progress, rather than work that is completed. These methods represent explorations in problem solving, rather than final decisions about how the robot is to do problem solving. An overview of the current status of the entire SRI robot project is provided by Nilsson. Coles has developed an English-to-logic translator that is part of the robot.
PROW: A step toward automatic program writing
Summary This paper aescriDes a program, called "PRUW", which writes programs. PROW accepts the specification of the program in the language of predicate calculus, decides the algorithm for the program and then produces a LISP program which is an implementation of the algorithm. Since the construction of the algorithm is obtained by formal theorem-proving techniques, the programs that PROW writes are free from logical errors and do not have to be debugged. The user of PROW can make PROW write programs in languages other than LISP by modifying the part of PROW that translates an algorithm to a LISP program. Thus PROW can be modified to write programs in any language.