I received an offline note saying that having just one reference to
Cordell Green was much too brief to do justice to all the interrelated
work that led to logic programming: (01)
JFS
> 5. Logic programming: This is a relation-based alternative to
> functional programming. Cordell Green proposed it in 1969.
> Prolog is the most widely known version, but it has a lot
> of procedural features. But there are more pure versions. (02)
For the record, at the end of this note are some excerpts from
the 1969 article by Cordell G. with my comments marked by ***. (03)
He cited an article by John McCarthy in 1958. Following is a more
detailed version by McCarthy in 1963: (04)
http://www-formal.stanford.edu/jmc/basis1.pdf
A basis for a mathematical theory of computation (05)
McCarthy and Hayes published a related article in 1969: (06)
http://www-formal.stanford.edu/jmc/mcchay69.pdf
Some philosophical problems from the standpoint of AI (07)
Carl Hewitt wrote a paper on Planner in 1969, which also had
a strong influence on logic programming: (08)
http://ijcai.org/Past%20Proceedings/IJCAI-69/PDF/030.pdf
Planner: A language for proving theorems in robots (09)
Following is Cordell Green's thesis (162 pages), also from 1969: (010)
http://www.ai.sri.com/pubs/files/1106.pdf
The Application of Theorem Proving to Question-Answering Systems (011)
Following is a report by Bertram Raphael, who was the supervisor
of the project, which included Cordell G. and others: (012)
http://www.ai.sri.com/pubs/files/raphael68-p6001-final.pdf (013)
That report also mentioned the following project: (014)
> C. Cordell Green, Axiomatization of Pure LISP and List Structures
> (in preparation).
>
> This paper presents a formalization, in first-order logic, of the
> syntax and semantics of a subset of the LISP 1. 5 programming language.
> An example is given, showing how a resolution-type theorem prover can
> use this axiomatization to construct a list-sorting function and to
> prove the correctness of the function constructed. (015)
This would be an early example of a compiler from logic to a more
traditional programming language (if you consider LISP traditional).
The term 'logic programming' came out of work in the 1970s by
Alain Colmerauer, Robert Kowalski, and Maarten van Emden. (016)
John
__________________________________________________________________________ (017)
http://www.kestrel.edu/home/people/green/publications/theorem-proving-retyped.pdf (018)
Theorem-Proving by Resolution as a Basis for Question-Answering Systems (019)
Cordell Green (020)
_Machine Intelligence_ 4, Bernard Meltzer and Donald Michie, editors,
Edinburgh University Press, Edinburgh, Scotland, 1969, pp. 183–205. (021)
Excerpts (my comments are marked by ***): (022)
The type of question-answering system considered in this paper is
ideally one having the following features: (023)
1. A language general enough to describe any reasonable question-
answering subjects and express desired questions and answers. (024)
2. The ability to search efficiently the stored information and
recognize items that are relevant to a particular query. (025)
3. The ability to derive an answer that is not stored explicitly, but
that is derivable by the use of moderate effort from the stored
facts. (026)
4. Interactions between subject areas; for example, if the system has
facts about Subject a and Subject b, then it should be able to
answer a question that requires the use of both sets of facts. (027)
5. Capability of allowing the user to add new facts or replace old
facts conveniently. (028)
This paper argues the case for formal methods to achieve such a system
and presents one particular approach in detail... (029)
McCarthy (1958) proposed using formal languages and deduction to
construct such a system, and suggested allowing the user to give
hints or advice on how to answer a question; he referred to the
proposed system as an 'advice taker'. (030)
Research on 'multi-purpose' or 'general problem-solving' tends to
differ from question-answering as described above by placing more
emphasis on solving deeper, more difficult problems and less emphasis
on user interaction, formality, and efficient retrieval of relevant
facts from a large data base... (031)
The use of a theorem-prover as a question-answerer can be explained
very simply. The question-answerer's knowledge of the world is
expressed as a set of axioms, and the questions asked it are presented
as theorems to be proved. The process of proving the theorem is the
process of deducing the answer to the question... (032)
*** Note that Prolog is a language that has these abilities.
So is Carl Hewitt's Planner and the implemented MicroPlanner. (033)
*** Note that Robert Kowalski (1979) begins his introduction to
_Logic for Problem Solving_ with two examples (pp. 1-12).
The first is a database of family relationships among the Greek
gods and heroes and some axioms that define more complex family
relations. The second is a database with the fact that the
factorial of 0 is 1 and the axiom that the factorial of n is
n times the factorial of n-1. (034)
In some of the applications of QA3 mentioned in section 5 it is
necessary to solve problems of the kind: 'Find a sequence of actions
that will achieve some goal.' One method for solving this type of
problem is to use the notion of transformations of states. We show
here how processes involving changes of state can be described in
first-order logic and how this formalism is used. The process of
finding the values of existentially quantified variables by theorem-
proving can be used to find the sequence of actions necessary to
reach a goal... (035)
*** He explicitly mentions "solve problems." This same method can
generate a plan that consists of a statement of each action.
If you want to generate a program, restrict the actions to
those that correspond to machine instructions. (036)
The theorem-prover can also be used to simplify the answer, as
described in section 3. (037)
*** An application of theorem proving to optimizing the sequence
of operations. All modern relational DBs do such optimization. (038)
Acknowledgements
I would like to acknowledge the advice and guidance of Dr Bertram
Raphael and Professor John McCarthy, as well as help from Mr. R.
Kowalski in correcting an earlier draft of section 3; also the
programming and ideas of Robert A. Yates. (039)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (040)
|